The exactness, additivity and dimension axioms for homology pretheories

Mathlib's TopPair.HomologyPretheory bundles relative homology functors Hₚ i, absolute homology functors H i, their comparison on pairs (X, ∅) and boundary morphisms δ i j : Hₚ i ⟶ proj₂ ⋙ H j, and states homotopy invariance as the class HomologyPretheory.IsHomotopyInvariant. This file adds three further Eilenberg--Steenrod axioms as classes on a homology pretheory:

• HomologyPretheory.HasPairSequence: for every topological pair (X, A) the sequence ⋯ ⟶ Hᵢ(A) ⟶ Hᵢ(X) ⟶ Hᵢ(X, A) ⟶ Hⱼ(A) ⟶ Hⱼ(X) ⟶ ⋯ (for c.Rel i j) is exact, and the map Hᵢ(X) ⟶ Hᵢ(X, A) is an epimorphism when i has no successor in the complex shape.
• HomologyPretheory.IsAdditive: every absolute homology functor H i preserves coproducts of families of spaces, so the homology of a disjoint union is the coproduct of the homologies of its summands, with the maps induced by the inclusions of the summands as the coprojections.
• HomologyPretheory.HasDimensionAxiom: for the complex shape ComplexShape.down ℕ, the homology of a point vanishes in every positive degree.

The map Hᵢ(X) ⟶ Hᵢ(X, A) of the pair sequence is HomologyPretheory.hFstToHₚ, the comparison H i ≅ incl ⋙ Hₚ i followed by the map induced by the pair map (X, ∅) ⟶ (X, A).

References

• S. Eilenberg and N. Steenrod, Foundations of Algebraic Topology, Chapter I.
• J. Scharmberg, mathlib4#38369: hFstToHₚ, HasPairSequence, IsAdditive and HasDimensionAxiom are adapted from this formalization.

def TopPair.HomologyPretheory.hFstToHₚ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (HP : HomologyPretheory C c) (i : ι) (X : TopPair) : (HP.H i).obj fst ⟶ (HP.Hₚ i).obj X

The map H i X.fst ⟶ Hₚ i X from the homology of the ambient space of a pair to the relative homology of the pair, induced by the pair map (X.fst, ∅) ⟶ X.

Equations

• HP.hFstToHₚ i X = CategoryTheory.CategoryStruct.comp ((HP.iso i).hom.app TopPair.fst) ((HP.Hₚ i).map X.j)

theorem TopPair.HomologyPretheory.hFstToHₚ_def {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (HP : HomologyPretheory C c) (i : ι) (X : TopPair) : HP.hFstToHₚ i X = CategoryTheory.CategoryStruct.comp ((HP.iso i).hom.app fst) ((HP.Hₚ i).map X.j)

The ambient-to-relative map is the comparison on (X.fst, ∅) followed by the map induced by the pair inclusion (X.fst, ∅) ⟶ X.

class TopPair.HomologyPretheory.HasPairSequence {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (HP : HomologyPretheory C c) : Prop

A homology pretheory has the long exact sequence of topological pairs ⋯ ⟶ H i X.snd ⟶ H i X.fst ⟶ Hₚ i X ⟶ H j X.snd ⟶ H j X.fst ⟶ ⋯ for c.Rel i j.

• exact_pair (X : TopPair) (i j : ι) (hij : c.Rel i j) : (CategoryTheory.ComposableArrows.mk₂ (HP.hFstToHₚ i X) ((HP.δ i j).app X)).Exact

  Exactness of the sequence H i X.fst ⟶ Hₚ i X ⟶ H j X.snd.

• exact_snd (X : TopPair) (i j : ι) (hij : c.Rel i j) : (CategoryTheory.ComposableArrows.mk₂ ((HP.δ i j).app X) ((HP.H j).map map)).Exact

  Exactness of the sequence Hₚ i X ⟶ H j X.snd ⟶ H j X.fst.

• exact_fst (X : TopPair) (i : ι) : (CategoryTheory.ComposableArrows.mk₂ ((HP.H i).map map) (HP.hFstToHₚ i X)).Exact

  Exactness of the sequence H i X.snd ⟶ H i X.fst ⟶ Hₚ i X.

• epi_map_of_not_rel (X : TopPair) (i : ι) (hi : ∀ (j : ι), ¬c.Rel i j) : CategoryTheory.Epi ((HP.Hₚ i).map X.j)

  The map on relative homology induced by the pair inclusion (X.fst, ∅) ⟶ X is an epimorphism when i has no successor in the complex shape, where the long exact sequence ends. Composing it with HP.iso gives the epimorphism HP.hFstToHₚ i X.

class TopPair.HomologyPretheory.IsAdditive {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (HP : HomologyPretheory C c) : Prop

A homology pretheory is additive if each of its absolute homology functors preserves coproducts of families of spaces indexed by a type in the universe of the spaces.

• preservesColimitsOfShape_discrete (J : Type u) (i : ι) : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (HP.H i)

  The absolute homology functor H i preserves coproducts indexed by J.

class TopPair.HomologyPretheory.HasDimensionAxiom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (HP : HomologyPretheory C (ComplexShape.down ℕ)) : Prop

A homology pretheory indexed by ComplexShape.down ℕ has the dimension axiom if the homology of a point vanishes in every positive degree.

• isZero_PUnit_of_gt_zero (n : ℕ) (hn : n ≠ 0) : CategoryTheory.Limits.IsZero ((HP.H n).obj ↧PUnit.{u + 1})