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 typeclass IsHomotopyInvariant for the first 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.

@[implicit_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.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)

@[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.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✝¹)

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 (CategoryTheory.CategoryStruct.comp ((f.hom i).app X) ((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 : (incl.comp (HP'.Hₚ i)).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

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_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✝) : (HomologyPretheory.hₚFunctor i).map f = f.homₚ i

@[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) : (HomologyPretheory.hₚFunctor i).obj HP = HP.Hₚ 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)

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_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✝) : (HomologyPretheory.hFunctor i).map f = f.hom i

@[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) : (HomologyPretheory.hFunctor i).obj HP = HP.H 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)

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