Step
*
1
1
3
1
1
of Lemma
groupoid-edges-commute1
1. G : Groupoid
2. I : Cname List
3. x : nameset(I)
4. J : nameset(I) List
5. j : nameset(I)
6. (j ∈ J)
7. (∀j'∈J.j' = j ∈ Cname)
8. i : ℕ2
9. box : open_box(cubical-nerve(cat(G));I;J;x;i)
10. f : name-morph(I;[])
11. f x ≠ i
12. a : nameset(I)
13. ¬(x = j ∈ Cname)
14. (f x) = 0 ∈ ℕ2
15. (f j) = 0 ∈ ℕ2
16. (1 - f x) = i ∈ ℤ
17. x = a ∈ Cname
18. i = 1 ∈ ℕ2
19. flip(flip(f;x);x) = f ∈ name-morph(I;[])
20. (flip(f;j) x) = 0 ∈ ℕ2
21. (flip(f;x) j) = 0 ∈ ℕ2
22. (flip(f;x) x) = i ∈ ℕ2
23. (∃j∈J. ¬(j = x ∈ Cname))
24. nerve_box_edge(box;f;x) ∈ cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;x))
25. nerve_box_edge(box;flip(f;j);x) ∈ cat-arrow(cat(G)) nerve_box_label(box;flip(f;j))
nerve_box_label(box;flip(flip(f;j);x))
26. nerve_box_edge(box;flip(f;x);j) ∈ cat-arrow(cat(G)) nerve_box_label(box;flip(f;x))
nerve_box_label(box;flip(flip(f;j);x))
⊢ (cat-comp(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;x)) nerve_box_label(box;flip(flip(f;x);j))
nerve_box_edge(box;f;x)
nerve_box_edge(box;flip(f;x);j))
= (cat-comp(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;j)) nerve_box_label(box;flip(flip(f;j);x))
groupoid-square2(G;nerve_box_label(box;f);nerve_box_label(box;flip(f;j));
nerve_box_label(box;flip(f;x));nerve_box_label(box;flip(flip(f;j);x));nerve_box_edge(box;flip(f;j);x);
nerve_box_edge(box;f;x);nerve_box_edge(box;flip(f;x);j))
nerve_box_edge(box;flip(f;j);x))
∈ (cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;x);j)))
BY
{ TACTIC:((GenConclTerm ⌜groupoid-square2(G;nerve_box_label(box;f);nerve_box_label(box;flip(f;j));
nerve_box_label(box;flip(f;x));nerve_box_label(box;flip(flip(f;j);x));
nerve_box_edge(box;flip(f;j);x);nerve_box_edge(box;f;x);nerve_box_edge(box;flip(f;x);j))⌝⋅
THENA Auto
)
THEN D -2
THEN Unfold `cat-square-commutes` -2) }
1
1. G : Groupoid
2. I : Cname List
3. x : nameset(I)
4. J : nameset(I) List
5. j : nameset(I)
6. (j ∈ J)
7. (∀j'∈J.j' = j ∈ Cname)
8. i : ℕ2
9. box : open_box(cubical-nerve(cat(G));I;J;x;i)
10. f : name-morph(I;[])
11. f x ≠ i
12. a : nameset(I)
13. ¬(x = j ∈ Cname)
14. (f x) = 0 ∈ ℕ2
15. (f j) = 0 ∈ ℕ2
16. (1 - f x) = i ∈ ℤ
17. x = a ∈ Cname
18. i = 1 ∈ ℕ2
19. flip(flip(f;x);x) = f ∈ name-morph(I;[])
20. (flip(f;j) x) = 0 ∈ ℕ2
21. (flip(f;x) j) = 0 ∈ ℕ2
22. (flip(f;x) x) = i ∈ ℕ2
23. (∃j∈J. ¬(j = x ∈ Cname))
24. nerve_box_edge(box;f;x) ∈ cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;x))
25. nerve_box_edge(box;flip(f;j);x) ∈ cat-arrow(cat(G)) nerve_box_label(box;flip(f;j))
nerve_box_label(box;flip(flip(f;j);x))
26. nerve_box_edge(box;flip(f;x);j) ∈ cat-arrow(cat(G)) nerve_box_label(box;flip(f;x))
nerve_box_label(box;flip(flip(f;j);x))
27. v : cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;j))
28. (cat-comp(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;j)) nerve_box_label(box;flip(flip(f;j);x)) v
nerve_box_edge(box;flip(f;j);x))
= (cat-comp(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;x)) nerve_box_label(box;flip(flip(f;j);x))
nerve_box_edge(box;f;x)
nerve_box_edge(box;flip(f;x);j))
∈ (cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;j);x)))
29. groupoid-square2(G;nerve_box_label(box;f);nerve_box_label(box;flip(f;j));
nerve_box_label(box;flip(f;x));nerve_box_label(box;flip(flip(f;j);x));nerve_box_edge(box;flip(f;j);x);
nerve_box_edge(box;f;x);nerve_box_edge(box;flip(f;x);j))
= v
∈ {a:cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;j))|
a o nerve_box_edge(box;flip(f;j);x) = nerve_box_edge(box;f;x) o nerve_box_edge(box;flip(f;x);j)}
⊢ (cat-comp(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;x)) nerve_box_label(box;flip(flip(f;x);j))
nerve_box_edge(box;f;x)
nerve_box_edge(box;flip(f;x);j))
= (cat-comp(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(f;j)) nerve_box_label(box;flip(flip(f;j);x)) v
nerve_box_edge(box;flip(f;j);x))
∈ (cat-arrow(cat(G)) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;x);j)))
Latex:
Latex:
1. G : Groupoid
2. I : Cname List
3. x : nameset(I)
4. J : nameset(I) List
5. j : nameset(I)
6. (j \mmember{} J)
7. (\mforall{}j'\mmember{}J.j' = j)
8. i : \mBbbN{}2
9. box : open\_box(cubical-nerve(cat(G));I;J;x;i)
10. f : name-morph(I;[])
11. f x \mneq{} i
12. a : nameset(I)
13. \mneg{}(x = j)
14. (f x) = 0
15. (f j) = 0
16. (1 - f x) = i
17. x = a
18. i = 1
19. flip(flip(f;x);x) = f
20. (flip(f;j) x) = 0
21. (flip(f;x) j) = 0
22. (flip(f;x) x) = i
23. (\mexists{}j\mmember{}J. \mneg{}(j = x))
24. nerve\_box\_edge(box;f;x) \mmember{} cat-arrow(cat(G)) nerve\_box\_label(box;f)
nerve\_box\_label(box;flip(f;x))
25. nerve\_box\_edge(box;flip(f;j);x) \mmember{} cat-arrow(cat(G)) nerve\_box\_label(box;flip(f;j))
nerve\_box\_label(box;flip(flip(f;j);x))
26. nerve\_box\_edge(box;flip(f;x);j) \mmember{} cat-arrow(cat(G)) nerve\_box\_label(box;flip(f;x))
nerve\_box\_label(box;flip(flip(f;j);x))
\mvdash{} (cat-comp(cat(G)) nerve\_box\_label(box;f) nerve\_box\_label(box;flip(f;x))
nerve\_box\_label(box;flip(flip(f;x);j))
nerve\_box\_edge(box;f;x)
nerve\_box\_edge(box;flip(f;x);j))
= (cat-comp(cat(G)) nerve\_box\_label(box;f) nerve\_box\_label(box;flip(f;j))
nerve\_box\_label(box;flip(flip(f;j);x))
groupoid-square2(G;nerve\_box\_label(box;f);nerve\_box\_label(box;flip(f;j));
nerve\_box\_label(box;flip(f;x));nerve\_box\_label(box;flip(flip(f;j);x));
nerve\_box\_edge(box;flip(f;j);x);nerve\_box\_edge(box;f;x);nerve\_box\_edge(box;flip(f;x);j))
nerve\_box\_edge(box;flip(f;j);x))
By
Latex:
TACTIC:((GenConclTerm \mkleeneopen{}groupoid-square2(G;nerve\_box\_label(box;f);nerve\_box\_label(box;flip(f;j));
nerve\_box\_label(box;flip(f;x));nerve\_box\_label(box;flip(flip(f;j);x));
nerve\_box\_edge(box;flip(f;j);x);nerve\_box\_edge(box;f;x);
nerve\_box\_edge(box;flip(f;x);j))\mkleeneclose{}\mcdot{}
THENA Auto
)
THEN D -2
THEN Unfold `cat-square-commutes` -2)
Home
Index