Step
*
2
1
2
1
2
2
of Lemma
groupoid-nerve-filler-uniform
1. G : Groupoid
2. True
3. I : Cname List
4. J : nameset(I) List
5. ¬(J = [] ∈ (nameset(I) List))
6. x : nameset(I)
7. i : ℕ2
8. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
9. ¬3 < ||bx||
10. K : Cname List
11. f : name-morph(I;K)
12. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
13. ↑isname(f x)
14. ¬False
15. f ∈ nameset(J) ⟶ nameset(K)
16. map(f;J) ∈ nameset(K) List
17. f x ∈ nameset(K)
18. nameset([x / J]) ⊆r name-morph-domain(f;I)
19. ¬↑null(J)
20. ¬↑null(map(f;J))
21. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
22. ¬3 < ||box||
23. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
24. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
25. ||bx|| = ||box|| ∈ ℤ
26. ||bx|| ≤ 3
27. (∀j'∈J.j' = hd(J) ∈ Cname)
28. ||box|| ≤ 3
29. (∀j'∈map(f;J).j' = hd(map(f;J)) ∈ Cname)
30. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
31. k : nameset(K)
32. f1 : {f:name-morph(K;[])| (f k) = 0 ∈ ℕ2}
⊢ poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);
λy,c. nerve_box_edge1(G;bx;x;i;hd(J);c;y);(f o f1);(f o flip(f1;k)))
= poset_functor_extend(cat(G);K;λc.nerve_box_label(box;c);λy,c. nerve_box_edge1(G;box;f x;i;hd(map(f;J));c;y);f1;flip(f1\000C;k))
∈ (cat-arrow(cat(G)) nerve_box_label(bx;(f o f1)) nerve_box_label(bx;(f o flip(f1;k))))
BY
{ Assert ⌜hd(map(f;J)) ∈ nameset(map(f;J))⌝⋅ }
1
.....assertion.....
1. G : Groupoid
2. True
3. I : Cname List
4. J : nameset(I) List
5. ¬(J = [] ∈ (nameset(I) List))
6. x : nameset(I)
7. i : ℕ2
8. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
9. ¬3 < ||bx||
10. K : Cname List
11. f : name-morph(I;K)
12. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
13. ↑isname(f x)
14. ¬False
15. f ∈ nameset(J) ⟶ nameset(K)
16. map(f;J) ∈ nameset(K) List
17. f x ∈ nameset(K)
18. nameset([x / J]) ⊆r name-morph-domain(f;I)
19. ¬↑null(J)
20. ¬↑null(map(f;J))
21. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
22. ¬3 < ||box||
23. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
24. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
25. ||bx|| = ||box|| ∈ ℤ
26. ||bx|| ≤ 3
27. (∀j'∈J.j' = hd(J) ∈ Cname)
28. ||box|| ≤ 3
29. (∀j'∈map(f;J).j' = hd(map(f;J)) ∈ Cname)
30. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
31. k : nameset(K)
32. f1 : {f:name-morph(K;[])| (f k) = 0 ∈ ℕ2}
⊢ hd(map(f;J)) ∈ nameset(map(f;J))
2
1. G : Groupoid
2. True
3. I : Cname List
4. J : nameset(I) List
5. ¬(J = [] ∈ (nameset(I) List))
6. x : nameset(I)
7. i : ℕ2
8. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
9. ¬3 < ||bx||
10. K : Cname List
11. f : name-morph(I;K)
12. ∀i:nameset(I). ((i ∈ J) ⇒ (↑isname(f i)))
13. ↑isname(f x)
14. ¬False
15. f ∈ nameset(J) ⟶ nameset(K)
16. map(f;J) ∈ nameset(K) List
17. f x ∈ nameset(K)
18. nameset([x / J]) ⊆r name-morph-domain(f;I)
19. ¬↑null(J)
20. ¬↑null(map(f;J))
21. box : open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
22. ¬3 < ||box||
23. open_box_image(cubical-nerve(cat(G));I;K;f;bx) = box ∈ open_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
24. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
25. ||bx|| = ||box|| ∈ ℤ
26. ||bx|| ≤ 3
27. (∀j'∈J.j' = hd(J) ∈ Cname)
28. ||box|| ≤ 3
29. (∀j'∈map(f;J).j' = hd(map(f;J)) ∈ Cname)
30. ∀f1:name-morph(K;[]). (nerve_box_label(bx;(f o f1)) = nerve_box_label(box;f1) ∈ cat-ob(cat(G)))
31. k : nameset(K)
32. f1 : {f:name-morph(K;[])| (f k) = 0 ∈ ℕ2}
33. hd(map(f;J)) ∈ nameset(map(f;J))
⊢ poset_functor_extend(cat(G);I;λc.nerve_box_label(bx;c);
λy,c. nerve_box_edge1(G;bx;x;i;hd(J);c;y);(f o f1);(f o flip(f1;k)))
= poset_functor_extend(cat(G);K;λc.nerve_box_label(box;c);λy,c. nerve_box_edge1(G;box;f x;i;hd(map(f;J));c;y);f1;flip(f1\000C;k))
∈ (cat-arrow(cat(G)) nerve_box_label(bx;(f o f1)) nerve_box_label(bx;(f o flip(f1;k))))
Latex:
Latex:
1. G : Groupoid
2. True
3. I : Cname List
4. J : nameset(I) List
5. \mneg{}(J = [])
6. x : nameset(I)
7. i : \mBbbN{}2
8. bx : open\_box(cubical-nerve(cat(G));I;J;x;i)
9. \mneg{}3 < ||bx||
10. K : Cname List
11. f : name-morph(I;K)
12. \mforall{}i:nameset(I). ((i \mmember{} J) {}\mRightarrow{} (\muparrow{}isname(f i)))
13. \muparrow{}isname(f x)
14. \mneg{}False
15. f \mmember{} nameset(J) {}\mrightarrow{} nameset(K)
16. map(f;J) \mmember{} nameset(K) List
17. f x \mmember{} nameset(K)
18. nameset([x / J]) \msubseteq{}r name-morph-domain(f;I)
19. \mneg{}\muparrow{}null(J)
20. \mneg{}\muparrow{}null(map(f;J))
21. box : open\_box(cubical-nerve(cat(G));K;map(f;J);f x;i)
22. \mneg{}3 < ||box||
23. open\_box\_image(cubical-nerve(cat(G));I;K;f;bx) = box
24. \mforall{}f1:name-morph(K;[]). (nerve\_box\_label(bx;(f o f1)) = nerve\_box\_label(box;f1))
25. ||bx|| = ||box||
26. ||bx|| \mleq{} 3
27. (\mforall{}j'\mmember{}J.j' = hd(J))
28. ||box|| \mleq{} 3
29. (\mforall{}j'\mmember{}map(f;J).j' = hd(map(f;J)))
30. \mforall{}f1:name-morph(K;[]). (nerve\_box\_label(bx;(f o f1)) = nerve\_box\_label(box;f1))
31. k : nameset(K)
32. f1 : \{f:name-morph(K;[])| (f k) = 0\}
\mvdash{} poset\_functor\_extend(cat(G);I;\mlambda{}c.nerve\_box\_label(bx;c);
\mlambda{}y,c. nerve\_box\_edge1(G;bx;x;i;hd(J);c;y);(f o f1);(f o flip(f1;k)))
= poset\_functor\_extend(cat(G);K;\mlambda{}c.nerve\_box\_label(box;c);
\mlambda{}y,c. nerve\_box\_edge1(G;box;f x;i;hd(map(f;J));c;y);f1;flip(f1;k))
By
Latex:
Assert \mkleeneopen{}hd(map(f;J)) \mmember{} nameset(map(f;J))\mkleeneclose{}\mcdot{}
Home
Index