Step
*
1
1
2
2
1
1
of Lemma
poset_functor_extend-face-map1
1. C : SmallCategory
2. I : Cname List
3. L : name-morph(I;[]) ⟶ cat-ob(C)
4. E : i:nameset(I) ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} ⟶ (cat-arrow(C) (L c) (L flip(c;i)))
5. y : nameset(I)
6. a : ℕ2
7. n : ℕ
8. ∀n:ℕn
∀[c1,c2:name-morph(I;[])].
((||filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I)|| ≤ n)
⇒ poset_functor_extend(C;I;L;E;((y:=a) o c1);((y:=a) o c2))
= poset_functor_extend(C;I-[y];L o (λf.((y:=a) o f));λz,f. (E z ((y:=a) o f));c1;c2)
∈ (cat-arrow(C) (L ((y:=a) o c1)) (L ((y:=a) o c2)))
supposing ∀x:nameset(I). ((c1 x) ≤ (c2 x)))
9. c1 : name-morph(I;[])
10. c2 : name-morph(I;[])
11. ¬(filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y]) = [] ∈ (nameset(I) List))
12. ||filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I)|| ≤ n
13. ∀x:nameset(I). ((c1 x) ≤ (c2 x))
14. I ∈ nameset(I) List
15. CnameDeq ∈ EqDecider(nameset(I))
16. ((y:=a) o c1) ∈ name-morph(I;[])
17. ((y:=a) o c2) ∈ name-morph(I;[])
18. filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y]) ∈ {x:nameset(I)| ↑((c1 x =z 0) ∧b (c2 x =z 1))} List
19. v : nameset(I)
20. (c1 v) = 0 ∈ ℤ
21. (c2 v) = 1 ∈ ℤ
22. hd(filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y])) = v ∈ {x:nameset(I)| ↑((c1 x =z 0) ∧b (c2 x =z 1))}
⊢ (cat-comp(C) (L ((y:=a) o c1)) (L flip(((y:=a) o c1);v)) (L ((y:=a) o c2)) (E v ((y:=a) o c1))
poset_functor_extend(C;I;L;E;flip(((y:=a) o c1);v);((y:=a) o c2)))
= (cat-comp(C) (L ((y:=a) o c1)) (L ((y:=a) o flip(c1;v))) (L ((y:=a) o c2)) (E v ((y:=a) o c1))
poset_functor_extend(C;I-[y];L o (λf.((y:=a) o f));λz,f. (E z ((y:=a) o f));flip(c1;v);c2))
∈ (cat-arrow(C) (L ((y:=a) o c1)) (L ((y:=a) o c2)))
BY
{ Assert ⌜||filter(λx.((flip(c1;v) x =z 0) ∧b (c2 x =z 1));I)|| < ||filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I)||⌝⋅ }
1
.....assertion.....
1. C : SmallCategory
2. I : Cname List
3. L : name-morph(I;[]) ⟶ cat-ob(C)
4. E : i:nameset(I) ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} ⟶ (cat-arrow(C) (L c) (L flip(c;i)))
5. y : nameset(I)
6. a : ℕ2
7. n : ℕ
8. ∀n:ℕn
∀[c1,c2:name-morph(I;[])].
((||filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I)|| ≤ n)
⇒ poset_functor_extend(C;I;L;E;((y:=a) o c1);((y:=a) o c2))
= poset_functor_extend(C;I-[y];L o (λf.((y:=a) o f));λz,f. (E z ((y:=a) o f));c1;c2)
∈ (cat-arrow(C) (L ((y:=a) o c1)) (L ((y:=a) o c2)))
supposing ∀x:nameset(I). ((c1 x) ≤ (c2 x)))
9. c1 : name-morph(I;[])
10. c2 : name-morph(I;[])
11. ¬(filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y]) = [] ∈ (nameset(I) List))
12. ||filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I)|| ≤ n
13. ∀x:nameset(I). ((c1 x) ≤ (c2 x))
14. I ∈ nameset(I) List
15. CnameDeq ∈ EqDecider(nameset(I))
16. ((y:=a) o c1) ∈ name-morph(I;[])
17. ((y:=a) o c2) ∈ name-morph(I;[])
18. filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y]) ∈ {x:nameset(I)| ↑((c1 x =z 0) ∧b (c2 x =z 1))} List
19. v : nameset(I)
20. (c1 v) = 0 ∈ ℤ
21. (c2 v) = 1 ∈ ℤ
22. hd(filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y])) = v ∈ {x:nameset(I)| ↑((c1 x =z 0) ∧b (c2 x =z 1))}
⊢ ||filter(λx.((flip(c1;v) x =z 0) ∧b (c2 x =z 1));I)|| < ||filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I)||
2
1. C : SmallCategory
2. I : Cname List
3. L : name-morph(I;[]) ⟶ cat-ob(C)
4. E : i:nameset(I) ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} ⟶ (cat-arrow(C) (L c) (L flip(c;i)))
5. y : nameset(I)
6. a : ℕ2
7. n : ℕ
8. ∀n:ℕn
∀[c1,c2:name-morph(I;[])].
((||filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I)|| ≤ n)
⇒ poset_functor_extend(C;I;L;E;((y:=a) o c1);((y:=a) o c2))
= poset_functor_extend(C;I-[y];L o (λf.((y:=a) o f));λz,f. (E z ((y:=a) o f));c1;c2)
∈ (cat-arrow(C) (L ((y:=a) o c1)) (L ((y:=a) o c2)))
supposing ∀x:nameset(I). ((c1 x) ≤ (c2 x)))
9. c1 : name-morph(I;[])
10. c2 : name-morph(I;[])
11. ¬(filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y]) = [] ∈ (nameset(I) List))
12. ||filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I)|| ≤ n
13. ∀x:nameset(I). ((c1 x) ≤ (c2 x))
14. I ∈ nameset(I) List
15. CnameDeq ∈ EqDecider(nameset(I))
16. ((y:=a) o c1) ∈ name-morph(I;[])
17. ((y:=a) o c2) ∈ name-morph(I;[])
18. filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y]) ∈ {x:nameset(I)| ↑((c1 x =z 0) ∧b (c2 x =z 1))} List
19. v : nameset(I)
20. (c1 v) = 0 ∈ ℤ
21. (c2 v) = 1 ∈ ℤ
22. hd(filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I-[y])) = v ∈ {x:nameset(I)| ↑((c1 x =z 0) ∧b (c2 x =z 1))}
23. ||filter(λx.((flip(c1;v) x =z 0) ∧b (c2 x =z 1));I)|| < ||filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I)||
⊢ (cat-comp(C) (L ((y:=a) o c1)) (L flip(((y:=a) o c1);v)) (L ((y:=a) o c2)) (E v ((y:=a) o c1))
poset_functor_extend(C;I;L;E;flip(((y:=a) o c1);v);((y:=a) o c2)))
= (cat-comp(C) (L ((y:=a) o c1)) (L ((y:=a) o flip(c1;v))) (L ((y:=a) o c2)) (E v ((y:=a) o c1))
poset_functor_extend(C;I-[y];L o (λf.((y:=a) o f));λz,f. (E z ((y:=a) o f));flip(c1;v);c2))
∈ (cat-arrow(C) (L ((y:=a) o c1)) (L ((y:=a) o c2)))
Latex:
Latex:
1. C : SmallCategory
2. I : Cname List
3. L : name-morph(I;[]) {}\mrightarrow{} cat-ob(C)
4. E : i:nameset(I) {}\mrightarrow{} c:\{c:name-morph(I;[])| (c i) = 0\} {}\mrightarrow{} (cat-arrow(C) (L c) (L flip(c;i)))
5. y : nameset(I)
6. a : \mBbbN{}2
7. n : \mBbbN{}
8. \mforall{}n:\mBbbN{}n
\mforall{}[c1,c2:name-morph(I;[])].
((||filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I)|| \mleq{} n)
{}\mRightarrow{} poset\_functor\_extend(C;I;L;E;((y:=a) o c1);((y:=a) o c2))
= poset\_functor\_extend(C;I-[y];L o (\mlambda{}f.((y:=a) o f));\mlambda{}z,f. (E z ((y:=a) o f));c1;c2)
supposing \mforall{}x:nameset(I). ((c1 x) \mleq{} (c2 x)))
9. c1 : name-morph(I;[])
10. c2 : name-morph(I;[])
11. \mneg{}(filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I-[y]) = [])
12. ||filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I)|| \mleq{} n
13. \mforall{}x:nameset(I). ((c1 x) \mleq{} (c2 x))
14. I \mmember{} nameset(I) List
15. CnameDeq \mmember{} EqDecider(nameset(I))
16. ((y:=a) o c1) \mmember{} name-morph(I;[])
17. ((y:=a) o c2) \mmember{} name-morph(I;[])
18. filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I-[y]) \mmember{} \{x:nameset(I)| \muparrow{}((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1))\} L\000Cist
19. v : nameset(I)
20. (c1 v) = 0
21. (c2 v) = 1
22. hd(filter(\mlambda{}x.((c1 x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I-[y])) = v
\mvdash{} (cat-comp(C) (L ((y:=a) o c1)) (L flip(((y:=a) o c1);v)) (L ((y:=a) o c2)) (E v ((y:=a) o c1))
poset\_functor\_extend(C;I;L;E;flip(((y:=a) o c1);v);((y:=a) o c2)))
= (cat-comp(C) (L ((y:=a) o c1)) (L ((y:=a) o flip(c1;v))) (L ((y:=a) o c2)) (E v ((y:=a) o c1))
poset\_functor\_extend(C;I-[y];L o (\mlambda{}f.((y:=a) o f));\mlambda{}z,f. (E z ((y:=a) o f));flip(c1;v);c2))
By
Latex:
Assert \mkleeneopen{}||filter(\mlambda{}x.((flip(c1;v) x =\msubz{} 0) \mwedge{}\msubb{} (c2 x =\msubz{} 1));I)|| < ||filter(\mlambda{}x.((c1 x =\msubz{} 0)
\mwedge{}\msubb{} (c2 x =\msubz{} 1));I)||\mkleeneclose{}\mcdot{}
Home
Index