Eilenberg-Steenrod homology theories

In this file we introduce the Eilenberg-Steenrod axioms for homology theories.

The data for a homology theory is bundled in a structure HomologyPretheory consisting of functors Hₚ i : TopPair ⥤ C and H i : TopCat ⥤ C which represent the ith relative and regular homology, respectively, (indexed by a ComplexShape) and a proof that they agree on TopCat. They also require boundary morphisms δ i j : Hₚ i ⟶ proj₂ ⋙ H j for the long exact sequence of topological pairs. These are nonzero only if c.Rel i j.

We introduce a type class for each axiom:

• IsHomotopyInvariant: Homotopic maps induce the same map in homology.
• HasExcisionIso: For a sufficiently nice subset U ⊆ A, the inclusion (X \ U, A \ U) → (X, A) induces an isomorphism in homology.
• IsAdditive: Homology preserves coproducts.
• HasPairSequence: For a topological pair (X, A), the sequence ⋯ ⟶ H i X ⟶ H i (X, A) ⟶ H (i - 1) A ⟶ H (i - 1) X ⟶ H (i - 1) (X, A) ⟶ ⋯ is exact.
• HasDimensionAxiom: A HomologyPretheory on ComplexShape.down ℕ : ComplexShape ℕ has the dimension axiom, if homology is zero for positive indices.

In addition, there are bundled type classes IsExtraordinaryEilenbergSteenrod with the homotopy-invariance, excision, additivity, and pair sequence axioms and IsEilenbergSteenrod which extends the former by the dimension axiom.

structure TopPair.HomologyPretheory (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) : Type (max (max (max (u + 1) u_1) u_2) v_1)

A HomologyPretheory is the data of an Eilenberg-Steenrod homology theory.

• Hₚ (i : ι) : CategoryTheory.Functor TopPair C

  The relative homology functor of a HomologyPretheory.

• H (i : ι) : CategoryTheory.Functor TopCat C

  The regular homology functor of a HomologyPretheory.

• iso (i : ι) : self.H i ≅ incl.comp (self.Hₚ i)

  Hₚ and H agree on TopCat.

• δ (i j : ι) : self.Hₚ i ⟶ proj₂.comp (self.H j)

  The boundary natural transformation of a HomologyPretheory.

• shape_δ (i j : ι) (h : ¬c.Rel i j) : self.δ i j = 0

  The boundary map is only nonzero if c.Rel i j.

theorem TopPair.HomologyPretheory.ext {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} {ι : Type u_2} {c : ComplexShape ι} {x y : HomologyPretheory C c} (Hₚ : x.Hₚ = y.Hₚ) (H : x.H = y.H) (iso : x.iso ≍ y.iso) (δ : x.δ ≍ y.δ) : x = y

theorem TopPair.HomologyPretheory.ext_iff {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} {ι : Type u_2} {c : ComplexShape ι} {x y : HomologyPretheory C c} : x = y ↔ x.Hₚ = y.Hₚ ∧ x.H = y.H ∧ x.iso ≍ y.iso ∧ x.δ ≍ y.δ

structure TopPair.HomologyPretheory.Hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (HP HP' : HomologyPretheory C c) : Type (max (max (u + 1) u_2) v_1)

A morphism in the category HomologyPretheory.

• homₚ (i : ι) : HP.Hₚ i ⟶ HP'.Hₚ i

  The natural transformation of relative homology functors in a morphism of HomologyPretheorys.

• hom (i : ι) : HP.H i ⟶ HP'.H i

  The natural transformation of homology functors in a morphism of HomologyPretheorys.

• iso_comm (i : ι) : CategoryTheory.CategoryStruct.comp (HP.iso i).hom (incl.whiskerLeft (self.homₚ i)) = CategoryTheory.CategoryStruct.comp (self.hom i) (HP'.iso i).hom

  homₚ and hom need to be compatible with HomologyPretheory.iso.

• w (i j : ι) : CategoryTheory.CategoryStruct.comp (HP.δ i j) (proj₂.whiskerLeft (self.hom j)) = CategoryTheory.CategoryStruct.comp (self.homₚ i) (HP'.δ i j)

  homₚ needs to be compatible with the boundary maps.

theorem TopPair.HomologyPretheory.Hom.ext {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} {x y : HP.Hom HP'} (homₚ : x.homₚ = y.homₚ) (hom : x.hom = y.hom) : x = y

theorem TopPair.HomologyPretheory.Hom.ext_iff {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} {x y : HP.Hom HP'} : x = y ↔ x.homₚ = y.homₚ ∧ x.hom = y.hom

@[simp]

theorem TopPair.HomologyPretheory.Hom.iso_comm_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (self : HP.Hom HP') (i : ι) {Z : CategoryTheory.Functor TopCat C} (h : incl.comp (HP'.Hₚ i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HP.iso i).hom (CategoryTheory.CategoryStruct.comp (incl.whiskerLeft (self.homₚ i)) h) = CategoryTheory.CategoryStruct.comp (self.hom i) (CategoryTheory.CategoryStruct.comp (HP'.iso i).hom h)

homₚ and hom need to be compatible with HomologyPretheory.iso.

theorem TopPair.HomologyPretheory.Hom.w_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (self : HP.Hom HP') (i j : ι) {Z : CategoryTheory.Functor TopPair C} (h : proj₂.comp (HP'.H j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HP.δ i j) (CategoryTheory.CategoryStruct.comp (proj₂.whiskerLeft (self.hom j)) h) = CategoryTheory.CategoryStruct.comp (self.homₚ i) (CategoryTheory.CategoryStruct.comp (HP'.δ i j) h)

homₚ needs to be compatible with the boundary maps.

@[instance_reducible]

instance TopPair.HomologyPretheory.instCategory {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} : CategoryTheory.Category.{max (max (u + 1) u_2) v_1, max (max (max (u + 1) u_2) u_1) v_1} (HomologyPretheory C c)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopPair.HomologyPretheory.id_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (x✝ : HomologyPretheory C c) (i : ι) : (CategoryTheory.CategoryStruct.id x✝).hom i = CategoryTheory.CategoryStruct.comp (x✝.iso i).hom (CategoryTheory.CategoryStruct.comp (incl.whiskerLeft ((fun (x : ι) => CategoryTheory.CategoryStruct.id (x✝.Hₚ x)) i)) (x✝.iso i).inv)

@[simp]

theorem TopPair.HomologyPretheory.id_homₚ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (x✝ : HomologyPretheory C c) (x✝¹ : ι) : (CategoryTheory.CategoryStruct.id x✝).homₚ x✝¹ = CategoryTheory.CategoryStruct.id (x✝.Hₚ x✝¹)

@[simp]

theorem TopPair.HomologyPretheory.comp_homₚ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {X✝ Y✝ Z✝ : HomologyPretheory C c} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (x✝ : ι) : (CategoryTheory.CategoryStruct.comp f g).homₚ x✝ = CategoryTheory.CategoryStruct.comp (f.homₚ x✝) (g.homₚ x✝)

@[simp]

theorem TopPair.HomologyPretheory.comp_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {X✝ Y✝ Z✝ : HomologyPretheory C c} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (i : ι) : (CategoryTheory.CategoryStruct.comp f g).hom i = CategoryTheory.CategoryStruct.comp (X✝.iso i).hom (CategoryTheory.CategoryStruct.comp (incl.whiskerLeft ((fun (x : ι) => CategoryTheory.CategoryStruct.comp (f.homₚ x) (g.homₚ x)) i)) (Z✝.iso i).inv)

theorem TopPair.HomologyPretheory.Hom.iso_comm_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (f : HP ⟶ HP') (i : ι) (X : TopCat) : CategoryTheory.CategoryStruct.comp ((HP.iso i).hom.app X) ((f.homₚ i).app (ofTopCat X)) = CategoryTheory.CategoryStruct.comp ((f.hom i).app X) ((HP'.iso i).hom.app X)

theorem TopPair.HomologyPretheory.Hom.iso_comm_app_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (f : HP ⟶ HP') (i : ι) (X : TopCat) {Z : C} (h : (HP'.Hₚ i).obj (ofTopCat X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((HP.iso i).hom.app X) (CategoryTheory.CategoryStruct.comp ((f.homₚ i).app (ofTopCat X)) h) = CategoryTheory.CategoryStruct.comp ((f.hom i).app X) (CategoryTheory.CategoryStruct.comp ((HP'.iso i).hom.app X) h)

theorem TopPair.HomologyPretheory.Hom.w_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (f : HP ⟶ HP') (i j : ι) (X : TopPair) : CategoryTheory.CategoryStruct.comp ((HP.δ i j).app X) ((f.hom j).app X.left) = CategoryTheory.CategoryStruct.comp ((f.homₚ i).app X) ((HP'.δ i j).app X)

theorem TopPair.HomologyPretheory.Hom.w_app_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (f : HP ⟶ HP') (i j : ι) (X : TopPair) {Z : C} (h : (HP'.H j).obj X.left ⟶ Z) : CategoryTheory.CategoryStruct.comp ((HP.δ i j).app X) (CategoryTheory.CategoryStruct.comp ((f.hom j).app X.left) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((f.homₚ i).app X) ((HP'.δ i j).app X)) h

theorem TopPair.HomologyPretheory.iso_homₚ_inv_hom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (f : HP ⟶ HP') (i : ι) : CategoryTheory.CategoryStruct.comp (HP.iso i).hom (CategoryTheory.CategoryStruct.comp (incl.whiskerLeft (f.homₚ i)) (HP'.iso i).inv) = f.hom i

theorem TopPair.HomologyPretheory.iso_homₚ_inv_hom_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (f : HP ⟶ HP') (i : ι) {Z : CategoryTheory.Functor TopCat C} (h : HP'.H i ⟶ Z) : CategoryTheory.CategoryStruct.comp (HP.iso i).hom (CategoryTheory.CategoryStruct.comp (incl.whiskerLeft (f.homₚ i)) (CategoryTheory.CategoryStruct.comp (HP'.iso i).inv h)) = CategoryTheory.CategoryStruct.comp (f.hom i) h

@[simp]

theorem TopPair.HomologyPretheory.iso_homₚ_inv_hom_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (f : HP ⟶ HP') (i : ι) (X : TopCat) : CategoryTheory.CategoryStruct.comp ((HP.iso i).hom.app X) (CategoryTheory.CategoryStruct.comp ((f.homₚ i).app (ofTopCat X)) ((HP'.iso i).inv.app X)) = (f.hom i).app X

@[simp]

theorem TopPair.HomologyPretheory.iso_homₚ_inv_hom_app_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (f : HP ⟶ HP') (i : ι) (X : TopCat) {Z : C} (h : (HP'.H i).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((HP.iso i).hom.app X) (CategoryTheory.CategoryStruct.comp ((f.homₚ i).app (ofTopCat X)) (CategoryTheory.CategoryStruct.comp ((HP'.iso i).inv.app X) h)) = CategoryTheory.CategoryStruct.comp ((f.hom i).app X) h

@[simp]

theorem TopPair.HomologyPretheory.inv_hom_iso_homₚ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (f : HP ⟶ HP') (i : ι) : CategoryTheory.CategoryStruct.comp (HP.iso i).inv (CategoryTheory.CategoryStruct.comp (f.hom i) (HP'.iso i).hom) = incl.whiskerLeft (f.homₚ i)

@[simp]

theorem TopPair.HomologyPretheory.inv_hom_iso_homₚ_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (f : HP ⟶ HP') (i : ι) {Z : CategoryTheory.Functor TopCat C} (h : incl.comp (HP'.Hₚ i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HP.iso i).inv (CategoryTheory.CategoryStruct.comp (f.hom i) (CategoryTheory.CategoryStruct.comp (HP'.iso i).hom h)) = CategoryTheory.CategoryStruct.comp (incl.whiskerLeft (f.homₚ i)) h

@[simp]

theorem TopPair.HomologyPretheory.inv_hom_iso_homₚ_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (f : HP ⟶ HP') (i : ι) (X : TopCat) : CategoryTheory.CategoryStruct.comp ((HP.iso i).inv.app X) (CategoryTheory.CategoryStruct.comp ((f.hom i).app X) ((HP'.iso i).hom.app X)) = (f.homₚ i).app (ofTopCat X)

@[simp]

theorem TopPair.HomologyPretheory.inv_hom_iso_homₚ_app_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (f : HP ⟶ HP') (i : ι) (X : TopCat) {Z : C} (h : (HP'.Hₚ i).obj (incl.obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((HP.iso i).inv.app X) (CategoryTheory.CategoryStruct.comp ((f.hom i).app X) (CategoryTheory.CategoryStruct.comp ((HP'.iso i).hom.app X) h)) = CategoryTheory.CategoryStruct.comp ((f.homₚ i).app (ofTopCat X)) h

@[reducible, inline]

abbrev 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 induced by the inclusion.

Equations

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

@[implicit_reducible]

def TopPair.HomologyPretheory.hₚFunctor {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (i : ι) : CategoryTheory.Functor (HomologyPretheory C c) (CategoryTheory.Functor TopPair C)

The forgetful functor that sends a HomologyPretheory to it's relative homology functor Hₚ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopPair.HomologyPretheory.hₚFunctor_obj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (i : ι) (HP : HomologyPretheory C c) : (hₚFunctor i).obj HP = HP.Hₚ i

@[simp]

theorem TopPair.HomologyPretheory.hₚFunctor_map {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (i : ι) {X✝ Y✝ : HomologyPretheory C c} (f : X✝ ⟶ Y✝) : (hₚFunctor i).map f = f.homₚ i

instance TopPair.HomologyPretheory.instIsIsoFunctorHomₚ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (f : HP ⟶ HP') [CategoryTheory.IsIso f] (i : ι) : CategoryTheory.IsIso (f.homₚ i)

@[reducible, inline]

abbrev TopPair.HomologyPretheory.hₚIsoOfIso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (e : HP ≅ HP') (i : ι) : HP.Hₚ i ≅ HP'.Hₚ i

The isomorphism of relative homology that is part of an isomorphism of HomologyPretheorys.

Equations

• TopPair.HomologyPretheory.hₚIsoOfIso e i = (TopPair.HomologyPretheory.hₚFunctor i).mapIso e

@[implicit_reducible]

def TopPair.HomologyPretheory.hFunctor {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (i : ι) : CategoryTheory.Functor (HomologyPretheory C c) (CategoryTheory.Functor TopCat C)

The forgetful functor that sends a HomologyPretheory to it's homology functor H.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopPair.HomologyPretheory.hFunctor_obj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (i : ι) (HP : HomologyPretheory C c) : (hFunctor i).obj HP = HP.H i

@[simp]

theorem TopPair.HomologyPretheory.hFunctor_map {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (i : ι) {X✝ Y✝ : HomologyPretheory C c} (f : X✝ ⟶ Y✝) : (hFunctor i).map f = f.hom i

instance TopPair.HomologyPretheory.instIsIsoFunctorTopCatHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (f : HP ⟶ HP') [CategoryTheory.IsIso f] (i : ι) : CategoryTheory.IsIso (f.hom i)

@[reducible, inline]

abbrev TopPair.HomologyPretheory.hIsoOfIso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} {HP HP' : HomologyPretheory C c} (e : HP ≅ HP') (i : ι) : HP.H i ≅ HP'.H i

The isomorphism of absolute homology that is part of an isomorphism of HomologyPretheorys.

Equations

• TopPair.HomologyPretheory.hIsoOfIso e i = HP.iso i ≪≫ TopPair.incl.isoWhiskerLeft ((TopPair.HomologyPretheory.hₚFunctor i).mapIso e) ≪≫ (HP'.iso i).symm

class TopPair.HomologyPretheory.IsHomotopyInvariant {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 HomologyPretheory is homotopy-invariant if its homology functor Hₚ takes homotopic maps to the same map in homology

• map_eq_of_homotopy {X Y : TopPair} {f g : X ⟶ Y} (F : Homotopy f g) (i : ι) : (HP.Hₚ i).map f = (HP.Hₚ i).map g

@[reducible, inline]

abbrev TopPair.HomologyPretheory.isHomotopyInvariant (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) : CategoryTheory.ObjectProperty (HomologyPretheory C c)

An abbreviation for HomologyPretheory.IsHomotopyInvariant as ObjectProperty.

Equations

• TopPair.HomologyPretheory.isHomotopyInvariant C c = TopPair.HomologyPretheory.IsHomotopyInvariant

@[simp]

theorem TopPair.HomologyPretheory.isHomotopyInvariant_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (HP : HomologyPretheory C c) : isHomotopyInvariant C c HP ↔ HP.IsHomotopyInvariant

instance TopPair.HomologyPretheory.instIsClosedUnderIsomorphismsIsHomotopyInvariant {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} : (isHomotopyInvariant C c).IsClosedUnderIsomorphisms

class TopPair.HomologyPretheory.HasExcisionIso {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 HomologyPretheory has the excision-isomorphism, if cutting out a sufficiently nice subspace U from a space X yields an isomorphism Hₚ i X ≅ Hₚ i (X \ U).

• isIso_of_isExcisive ⦃X V : TopPair⦄ (g : V ⟶ X) [IsExcisive g] (i : ι) : CategoryTheory.IsIso ((HP.Hₚ i).map g)

theorem TopPair.HomologyPretheory.hasExcisionIso_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (HP : HomologyPretheory C c) : HP.HasExcisionIso ↔ autoParam (∀ ⦃X V : TopPair⦄ (g : V ⟶ X) [IsExcisive g] (i : ι), CategoryTheory.IsIso ((HP.Hₚ i).map g)) HasExcisionIso.isIso_of_isExcisive._autoParam

@[reducible, inline]

abbrev TopPair.HomologyPretheory.hasExcisionIso (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) : CategoryTheory.ObjectProperty (HomologyPretheory C c)

An abbreviation for HomologyPretheory.HasExcisionIso as ObjectProperty.

Equations

• TopPair.HomologyPretheory.hasExcisionIso C c = TopPair.HomologyPretheory.HasExcisionIso

@[simp]

theorem TopPair.HomologyPretheory.hasExcisionIso_iff' {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (HP : HomologyPretheory C c) : hasExcisionIso C c HP ↔ HP.HasExcisionIso

instance TopPair.HomologyPretheory.instIsClosedUnderIsomorphismsHasExcisionIso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} : (hasExcisionIso C c).IsClosedUnderIsomorphisms

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 HomologyPretheory is additive if its homology functor preserves coproducts.

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

@[reducible, inline]

abbrev TopPair.HomologyPretheory.isAdditive (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) : CategoryTheory.ObjectProperty (HomologyPretheory C c)

An abbreviation for HomologyPretheory.IsAdditive as ObjectProperty.

Equations

• TopPair.HomologyPretheory.isAdditive C c = TopPair.HomologyPretheory.IsAdditive

@[simp]

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

instance TopPair.HomologyPretheory.IsAdditive.preserves_coproducts_of_small {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (HP : HomologyPretheory C c) [HP.IsAdditive] (J : Type u_3) [Small.{u, u_3} J] (i : ι) : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (HP.H i)

instance TopPair.HomologyPretheory.instIsClosedUnderIsomorphismsIsAdditive {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} : (isAdditive C c).IsClosedUnderIsomorphisms

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

This imposes that a HomologyPretheory has the long exact sequence of topological pairs ⋯ ⟶ H (c.next i) X.fst ⟶ Hₚ (c.next i) X) ⟶ H i X.snd ⟶ H i X.fst ⟶ ⋯.

• exact_pair (X : TopPair) (i j : ι) (hij : c.Rel i j) : (CategoryTheory.ComposableArrows.mk₂ (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) (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 boundary map out of homology with final index (i.e. an index with no successors in the ComplexShape) is an epi.

@[reducible, inline]

abbrev TopPair.HomologyPretheory.hasPairSequence (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) : CategoryTheory.ObjectProperty (HomologyPretheory C c)

An abbreviation for HomologyPretheory.HasPairSequence as ObjectProperty.

Equations

• TopPair.HomologyPretheory.hasPairSequence C c = TopPair.HomologyPretheory.HasPairSequence

@[simp]

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

instance TopPair.HomologyPretheory.instIsClosedUnderIsomorphismsHasPairSequence {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} : (hasPairSequence C c).IsClosedUnderIsomorphisms

class TopPair.HomologyPretheory.IsExtraordinaryEilenbergSteenrod {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

An extraordinary Eilenberg-Steenrod homology theory requires the homotopy, excision, additivity, and exactness axioms.

• isHomotopyInvariant : HP.IsHomotopyInvariant

  Invariance of an extraordinary Eilenberg-Steenrod homology theory on homotopic maps.

• hasExcisionIso : HP.HasExcisionIso

  Excision axiom of an extraordinary Eilenberg-Steenrod homology theory.

• isAdditive : HP.IsAdditive

  An extraordinary Eilenberg-Steenrod homology functor preserves coproducts.

• hasPairSequence : HP.HasPairSequence

  The long exact sequence of topological pairs in an extraordinary Eilenberg-Steenrod homology theory.

@[reducible, inline]

abbrev TopPair.HomologyPretheory.isExtraordinaryEilenbergSteenrod (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} (c : ComplexShape ι) : CategoryTheory.ObjectProperty (HomologyPretheory C c)

An abbreviation for HomologyPretheory.IsExtraordinaryEilenbergSteenrod as ObjectProperty.

Equations

• TopPair.HomologyPretheory.isExtraordinaryEilenbergSteenrod C c = TopPair.HomologyPretheory.IsExtraordinaryEilenbergSteenrod

@[simp]

theorem TopPair.HomologyPretheory.isExtraordinaryEilenbergSteenrod_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} (HP : HomologyPretheory C c) : isExtraordinaryEilenbergSteenrod C c HP ↔ HP.IsExtraordinaryEilenbergSteenrod

instance TopPair.HomologyPretheory.instIsClosedUnderIsomorphismsIsExtraordinaryEilenbergSteenrod {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_2} {c : ComplexShape ι} : (isExtraordinaryEilenbergSteenrod C c).IsClosedUnderIsomorphisms

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 HomologyPretheory on ComplexShape.down ℕ has the dimension axiom if it is trivial on the terminal space for n > 0.

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

@[reducible, inline]

abbrev TopPair.HomologyPretheory.hasDimensionAxiom (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.ObjectProperty (HomologyPretheory C (ComplexShape.down ℕ))

An abbreviation for HomologyPretheory.HasDimensionAxiom as ObjectProperty.

Equations

• TopPair.HomologyPretheory.hasDimensionAxiom C = TopPair.HomologyPretheory.HasDimensionAxiom

@[simp]

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

instance TopPair.HomologyPretheory.instIsClosedUnderIsomorphismsNatDownHasDimensionAxiom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : (hasDimensionAxiom C).IsClosedUnderIsomorphisms

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

An Eilenberg-Steenrod homology theory is an extraordinary Eilenberg-Steenrod homology theory which additionally satisfies the dimension axiom.

• isHomotopyInvariant : HP.IsHomotopyInvariant
• hasExcisionIso : HP.HasExcisionIso
• isAdditive : HP.IsAdditive
• hasPairSequence : HP.HasPairSequence
• hasDimensionAxiom : HP.HasDimensionAxiom

  An Eilenberg-Steenrod homology theory is trivial on the terminal space for n > 0.

@[reducible, inline]

abbrev TopPair.HomologyPretheory.isEilenbergSteenrod (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.ObjectProperty (HomologyPretheory C (ComplexShape.down ℕ))

An abbreviation for HomologyPretheory.IsEilenbergSteenrod as ObjectProperty.

Equations

• TopPair.HomologyPretheory.isEilenbergSteenrod C = TopPair.HomologyPretheory.IsEilenbergSteenrod

@[simp]

theorem TopPair.HomologyPretheory.isEilenbergSteenrod_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (HP : HomologyPretheory C (ComplexShape.down ℕ)) : isEilenbergSteenrod C HP ↔ HP.IsEilenbergSteenrod

instance TopPair.HomologyPretheory.instIsClosedUnderIsomorphismsNatDownIsEilenbergSteenrod {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : (isEilenbergSteenrod C).IsClosedUnderIsomorphisms