Step
*
1
2
1
1
1
of Lemma
nerve_box_label_same
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : I-face(cubical-nerve(C);I) List
7. ∀f1,f2:I-face(cubical-nerve(C);I).
((f1 ∈ box)
⇒ (f2 ∈ box)
⇒ (¬(dimension(f1) = dimension(f2) ∈ Cname))
⇒ ((dimension(f2):=direction(f2))(cube(f1))
= (dimension(f1):=direction(f1))(cube(f2))
∈ cubical-nerve(C)(I-[dimension(f1); dimension(f2)])))
8. ¬(x ∈ J)
9. l_subset(Cname;J;I)
10. ∀y:nameset(J). ∀c:ℕ2. (∃f∈box. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
11. (∃f∈box. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
12. (∀f∈box.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
13. (∀f∈box.(fst(f) ∈ [x / J]))
14. (∀f1,f2∈box. ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
15. L : name-morph(I;[])
16. ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))
17. f : I-face(cubical-nerve(C);I)
18. direction(f) = (L dimension(f)) ∈ ℕ2
19. (f ∈ box)
20. v : I-face(cubical-nerve(C);I)
21. (v ∈ box)
22. direction(v) = (L dimension(v)) ∈ ℕ2
23. nerve-box-face(box;L) = v ∈ {f:I-face(cubical-nerve(C);I)| (f ∈ box) ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)}
24. ¬(dimension(v) = dimension(f) ∈ Cname)
⊢ ∀G:Functor(poset-cat(I-[dimension(f)]);C). ∀F:Functor(poset-cat(I-[dimension(v)]);C).
((functor-comp(poset-functor(I-[dimension(v)];I-[dimension(v); dimension(f)];(dimension(f):=direction(f)));F)
= functor-comp(poset-functor(I-[dimension(f)];I-[dimension(v); dimension(f)];(dimension(v):=direction(v)));G)
∈ Functor(poset-cat(I-[dimension(v); dimension(f)]);C))
⇒ ((ob(G) L) = (ob(F) L) ∈ cat-ob(C)))
BY
{ ((Assert (dimension(f):=L dimension(f)) ∈ name-morph(I-[dimension(v)];I-[dimension(v); dimension(f)]) BY
(FaceMapDiff2 THEN Auto))
THEN (Assert (dimension(v):=L dimension(v)) ∈ name-morph(I-[dimension(f)];I-[dimension(v); dimension(f)]) BY
(FaceMapDiff2 THEN Auto))
THEN Auto) }
1
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. box : I-face(cubical-nerve(C);I) List
7. ∀f1,f2:I-face(cubical-nerve(C);I).
((f1 ∈ box)
⇒ (f2 ∈ box)
⇒ (¬(dimension(f1) = dimension(f2) ∈ Cname))
⇒ ((dimension(f2):=direction(f2))(cube(f1))
= (dimension(f1):=direction(f1))(cube(f2))
∈ cubical-nerve(C)(I-[dimension(f1); dimension(f2)])))
8. ¬(x ∈ J)
9. l_subset(Cname;J;I)
10. ∀y:nameset(J). ∀c:ℕ2. (∃f∈box. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))
11. (∃f∈box. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))
12. (∀f∈box.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2)))
13. (∀f∈box.(fst(f) ∈ [x / J]))
14. (∀f1,f2∈box. ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))
15. L : name-morph(I;[])
16. ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))
17. f : I-face(cubical-nerve(C);I)
18. direction(f) = (L dimension(f)) ∈ ℕ2
19. (f ∈ box)
20. v : I-face(cubical-nerve(C);I)
21. (v ∈ box)
22. direction(v) = (L dimension(v)) ∈ ℕ2
23. nerve-box-face(box;L) = v ∈ {f:I-face(cubical-nerve(C);I)| (f ∈ box) ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)}
24. ¬(dimension(v) = dimension(f) ∈ Cname)
25. (dimension(f):=L dimension(f)) ∈ name-morph(I-[dimension(v)];I-[dimension(v); dimension(f)])
26. (dimension(v):=L dimension(v)) ∈ name-morph(I-[dimension(f)];I-[dimension(v); dimension(f)])
27. G : Functor(poset-cat(I-[dimension(f)]);C)
28. F : Functor(poset-cat(I-[dimension(v)]);C)
29. functor-comp(poset-functor(I-[dimension(v)];I-[dimension(v); dimension(f)];(dimension(f):=direction(f)));F)
= functor-comp(poset-functor(I-[dimension(f)];I-[dimension(v); dimension(f)];(dimension(v):=direction(v)));G)
∈ Functor(poset-cat(I-[dimension(v); dimension(f)]);C)
⊢ (ob(G) L) = (ob(F) L) ∈ cat-ob(C)
Latex:
Latex:
1. C : SmallCategory
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : \mBbbN{}2
6. box : I-face(cubical-nerve(C);I) List
7. \mforall{}f1,f2:I-face(cubical-nerve(C);I).
((f1 \mmember{} box)
{}\mRightarrow{} (f2 \mmember{} box)
{}\mRightarrow{} (\mneg{}(dimension(f1) = dimension(f2)))
{}\mRightarrow{} ((dimension(f2):=direction(f2))(cube(f1)) = (dimension(f1):=direction(f1))(cube(f2))))
8. \mneg{}(x \mmember{} J)
9. l\_subset(Cname;J;I)
10. \mforall{}y:nameset(J). \mforall{}c:\mBbbN{}2. (\mexists{}f\mmember{}box. face-name(f) = <y, c>)
11. (\mexists{}f\mmember{}box. face-name(f) = <x, i>)
12. (\mforall{}f\mmember{}box.\mneg{}(face-name(f) = <x, 1 - i>))
13. (\mforall{}f\mmember{}box.(fst(f) \mmember{} [x / J]))
14. (\mforall{}f1,f2\mmember{}box. \mneg{}(face-name(f1) = face-name(f2)))
15. L : name-morph(I;[])
16. ((L x) = i) \mvee{} (\mneg{}\muparrow{}null(J))
17. f : I-face(cubical-nerve(C);I)
18. direction(f) = (L dimension(f))
19. (f \mmember{} box)
20. v : I-face(cubical-nerve(C);I)
21. (v \mmember{} box)
22. direction(v) = (L dimension(v))
23. nerve-box-face(box;L) = v
24. \mneg{}(dimension(v) = dimension(f))
\mvdash{} \mforall{}G:Functor(poset-cat(I-[dimension(f)]);C). \mforall{}F:Functor(poset-cat(I-[dimension(v)]);C).
((functor-comp(poset-functor(I-[dimension(v)];I-[dimension(v);
dimension(f)];(dimension(f):=direction(f)));F)
= functor-comp(poset-functor(I-[dimension(f)];I-[dimension(v);
dimension(f)];(dimension(v):=direction(v)));G))
{}\mRightarrow{} ((ob(G) L) = (ob(F) L)))
By
Latex:
((Assert (dimension(f):=L dimension(f)) \mmember{} name-morph(I-[dimension(v)];I-[dimension(v);
dimension(f)]) BY
(FaceMapDiff2 THEN Auto))
THEN (Assert (dimension(v):=L dimension(v)) \mmember{} name-morph(I-[dimension(f)];I-[dimension(v);
dimension(f)]) BY
(FaceMapDiff2 THEN Auto))
THEN Auto)
Home
Index