noncomputable def HomologyLongExactSequence.connectingHomomorphism {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : S.X₃.homology i ⟶ S.X₁.homology j

The connecting (boundary) homomorphism ∂ : Hᵢ(C) ⟶ Hⱼ(A) associated with a short exact sequence 0 → A → B → C → 0 of chain complexes, where j is the index reached from i under the complex shape. This is the key map appearing in the homology long exact sequence (Theorem 9.1).

theorem HomologyLongExactSequence.exact_f_g {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i : ι) : { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i, g := HomologicalComplex.homologyMap S.g i, zero := ⋯ }.Exact

Exactness of the long exact sequence at the middle term Hᵢ(B): the image of Hᵢ(A) → Hᵢ(B) equals the kernel of Hᵢ(B) → Hᵢ(C) for a short exact sequence of chain complexes.

theorem HomologyLongExactSequence.exact_g_δ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i, g := hS.δ i j hij, zero := ⋯ }.Exact

Exactness of the long exact sequence at Hᵢ(C): the image of Hᵢ(B) → Hᵢ(C) equals the kernel of the connecting map ∂ : Hᵢ(C) → Hⱼ(A).

theorem HomologyLongExactSequence.exact_δ_f {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : { X₁ := S.X₃.homology i, X₂ := S.X₁.homology j, X₃ := S.X₂.homology j, f := hS.δ i j hij, g := HomologicalComplex.homologyMap S.f j, zero := ⋯ }.Exact

Exactness of the long exact sequence at Hⱼ(A): the image of the connecting map ∂ : Hᵢ(C) → Hⱼ(A) equals the kernel of Hⱼ(A) → Hⱼ(B).

structure HomologyLongExactSequence.HomologyLongExactSequenceData {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : Type u_3

Packaged data for the homology long exact sequence (Theorem 9.1): the connecting homomorphism δ and the three exactness statements (at Hᵢ(B), at Hᵢ(C), and at Hⱼ(A)) for a short exact sequence of chain complexes.

• δ : S.X₃.homology i ⟶ S.X₁.homology j
• exact_at_X₂ : { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i, g := HomologicalComplex.homologyMap S.g i, zero := ⋯ }.Exact
• exact_at_X₃ : { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i, g := hS.δ i j hij, zero := ⋯ }.Exact
• exact_at_X₁ : { X₁ := S.X₃.homology i, X₂ := S.X₁.homology j, X₃ := S.X₂.homology j, f := hS.δ i j hij, g := HomologicalComplex.homologyMap S.f j, zero := ⋯ }.Exact

noncomputable def HomologyLongExactSequence.homologyLongExactSequence {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι) (hij : c.Rel i j) : HomologyLongExactSequenceData hS i j hij

Theorem 9.1 (Homology long exact sequence). Given a short exact sequence 0 → A → B → C → 0 of chain complexes, there is a natural connecting homomorphism ∂ : Hₙ(C) → Hₙ₋₁(A) such that ⋯ → Hₙ(A) → Hₙ(B) → Hₙ(C) →∂ Hₙ₋₁(A) → ⋯ is exact. This bundles the connecting map together with exactness at each spot.

theorem FiveLemma.five_lemma {A₁ : Type u_1} {A₂ : Type u_2} {A₃ : Type u_3} {A₄ : Type u_4} {A₅ : Type u_5} {B₁ : Type u_6} {B₂ : Type u_7} {B₃ : Type u_8} {B₄ : Type u_9} {B₅ : Type u_10} [AddCommGroup A₁] [AddCommGroup A₂] [AddCommGroup A₃] [AddCommGroup A₄] [AddCommGroup A₅] [AddCommGroup B₁] [AddCommGroup B₂] [AddCommGroup B₃] [AddCommGroup B₄] [AddCommGroup B₅] (α₁ : A₁ →+ A₂) (α₂ : A₂ →+ A₃) (α₃ : A₃ →+ A₄) (α₄ : A₄ →+ A₅) (β₁ : B₁ →+ B₂) (β₂ : B₂ →+ B₃) (β₃ : B₃ →+ B₄) (β₄ : B₄ →+ B₅) (f₁ : A₁ →+ B₁) (f₂ : A₂ →+ B₂) (f₃ : A₃ →+ B₃) (f₄ : A₄ →+ B₄) (f₅ : A₅ →+ B₅) (hc₁ : β₁.comp f₁ = f₂.comp α₁) (hc₂ : β₂.comp f₂ = f₃.comp α₂) (hc₃ : β₃.comp f₃ = f₄.comp α₃) (hc₄ : β₄.comp f₄ = f₅.comp α₄) (hα₁ : Function.Exact ⇑α₁ ⇑α₂) (hα₂ : Function.Exact ⇑α₂ ⇑α₃) (hα₃ : Function.Exact ⇑α₃ ⇑α₄) (hβ₁ : Function.Exact ⇑β₁ ⇑β₂) (hβ₂ : Function.Exact ⇑β₂ ⇑β₃) (hβ₃ : Function.Exact ⇑β₃ ⇑β₄) (hf₁ : Function.Surjective ⇑f₁) (hf₂ : Function.Bijective ⇑f₂) (hf₄ : Function.Bijective ⇑f₄) (hf₅ : Function.Injective ⇑f₅) : Function.Bijective ⇑f₃

Proposition 9.4 (Five lemma). In a commutative ladder of two exact sequences of five abelian groups, if the outer four vertical maps f₁, f₂, f₄, f₅ are suitably surjective/bijective/injective (here f₁ surjective, f₂ and f₄ bijective, f₅ injective), then the middle map f₃ is bijective.

structure FiveLemma.HomologyLadder : Type (max (max (max (max (max (u_11 + 1) (u_12 + 1)) (u_13 + 1)) (u_14 + 1)) (u_15 + 1)) (u_16 + 1))

A "homology ladder": a commutative ladder of two long exact sequences (with maps i, p, δ on each row) of graded abelian groups indexed by ℤ, together with vertical chain maps fMap, gMap, hMap between corresponding groups. This is the algebraic setup used to apply the five lemma degree-by-degree (Proposition 9.4).

• HA : ℤ → Type u_11
• HB : ℤ → Type u_12
• HC : ℤ → Type u_13
• HA' : ℤ → Type u_14
• HB' : ℤ → Type u_15
• HC' : ℤ → Type u_16
• grpHA (n : ℤ) : AddCommGroup (self.HA n)
• grpHB (n : ℤ) : AddCommGroup (self.HB n)
• grpHC (n : ℤ) : AddCommGroup (self.HC n)
• grpHA' (n : ℤ) : AddCommGroup (self.HA' n)
• grpHB' (n : ℤ) : AddCommGroup (self.HB' n)
• grpHC' (n : ℤ) : AddCommGroup (self.HC' n)
• iMap (n : ℤ) : self.HA n →+ self.HB n
• pMap (n : ℤ) : self.HB n →+ self.HC n
• δ (n : ℤ) : self.HC (n + 1) →+ self.HA n
• iMap' (n : ℤ) : self.HA' n →+ self.HB' n
• pMap' (n : ℤ) : self.HB' n →+ self.HC' n
• δ' (n : ℤ) : self.HC' (n + 1) →+ self.HA' n
• fMap (n : ℤ) : self.HA n →+ self.HA' n
• gMap (n : ℤ) : self.HB n →+ self.HB' n
• hMap (n : ℤ) : self.HC n →+ self.HC' n
• exact_ip (n : ℤ) : Function.Exact ⇑(self.iMap n) ⇑(self.pMap n)
• exact_pδ (n : ℤ) : Function.Exact ⇑(self.pMap (n + 1)) ⇑(self.δ n)
• exact_δi (n : ℤ) : Function.Exact ⇑(self.δ n) ⇑(self.iMap n)
• exact_i'p' (n : ℤ) : Function.Exact ⇑(self.iMap' n) ⇑(self.pMap' n)
• exact_p'δ' (n : ℤ) : Function.Exact ⇑(self.pMap' (n + 1)) ⇑(self.δ' n)
• exact_δ'i' (n : ℤ) : Function.Exact ⇑(self.δ' n) ⇑(self.iMap' n)
• comm_fi (n : ℤ) : (self.iMap' n).comp (self.fMap n) = (self.gMap n).comp (self.iMap n)
• comm_gp (n : ℤ) : (self.pMap' n).comp (self.gMap n) = (self.hMap n).comp (self.pMap n)
• comm_hδ (n : ℤ) : (self.δ' n).comp (self.hMap (n + 1)) = (self.fMap n).comp (self.δ n)

theorem FiveLemma.HomologyLadder.h_bijective_of_f_g_bijective (L : HomologyLadder) (hf : ∀ (n : ℤ), Function.Bijective ⇑(L.fMap n)) (hg : ∀ (n : ℤ), Function.Bijective ⇑(L.gMap n)) (n : ℤ) : Function.Bijective ⇑(L.hMap (n + 1))

In a homology ladder, if fMap and gMap are bijective in every degree, then so is hMap (proved via the five lemma applied to a window of the ladder).

theorem FiveLemma.HomologyLadder.g_bijective_of_f_h_bijective (L : HomologyLadder) (hf : ∀ (n : ℤ), Function.Bijective ⇑(L.fMap n)) (hh : ∀ (n : ℤ), Function.Bijective ⇑(L.hMap n)) (n : ℤ) : Function.Bijective ⇑(L.gMap (n + 1))

In a homology ladder, if fMap and hMap are bijective in every degree, then so is gMap (proved via the five lemma applied to a window of the ladder).

theorem FiveLemma.HomologyLadder.f_bijective_of_g_h_bijective (L : HomologyLadder) (hg : ∀ (n : ℤ), Function.Bijective ⇑(L.gMap n)) (hh : ∀ (n : ℤ), Function.Bijective ⇑(L.hMap n)) (n : ℤ) : Function.Bijective ⇑(L.fMap n)

In a homology ladder, if gMap and hMap are bijective in every degree, then so is fMap (proved via the five lemma applied to a window of the ladder).

structure FiveLemma.LongExactLadder : Type (max (max (max (max (max (u_11 + 1) (u_12 + 1)) (u_13 + 1)) (u_14 + 1)) (u_15 + 1)) (u_16 + 1))

A ladder of two long exact sequences (with maps ι, π, δ on each row), connected by vertical maps fA, fB, fC. This is a streamlined presentation of the data needed for the 2-out-of-3 isomorphism principle in homology (Corollary 9.5 and Proposition 9.6).

• A : ℤ → Type u_11
• A' : ℤ → Type u_12
• B : ℤ → Type u_13
• B' : ℤ → Type u_14
• C : ℤ → Type u_15
• C' : ℤ → Type u_16
• grpA (n : ℤ) : AddCommGroup (self.A n)
• grpA' (n : ℤ) : AddCommGroup (self.A' n)
• grpB (n : ℤ) : AddCommGroup (self.B n)
• grpB' (n : ℤ) : AddCommGroup (self.B' n)
• grpC (n : ℤ) : AddCommGroup (self.C n)
• grpC' (n : ℤ) : AddCommGroup (self.C' n)
• ι (n : ℤ) : self.A n →+ self.B n
• π (n : ℤ) : self.B n →+ self.C n
• δ (n : ℤ) : self.C (n + 1) →+ self.A n
• ι' (n : ℤ) : self.A' n →+ self.B' n
• π' (n : ℤ) : self.B' n →+ self.C' n
• δ' (n : ℤ) : self.C' (n + 1) →+ self.A' n
• fA (n : ℤ) : self.A n →+ self.A' n
• fB (n : ℤ) : self.B n →+ self.B' n
• fC (n : ℤ) : self.C n →+ self.C' n
• exact_δι (n : ℤ) : Function.Exact ⇑(self.δ n) ⇑(self.ι n)
• exact_ιπ (n : ℤ) : Function.Exact ⇑(self.ι n) ⇑(self.π n)
• exact_πδ (n : ℤ) : Function.Exact ⇑(self.π (n + 1)) ⇑(self.δ n)
• exact_δ'ι' (n : ℤ) : Function.Exact ⇑(self.δ' n) ⇑(self.ι' n)
• exact_ι'π' (n : ℤ) : Function.Exact ⇑(self.ι' n) ⇑(self.π' n)
• exact_π'δ' (n : ℤ) : Function.Exact ⇑(self.π' (n + 1)) ⇑(self.δ' n)
• comm_ι (n : ℤ) : (self.ι' n).comp (self.fA n) = (self.fB n).comp (self.ι n)
• comm_π (n : ℤ) : (self.π' n).comp (self.fB n) = (self.fC n).comp (self.π n)
• comm_δ (n : ℤ) : (self.δ' n).comp (self.fC (n + 1)) = (self.fA n).comp (self.δ n)

theorem FiveLemma.LongExactLadder.two_of_three_fC (L : LongExactLadder) (hfA : ∀ (n : ℤ), Function.Bijective ⇑(L.fA n)) (hfB : ∀ (n : ℤ), Function.Bijective ⇑(L.fB n)) (n : ℤ) : Function.Bijective ⇑(L.fC n)

In a long exact ladder, if fA and fB are bijective in every degree, then so is fC in every degree.

theorem FiveLemma.LongExactLadder.two_of_three_fB_inj (L : LongExactLadder) (hfA : ∀ (n : ℤ), Function.Bijective ⇑(L.fA n)) (hfC : ∀ (n : ℤ), Function.Bijective ⇑(L.fC n)) (n : ℤ) : Function.Injective ⇑(L.fB n)

Injectivity half of the 2-out-of-3 principle: if fA and fC are bijective in every degree, then fB is injective in every degree.

theorem FiveLemma.LongExactLadder.two_of_three_fB_surj_aux (L : LongExactLadder) (hfA : ∀ (n : ℤ), Function.Bijective ⇑(L.fA n)) (hfC : ∀ (n : ℤ), Function.Bijective ⇑(L.fC n)) (n : ℤ) : Function.Surjective ⇑(L.fB (n + 1))

Surjectivity half of the 2-out-of-3 principle (shifted form): if fA and fC are bijective in every degree, then fB (n+1) is surjective.

theorem FiveLemma.LongExactLadder.two_of_three_fB (L : LongExactLadder) (hfA : ∀ (n : ℤ), Function.Bijective ⇑(L.fA n)) (hfC : ∀ (n : ℤ), Function.Bijective ⇑(L.fC n)) (n : ℤ) : Function.Bijective ⇑(L.fB n)

In a long exact ladder, if fA and fC are bijective in every degree, then so is fB in every degree (combining the injectivity and surjectivity halves).

theorem FiveLemma.LongExactLadder.two_of_three_fA (L : LongExactLadder) (hfB : ∀ (n : ℤ), Function.Bijective ⇑(L.fB n)) (hfC : ∀ (n : ℤ), Function.Bijective ⇑(L.fC n)) (n : ℤ) : Function.Bijective ⇑(L.fA n)

In a long exact ladder, if fB and fC are bijective in every degree, then so is fA in every degree.

theorem FiveLemma.LongExactLadder.two_of_three_iso (L : LongExactLadder) (h : ((∀ (n : ℤ), Function.Bijective ⇑(L.fA n)) ∧ ∀ (n : ℤ), Function.Bijective ⇑(L.fB n)) ∨ ((∀ (n : ℤ), Function.Bijective ⇑(L.fA n)) ∧ ∀ (n : ℤ), Function.Bijective ⇑(L.fC n)) ∨ (∀ (n : ℤ), Function.Bijective ⇑(L.fB n)) ∧ ∀ (n : ℤ), Function.Bijective ⇑(L.fC n)) : (∀ (n : ℤ), Function.Bijective ⇑(L.fA n)) ∧ (∀ (n : ℤ), Function.Bijective ⇑(L.fB n)) ∧ ∀ (n : ℤ), Function.Bijective ⇑(L.fC n)

Corollary 9.5 (2-out-of-3 for chain maps). For a map of short exact sequences of chain complexes presented as a long exact ladder, if any two of the three vertical maps fA, fB, fC are isomorphisms in homology (bijective in every degree), then so is the third. The same statement underlies Proposition 9.6 for a map of pairs.

theorem FiveLemma.HomologyLadder.two_of_three_bijective (L : HomologyLadder) : ((∀ (n : ℤ), Function.Bijective ⇑(L.fMap n)) → (∀ (n : ℤ), Function.Bijective ⇑(L.gMap n)) → ∀ (n : ℤ), Function.Bijective ⇑(L.hMap n)) ∧ ((∀ (n : ℤ), Function.Bijective ⇑(L.fMap n)) → (∀ (n : ℤ), Function.Bijective ⇑(L.hMap n)) → ∀ (n : ℤ), Function.Bijective ⇑(L.gMap n)) ∧ ((∀ (n : ℤ), Function.Bijective ⇑(L.gMap n)) → (∀ (n : ℤ), Function.Bijective ⇑(L.hMap n)) → ∀ (n : ℤ), Function.Bijective ⇑(L.fMap n))

2-out-of-3 principle packaged for HomologyLadder: the three implications among {fMap, gMap, hMap} saying that bijectivity of any two of the three vertical maps forces bijectivity of the third.

def EilenbergSteenrod.MapOfPairs.toSpaceMap {P : TopPair} {Q : TopPair} (f : MapOfPairs P Q) : MapOfPairs (TopPair.ofSpace P.space) (TopPair.ofSpace Q.space)

Forgetting the subspace data: a map of pairs (X, A) → (Y, B) induces a map between the trivial pairs (X, ∅) → (Y, ∅). Used in the Eilenberg–Steenrod packaging.