Ready for pull request?
This commit is contained in:
Sayantan Khan
parent
d5d004ad6c
commit
75fd816248
2 changed files with 105 additions and 98 deletions
70
hott/algebra/homological_algebra/algebraic_lemmas.hlean
Normal file
70
hott/algebra/homological_algebra/algebraic_lemmas.hlean
Normal file
|
|
@ -0,0 +1,70 @@
|
|||
/-
|
||||
Copyright (c) 2017 Sayantan Khan
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sayantan Khan
|
||||
|
||||
Proofs of elementary algebraic lemmas.
|
||||
-/
|
||||
|
||||
import algebra.group_theory
|
||||
|
||||
open algebra
|
||||
open group
|
||||
|
||||
lemma transport_equality_hom : Π {G₁ G₂ : AbGroup}, Π (φ : homomorphism (G₁) (G₂)), Π {x y : G₁},
|
||||
(x = y) → (φ(x) = φ(y)) :=
|
||||
λ G₁ G₂ φ x, @eq.rec(_)(x)(_) (eq.refl(group_fun φ(x)))
|
||||
|
||||
lemma transport_equality_left_mul : Π {G : AbGroup}, Π (l : G), Π {x y : G},
|
||||
(x = y) → (l*x = l*y) :=
|
||||
λ G l x, @eq.rec(_)(x)(_) (eq.refl(l*x))
|
||||
|
||||
lemma transport_equality_right_mul : Π {G : AbGroup}, Π (r : G), Π {x y : G},
|
||||
(x = y) → (x*r = y*r) :=
|
||||
λ G r x, @eq.rec(_)(x)(_) (eq.refl(x*r))
|
||||
|
||||
lemma mul_inverse : Π {G : AbGroup}, Π (x : G), (x⁻¹)*x = group.one(G) := λ G x, ab_group.mul_left_inv x
|
||||
|
||||
lemma inverse_inverse : Π {G : AbGroup}, Π (x : G), (x⁻¹)⁻¹ = x :=
|
||||
λ G x, inv_inv(x)
|
||||
|
||||
lemma mul_commutative : Π {G : AbGroup}, Π (x y : G), x*y = y*x :=
|
||||
λ G x y, ab_group.mul_comm x y
|
||||
|
||||
lemma mul_associative : Π {G : AbGroup}, Π (x y z : G), (x*y)*z = x*(y*z) :=
|
||||
λ G x y z, ab_group.mul_assoc x y z
|
||||
|
||||
lemma mul_respects_one : Π {G : AbGroup}, Π (x : G),
|
||||
1*x = x := λ G x, ab_group.one_mul x
|
||||
|
||||
lemma cancelling : Π {G : AbGroup}, Π (x y : G), (x = y) → (y⁻¹*x = 1) :=
|
||||
λ G x y proofEq,
|
||||
eq.trans (transport_equality_left_mul (y⁻¹) (proofEq)) (mul_inverse(y))
|
||||
|
||||
lemma hom_respects_one : Π {G₁ G₂ : AbGroup}, Π (φ : homomorphism (G₁) (G₂)), Π (x : G₁),
|
||||
(x = group.one(G₁)) → (φ(x) = group.one(G₂)) :=
|
||||
λ G₁ G₂ φ x proofOfOne, eq.trans (transport_equality_hom (φ)(proofOfOne)) (respect_one φ)
|
||||
|
||||
lemma hom_respects_mul : Π {G₁ G₂ : AbGroup}, Π (φ : homomorphism (G₁) (G₂)), Π (x y : G₁),
|
||||
φ(x*y) = φ(x)*φ(y) :=
|
||||
λ G₁ G₂ φ x y, to_respect_mul φ x y
|
||||
|
||||
lemma hom_respects_inv : Π {G₁ G₂ : AbGroup}, Π (φ : homomorphism (G₁) (G₂)), Π (x : G₁),
|
||||
φ(x⁻¹) = (φ(x))⁻¹ :=
|
||||
λ G₁ G₂ φ x, to_respect_inv φ x
|
||||
|
||||
lemma hom_respects_cancelling : Π {G₁ G₂ : AbGroup}, Π (φ : homomorphism (G₁) (G₂)), Π {x y : G₁},
|
||||
(φ(x) = φ(y)) → φ(y⁻¹*x) = 1 :=
|
||||
λ G₁ G₂ φ x y proofEq,
|
||||
eq.trans
|
||||
(eq.trans (hom_respects_mul (φ) (y⁻¹) (x)) (transport_equality_right_mul (group_fun (φ) (x)) (hom_respects_inv(φ)(y))))
|
||||
(eq.trans (transport_equality_left_mul((group_fun (φ) (y))⁻¹)(proofEq))
|
||||
(mul_inverse(group_fun (φ) (y))))
|
||||
|
||||
/-
|
||||
This was supposed to be a lemma: compiling the proof however led to
|
||||
unification errors which I could not debug. Setting this as an axiom
|
||||
is a temporary workaround.
|
||||
-/
|
||||
axiom combine_terms : Π {G₁ G₂ : AbGroup}, Π (φ : homomorphism (G₁) (G₂)), Π (a c : G₁), Π (b : G₂),
|
||||
φ(a) = b⁻¹*φ(c) → b = φ(a⁻¹*c)
|
||||
|
|
@ -3,11 +3,12 @@ Copyright (c) 2017 Sayantan Khan
|
|||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Sayantan Khan
|
||||
|
||||
Proofs of elementary lemmas.
|
||||
Proofs of elementary homological lemmas.
|
||||
-/
|
||||
|
||||
import algebra.group_theory
|
||||
import .chain_complex_abelian_group
|
||||
import .algebraic_lemmas
|
||||
|
||||
open int
|
||||
open sigma.ops
|
||||
|
|
@ -17,77 +18,6 @@ open abelian_chain_complex
|
|||
open abelian_chain_complex.ab_exact_chain_complex
|
||||
open abelian_chain_complex.exact_chain_map
|
||||
|
||||
set_option unifier.max_steps 1000000
|
||||
|
||||
/-
|
||||
Auxiliary lemmas. May be moved somewhere else.
|
||||
-/
|
||||
|
||||
lemma transport_equality_hom : Π {G₁ G₂ : AbGroup}, Π (φ : homomorphism (G₁) (G₂)), Π {x y : G₁},
|
||||
(x = y) → (φ(x) = φ(y)) :=
|
||||
λ G₁ G₂ φ x, @eq.rec(_)(x)(_) (eq.refl(group_fun φ(x)))
|
||||
|
||||
lemma transport_equality_left_mul : Π {G : AbGroup}, Π (l : G), Π {x y : G},
|
||||
(x = y) → (l*x = l*y) :=
|
||||
λ G l x, @eq.rec(_)(x)(_) (eq.refl(l*x))
|
||||
|
||||
lemma transport_equality_right_mul : Π {G : AbGroup}, Π (r : G), Π {x y : G},
|
||||
(x = y) → (x*r = y*r) :=
|
||||
λ G r x, @eq.rec(_)(x)(_) (eq.refl(x*r))
|
||||
|
||||
lemma mul_inverse : Π {G : AbGroup}, Π (x : G), (x⁻¹)*x = group.one(G) := λ G x, ab_group.mul_left_inv x
|
||||
|
||||
lemma inverse_inverse : Π {G : AbGroup}, Π (x : G), (x⁻¹)⁻¹ = x :=
|
||||
λ G x, inv_inv(x)
|
||||
|
||||
lemma mul_commutative : Π {G : AbGroup}, Π (x y : G), x*y = y*x :=
|
||||
λ G x y, ab_group.mul_comm x y
|
||||
|
||||
lemma mul_associative : Π {G : AbGroup}, Π (x y z : G), (x*y)*z = x*(y*z) :=
|
||||
λ G x y z, ab_group.mul_assoc x y z
|
||||
|
||||
lemma mul_respects_one : Π {G : AbGroup}, Π (x : G),
|
||||
1*x = x := λ G x, ab_group.one_mul x
|
||||
|
||||
lemma cancelling : Π {G : AbGroup}, Π (x y : G), (x = y) → (y⁻¹*x = 1) :=
|
||||
λ G x y proofEq,
|
||||
eq.trans (transport_equality_left_mul (y⁻¹) (proofEq)) (mul_inverse(y))
|
||||
|
||||
lemma hom_respects_one : Π {G₁ G₂ : AbGroup}, Π (φ : homomorphism (G₁) (G₂)), Π (x : G₁),
|
||||
(x = group.one(G₁)) → (φ(x) = group.one(G₂)) :=
|
||||
λ G₁ G₂ φ x proofOfOne, eq.trans (transport_equality_hom (φ)(proofOfOne)) (respect_one φ)
|
||||
|
||||
lemma hom_respects_mul : Π {G₁ G₂ : AbGroup}, Π (φ : homomorphism (G₁) (G₂)), Π (x y : G₁),
|
||||
φ(x*y) = φ(x)*φ(y) :=
|
||||
λ G₁ G₂ φ x y, to_respect_mul φ x y
|
||||
|
||||
lemma hom_respects_inv : Π {G₁ G₂ : AbGroup}, Π (φ : homomorphism (G₁) (G₂)), Π (x : G₁),
|
||||
φ(x⁻¹) = (φ(x))⁻¹ :=
|
||||
λ G₁ G₂ φ x, to_respect_inv φ x
|
||||
|
||||
lemma hom_respects_cancelling : Π {G₁ G₂ : AbGroup}, Π (φ : homomorphism (G₁) (G₂)), Π {x y : G₁},
|
||||
(φ(x) = φ(y)) → φ(y⁻¹*x) = 1 :=
|
||||
λ G₁ G₂ φ x y proofEq,
|
||||
eq.trans
|
||||
(eq.trans (hom_respects_mul (φ) (y⁻¹) (x)) (transport_equality_right_mul (group_fun (φ) (x)) (hom_respects_inv(φ)(y))))
|
||||
(eq.trans (transport_equality_left_mul((group_fun (φ) (y))⁻¹)(proofEq))
|
||||
(mul_inverse(group_fun (φ) (y))))
|
||||
|
||||
axiom combine_terms : Π {G₁ G₂ : AbGroup}, Π (φ : homomorphism (G₁) (G₂)), Π (a c : G₁), Π (b : G₂),
|
||||
φ(a) = b⁻¹*φ(c) → b = φ(a⁻¹*c)
|
||||
|
||||
-- lemma combine_terms : Π {G₁ G₂ : AbGroup}, Π (φ : homomorphism (G₁) (G₂)), Π (a b : G₁), Π (c : G₂),
|
||||
-- φ(a)*φ(b) = c → c = φ(a*b) :=
|
||||
-- λ G₁ G₂ φ a b c proofEq,
|
||||
-- eq.symm (eq.trans (hom_respects_mul (φ) (a) (b)) (proofEq))
|
||||
|
||||
-- lemma take_over : Π {G₁ G₂ : AbGroup}, Π (φ : homomorphism (G₁) (G₂)), Π (a c : G₁), Π (b : G₂),
|
||||
-- φ(a) = b⁻¹ * φ(c) → b*φ(a) = φ(c) :=
|
||||
-- λ G₁ G₂ φ a c b proofEq,
|
||||
-- eq.trans
|
||||
-- (transport_equality_right_mul (group_fun (φ) (a)) (eq.symm (inverse_inverse(b))))
|
||||
-- (transport_equality_left_mul ((b⁻¹)⁻¹) (proofEq))
|
||||
|
||||
/-
|
||||
Simple lemma showing surjective and injective imply bijective.
|
||||
-/
|
||||
|
|
@ -140,17 +70,19 @@ theorem left_right_zero_implies_bijective : Π (C : ab_exact_chain_complex), Π
|
|||
(left_zero_implies_injective(C)(z)(pLeftZeroMap))
|
||||
|
||||
/-
|
||||
Four lemma
|
||||
Proof of the Four Lemma. Proving the lemma requires nine lemmas,
|
||||
roughly one for each step in the diagram chase. This could have
|
||||
been done in a cleaner manner.
|
||||
-/
|
||||
|
||||
lemma lFlLemmaOne : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
lemma subLemmaOne : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
surjective_map (group_map(M)(z)) → surjective_map (group_map(M)(z-1-1)) → injective_map (group_map(M)(z-1-1-1)) →
|
||||
(Π (b' : chain_group(C₂)(z-1)), (Σ (c : chain_group(C₁)(z-1-1)), group_map(M)(z-1-1)(c) = boundary_map(C₂)(z-1)(b'))) :=
|
||||
λ C₁ C₂ M z proofSurj_m proofSurj_p proofInj_q b',
|
||||
((λ c', surjective_map.get_preimage(proofSurj_p)(c'))
|
||||
(boundary_map(C₂)(z-1)(b')))
|
||||
|
||||
lemma lFlLemmaTwo : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
lemma subLemmaTwo : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
surjective_map (group_map(M)(z)) → surjective_map (group_map(M)(z-1-1)) → injective_map (group_map(M)(z-1-1-1)) →
|
||||
Π (c : chain_group(C₁)(z-1-1)), (boundary_map(C₂)(z-1-1)(group_map(M)(z-1-1)(c)) = group.one(chain_group(C₂)(z-1-1-1))) →
|
||||
(boundary_map(C₁)(z-1-1)(c) = group.one(chain_group(C₁)(z-1-1-1))) :=
|
||||
|
|
@ -161,34 +93,34 @@ lemma lFlLemmaTwo : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain
|
|||
(proofBottomRight)
|
||||
)
|
||||
|
||||
lemma lFlLemmaThree : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
lemma subLemmaThree : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
surjective_map (group_map(M)(z)) → surjective_map (group_map(M)(z-1-1)) → injective_map (group_map(M)(z-1-1-1)) →
|
||||
Π (b' : chain_group(C₂)(z-1)), Π (c : chain_group(C₁)(z-1-1)),
|
||||
((group_map(M)(z-1-1)(c)) = (boundary_map(C₂)(z-1)(b'))) → (boundary_map(C₁)(z-1-1)(c) = group.one(chain_group(C₁)(z-1-1-1))) :=
|
||||
λ C₁ C₂ M z proofSurj_m proofSurj_p proofInj_q b' c proofEq,
|
||||
lFlLemmaTwo (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (c)
|
||||
subLemmaTwo (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (c)
|
||||
(eq.trans (transport_equality_hom (boundary_map(C₂)(z-1-1)) (proofEq))
|
||||
(boundary_of_boundary(C₂)(z-1)(b')))
|
||||
|
||||
lemma lFlLemmaFour : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
lemma subLemmaFour : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
surjective_map (group_map(M)(z)) → surjective_map (group_map(M)(z-1-1)) → injective_map (group_map(M)(z-1-1-1)) →
|
||||
Π (b' : chain_group(C₂)(z-1)), Σ (b : chain_group(C₁)(z-1)), (group_map(M)(z-1-1)(boundary_map(C₁)(z-1)(b)) = boundary_map(C₂)(z-1)(b')) :=
|
||||
λ C₁ C₂ M z proofSurj_m proofSurj_p proofInj_q b',
|
||||
(
|
||||
(λ c proofEq,
|
||||
sigma.mk
|
||||
(pr₁(exactness(C₁)(z-1)(c) (lFlLemmaThree (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b') (c) (proofEq) )))
|
||||
(pr₁(exactness(C₁)(z-1)(c) (subLemmaThree (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b') (c) (proofEq) )))
|
||||
(
|
||||
eq.trans
|
||||
(transport_equality_hom (group_map(M)(z-1-1)) (pr₂(exactness(C₁)(z-1)(c) (lFlLemmaThree (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b') (c) (proofEq) ))))
|
||||
(transport_equality_hom (group_map(M)(z-1-1)) (pr₂(exactness(C₁)(z-1)(c) (subLemmaThree (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b') (c) (proofEq) ))))
|
||||
(proofEq)
|
||||
)
|
||||
)
|
||||
(pr₁(lFlLemmaOne (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b')))
|
||||
(pr₂(lFlLemmaOne (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b')))
|
||||
(pr₁(subLemmaOne (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b')))
|
||||
(pr₂(subLemmaOne (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b')))
|
||||
)
|
||||
|
||||
lemma lFlLemmaFive : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
lemma subLemmaFive : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
surjective_map (group_map(M)(z)) → surjective_map (group_map(M)(z-1-1)) → injective_map (group_map(M)(z-1-1-1)) →
|
||||
Π (b' : chain_group(C₂)(z-1)), Σ (b : chain_group(C₁)(z-1)), boundary_map(C₂)(z-1)(group_map(M)(z-1)(b)) = boundary_map(C₂)(z-1)(b') :=
|
||||
λ C₁ C₂ M z proofSurj_m proofSurj_p proofInj_q b',
|
||||
|
|
@ -196,11 +128,11 @@ lemma lFlLemmaFive : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chai
|
|||
(λ b proofEq,
|
||||
sigma.mk (b) (eq.trans (commutes(M)(z-1)(b)) (proofEq))
|
||||
)
|
||||
(pr₁(lFlLemmaFour (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b')))
|
||||
(pr₂(lFlLemmaFour (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b')))
|
||||
(pr₁(subLemmaFour (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b')))
|
||||
(pr₂(subLemmaFour (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b')))
|
||||
)
|
||||
|
||||
lemma lFlLemmaSix : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
lemma subLemmaSix : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
surjective_map (group_map(M)(z)) → surjective_map (group_map(M)(z-1-1)) → injective_map (group_map(M)(z-1-1-1)) →
|
||||
Π (b' : chain_group(C₂)(z-1)), Σ (b : chain_group(C₁)(z-1)), boundary_map(C₂)(z-1)((b'⁻¹)*group_map(M)(z-1)(b)) = 1 :=
|
||||
λ C₁ C₂ M z proofSurj_m proofSurj_p proofInj_q b',
|
||||
|
|
@ -209,11 +141,11 @@ lemma lFlLemmaSix : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain
|
|||
sigma.mk (b)
|
||||
(hom_respects_cancelling (boundary_map(C₂)(z-1)) (proofEq))
|
||||
)
|
||||
(pr₁(lFlLemmaFive (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b')))
|
||||
(pr₂(lFlLemmaFive (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b')))
|
||||
(pr₁(subLemmaFive (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b')))
|
||||
(pr₂(subLemmaFive (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b')))
|
||||
)
|
||||
|
||||
lemma lFlLemmaSeven : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
lemma subLemmaSeven : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
surjective_map (group_map(M)(z)) → surjective_map (group_map(M)(z-1-1)) → injective_map (group_map(M)(z-1-1-1)) →
|
||||
Π (b' : chain_group(C₂)(z-1)), Π (b : chain_group(C₁)(z-1)), boundary_map(C₂)(z-1)((b'⁻¹)*group_map(M)(z-1)(b)) = 1 →
|
||||
Σ (a : chain_group(C₁)(z)), boundary_map(C₂)(z)(group_map(M)(z)(a)) = (b'⁻¹)*group_map(M)(z-1)(b) :=
|
||||
|
|
@ -231,7 +163,7 @@ lemma lFlLemmaSeven : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_cha
|
|||
(pr₂(exactness(C₂)(z)((b'⁻¹)*group_map(M)(z-1)(b))(proofZero)))
|
||||
)
|
||||
|
||||
lemma lFlLemmaEight : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
lemma subLemmaEight : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
surjective_map (group_map(M)(z)) → surjective_map (group_map(M)(z-1-1)) → injective_map (group_map(M)(z-1-1-1)) →
|
||||
Π (b' : chain_group(C₂)(z-1)), Π (b : chain_group(C₁)(z-1)), boundary_map(C₂)(z-1)((b'⁻¹)*group_map(M)(z-1)(b)) = 1 →
|
||||
Σ (a : chain_group(C₁)(z)), group_map(M)(z-1)(boundary_map(C₁)(z)(a)) = (b'⁻¹)*group_map(M)(z-1)(b) :=
|
||||
|
|
@ -242,11 +174,11 @@ lemma lFlLemmaEight : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_cha
|
|||
(a)
|
||||
(eq.trans (eq.symm (commutes(M)(z)(a))) (proofBottomRight))
|
||||
)
|
||||
(pr₁(lFlLemmaSeven (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b') (b) (proofZero)))
|
||||
(pr₂(lFlLemmaSeven (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b') (b) (proofZero)))
|
||||
(pr₁(subLemmaSeven (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b') (b) (proofZero)))
|
||||
(pr₂(subLemmaSeven (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b') (b) (proofZero)))
|
||||
)
|
||||
|
||||
lemma lFlLemmaNine : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
lemma subLemmaNine : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
surjective_map (group_map(M)(z)) → surjective_map (group_map(M)(z-1-1)) → injective_map (group_map(M)(z-1-1-1)) →
|
||||
Π (b' : chain_group(C₂)(z-1)), Σ (j : chain_group(C₁)(z-1)), group_map(M)(z-1)(j) = b' :=
|
||||
λ C₁ C₂ M z proofSurj_m proofSurj_p proofInj_q b',
|
||||
|
|
@ -257,15 +189,20 @@ lemma lFlLemmaNine : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chai
|
|||
((boundary_map(C₁)(z)(a))⁻¹*b)
|
||||
(eq.symm (combine_terms (group_map(M)(z-1)) (boundary_map(C₁)(z)(a)) (b) (b') (proofEq2)))
|
||||
)
|
||||
(pr₁ (lFlLemmaEight (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b') (b) (proofEq1)))
|
||||
(pr₂ (lFlLemmaEight (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b') (b) (proofEq1)))
|
||||
(pr₁ (subLemmaEight (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b') (b) (proofEq1)))
|
||||
(pr₂ (subLemmaEight (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b') (b) (proofEq1)))
|
||||
)
|
||||
(pr₁ (lFlLemmaSix (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b')))
|
||||
(pr₂ (lFlLemmaSix (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b')))
|
||||
(pr₁ (subLemmaSix (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b')))
|
||||
(pr₂ (subLemmaSix (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b')))
|
||||
)
|
||||
|
||||
/-
|
||||
This is the surjective variant of the Four Lemma. Proving the injective variant
|
||||
of the Four Lemma will take a similar approach, and once we have both, the Five
|
||||
Lemma is an easy consequence.
|
||||
-/
|
||||
theorem FourLemma : Π {C₁ C₂ : ab_exact_chain_complex}, Π (M : exact_chain_map (C₁) (C₂)), Π (z : ℤ),
|
||||
surjective_map (group_map(M)(z)) → surjective_map (group_map(M)(z-1-1)) → injective_map (group_map(M)(z-1-1-1)) →
|
||||
surjective_map (group_map(M)(z-1)) :=
|
||||
λ C₁ C₂ M z proofSurj_m proofSurj_p proofInj_q,
|
||||
surjective_map.mk (λ b', lFlLemmaNine (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b'))
|
||||
surjective_map.mk (λ b', subLemmaNine (M) (z) (proofSurj_m) (proofSurj_p) (proofInj_q) (b'))
|
||||
|
|
|
|||
Loading…
Reference in a new issue