From d5f60e5d24e5ed8158151e267456dc04e9fc26af Mon Sep 17 00:00:00 2001
From: Jacob Scharmberg <hi@jacobscharmberg.net>
Date: Tue, 12 May 2026 10:34:30 +0200
Subject: [PATCH 01/12] add `TopPair.HomologyPretheory` and
 `EilenbergSteenrod.IsHomotopyInvariant`

---
 Mathlib.lean                                  |   1 +
 .../AlgebraicTopology/EilenbergSteenrod.lean  | 159 ++++++++++++++++++
 2 files changed, 160 insertions(+)
 create mode 100644 Mathlib/AlgebraicTopology/EilenbergSteenrod.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 28ac19389e07c9..73827cf449a143 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1468,6 +1468,7 @@ public import Mathlib.AlgebraicTopology.DoldKan.Notations
 public import Mathlib.AlgebraicTopology.DoldKan.PInfty
 public import Mathlib.AlgebraicTopology.DoldKan.Projections
 public import Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
+public import Mathlib.AlgebraicTopology.EilenbergSteenrod
 public import Mathlib.AlgebraicTopology.ExtraDegeneracy
 public import Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
 public import Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup
diff --git a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
new file mode 100644
index 00000000000000..5756f85ed349a3
--- /dev/null
+++ b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
@@ -0,0 +1,159 @@
+/-
+Copyright (c) 2026 Jakob Scharmberg. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jakob Scharmberg
+-/
+
+module
+
+public import Mathlib.Algebra.Homology.ComplexShape
+public import Mathlib.Combinatorics.Quiver.ReflQuiver
+public import Mathlib.Topology.Category.TopPair
+/-!
+# 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 `i`th 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`.
+
+TODO: We introduce a type class for each axiom. In addition, there are bundled type classes
+`IsExtraordinaryEilenbergSteenrod` with the homotopy, excision, additivity, and exactness axioms and
+`IsEilenbergSteenrod` on a `HomologyPretheory` on `ComplexShape.down ℕ : ComplexShape ℕ` which
+extends the former by the dimension axiom.
+
+TODO: Excision is formulated in terms of complements of topological pairs: Suppose `U` and `V` are
+complements of a topological pair `X` with embeddings `f : U ⟶ X` and `g : V ⟶ X`. Suppose further
+that the closure of `Hom.fst f (U.fst)` is a subset of the interior of the image of `X.snd` in
+`X.fst`. Then the excision axiom postulates that the homology of `X` is isomorphic to that of `V`.
+Note that this closure condition a priori seems weaker than in the literature. However, we prove
+that under these assumptions, `U` is actually an isomorphism.
+-/
+
+@[expose] public section
+
+open CategoryTheory TopPair ObjectProperty
+
+universe u v
+
+namespace TopPair
+
+/-- A `HomologyPretheory` is the data of an Eilenberg-Steenrod homology theory. -/
+@[ext]
+structure HomologyPretheory
+    (C : Type v) [Category C] [Limits.HasZeroMorphisms C] {ι : Type*} (c : ComplexShape ι) where
+  /-- The relative homology functor of a `HomologyPretheory`. -/
+  Hₚ (i : ι) : TopPair.{u} ⥤ C
+  /-- The regular homology functor of a `HomologyPretheory`. -/
+  H (i : ι) : TopCat.{u} ⥤ C
+  /-- The proof that `Hₚ` and `H` agree on `TopCat` -/
+  iso (i : ι) : H i ≅ incl ⋙ Hₚ i
+  /-- The boundary natural transformation of a `HomologyPretheory`. -/
+  δ (i j : ι) : (Hₚ i) ⟶ proj₂ ⋙ H j
+  /-- The boundary map is only nonzero if `c.Rel i j`. -/
+  shape_δ (i j : ι) (h : ¬ c.Rel i j) : δ i j = 0 := by cat_disch
+
+namespace HomologyPretheory
+
+variable {C : Type v} [Category C] [Limits.HasZeroMorphisms C] {ι : Type*} {c : ComplexShape ι}
+
+/-- A morphism in the category `HomologyPretheory`. -/
+@[ext]
+structure Hom (HP HP' : HomologyPretheory C c) where
+  /-- The natural transformation of relative homology functors in a morphism of
+  `HomologyPretheory`s. -/
+  homₚ (i : ι) : HP.Hₚ i ⟶ HP'.Hₚ i
+  /-- The natural transformation of homology functors in a morphism of
+  `HomologyPretheory`s. -/
+  hom (i : ι) : HP.H i ⟶ HP'.H i := (HP.iso i).hom ≫ incl.whiskerLeft (homₚ i) ≫ (HP'.iso i).inv
+  /-- `homₚ` and `hom` need to be compatible with `HomologyPretheory.iso`. -/
+  iso_comm (i : ι) :
+    (HP.iso i).hom ≫ incl.whiskerLeft (homₚ i) = hom i ≫ (HP'.iso i).hom := by cat_disch
+  /-- `homₚ` needs to be compatible with the boundary maps. -/
+  w (i j : ι) : HP.δ i j ≫ proj₂.whiskerLeft (hom j) = homₚ i ≫ HP'.δ i j := by cat_disch
+
+attribute [reassoc (attr := simp)] Hom.iso_comm
+attribute [reassoc (attr := local simp)] Hom.w
+
+variable {HP HP' : HomologyPretheory C c}
+
+@[reassoc]
+lemma Hom.iso_comm_congr_app (f : HP.Hom HP') (i : ι) (X : TopCat.{u}) :
+    dsimp% (HP.iso i).hom.app X ≫ (incl.whiskerLeft (f.homₚ i)).app X =
+    (f.hom i).app X ≫ (HP'.iso i).hom.app X :=
+  congr($(f.iso_comm _).app _)
+
+@[reassoc]
+lemma Hom.w_congr_app (f : HP.Hom HP') (i j : ι) (X : TopPair) :
+    dsimp% (HP.δ i j).app X ≫ (f.hom j).app X.left = (f.homₚ i).app X ≫ (HP'.δ i j).app X :=
+  congr($(f.w _ _).app _)
+
+@[reassoc]
+lemma iso_homₚ_inv_hom (f : HP.Hom HP') (i : ι) :
+    (HP.iso i).hom ≫ incl.whiskerLeft (f.homₚ i) ≫ (HP'.iso i).inv = f.hom i := by simp
+
+@[reassoc (attr := simp)]
+lemma iso_homₚ_inv_hom_congr_app (f : HP.Hom HP') (i : ι) (X : TopCat) :
+    dsimp% (HP.iso i).hom.app X ≫ (f.homₚ i).app (ofTopCat X) ≫ (HP'.iso i).inv.app X =
+    (f.hom i).app X := congr($(iso_homₚ_inv_hom _ _).app _)
+
+@[reassoc (attr := simp)]
+lemma inv_hom_iso_homₚ (f : HP.Hom HP') (i : ι) :
+    (HP.iso i).inv ≫ f.hom i ≫ (HP'.iso i).hom = incl.whiskerLeft (f.homₚ i) :=
+  ((Iso.inv_comp_eq (HP.iso i)).mpr (f.iso_comm i).symm)
+
+@[reassoc (attr := simp)]
+lemma inv_hom_iso_homₚ_congr_app (f : HP.Hom HP') (i : ι) (X : TopCat) :
+    dsimp% (HP.iso i).inv.app X ≫ (f.hom i).app X ≫ (HP'.iso i).hom.app X =
+    (f.homₚ i).app (ofTopCat X) := congr($(inv_hom_iso_homₚ _ _).app _)
+
+@[simps]
+instance : Category (HomologyPretheory C c) where
+  Hom := HomologyPretheory.Hom
+  id _ := { homₚ _ := 𝟙 _ }
+  comp f g := { homₚ _ := f.homₚ _ ≫ g.homₚ _ }
+
+/-- The forgetful functor that sends a `HomologyPretheory` to it's relative homology functor `Hₚ`.
+-/
+@[simps]
+protected def forgetₚ (i : ι) : HomologyPretheory C c ⥤ TopPair.{u} ⥤ C where
+  obj HP := HP.Hₚ i
+  map f := f.homₚ i
+
+/-- The forgetful functor that sends a `HomologyPretheory` to it's homology functor `H`. -/
+@[simps]
+protected def forget (i : ι) : HomologyPretheory C c ⥤ TopCat.{u} ⥤ C where
+  obj HP := HP.H i
+  map f := f.hom i
+
+end HomologyPretheory
+
+end TopPair
+
+namespace EilenbergSteenrod
+
+open HomologyPretheory
+
+variable {C : Type v} [Category C] [Limits.HasZeroMorphisms C] {ι : Type*} {c : ComplexShape ι}
+  (HP HP' : HomologyPretheory.{u} C c)
+
+/-- A `HomologyPretheory` is homotopy-invariant if its homology functor `Hₚ` takes homotopic maps to
+the same map in homology -/
+class IsHomotopyInvariant where
+  homotopy ⦃X Y : TopPair⦄ (f g : X ⟶ Y) (hfg : Homotopic f g) :
+      ∀ (i : ι), (HP.Hₚ i).map f = (HP.Hₚ i).map g := by cat_disch
+
+instance : IsClosedUnderIsomorphisms (C := HomologyPretheory C c) IsHomotopyInvariant where
+  of_iso {HP HP'} e hHP := ⟨by
+    intro _ _ _ _ hfg _
+    have := hHP.homotopy _ _ hfg
+    apply ((((HomologyPretheory.forgetₚ _).mapIso e).app _).cancel_iso_hom_left
+      ((HP'.Hₚ _).map _) ((HP'.Hₚ _).map _)).mp
+    simp only [CategoryTheory.Iso.app_hom, HomologyPretheory.forgetₚ_obj, Functor.mapIso_hom,
+      forgetₚ_map, ← (e.hom.homₚ _).naturality]
+    cat_disch⟩
+
+end EilenbergSteenrod

From 2b7385f0923e7344c37ac8db6ca4d0528f55d4c6 Mon Sep 17 00:00:00 2001
From: quantumsnow <205372035+quantumsnow@users.noreply.github.com>
Date: Tue, 12 May 2026 11:58:51 +0000
Subject: [PATCH 02/12] style fixes
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
---
 Mathlib/AlgebraicTopology/EilenbergSteenrod.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
index 5756f85ed349a3..81ef00102457de 100644
--- a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
+++ b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
@@ -3,12 +3,12 @@ Copyright (c) 2026 Jakob Scharmberg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jakob Scharmberg
 -/
-
 module
 
 public import Mathlib.Algebra.Homology.ComplexShape
 public import Mathlib.Combinatorics.Quiver.ReflQuiver
 public import Mathlib.Topology.Category.TopPair
+
 /-!
 # Eilenberg-Steenrod homology theories
 
@@ -49,10 +49,10 @@ structure HomologyPretheory
   Hₚ (i : ι) : TopPair.{u} ⥤ C
   /-- The regular homology functor of a `HomologyPretheory`. -/
   H (i : ι) : TopCat.{u} ⥤ C
-  /-- The proof that `Hₚ` and `H` agree on `TopCat` -/
+  /-- `Hₚ` and `H` agree on `TopCat` -/
   iso (i : ι) : H i ≅ incl ⋙ Hₚ i
   /-- The boundary natural transformation of a `HomologyPretheory`. -/
-  δ (i j : ι) : (Hₚ i) ⟶ proj₂ ⋙ H j
+  δ (i j : ι) : Hₚ i ⟶ proj₂ ⋙ H j
   /-- The boundary map is only nonzero if `c.Rel i j`. -/
   shape_δ (i j : ι) (h : ¬ c.Rel i j) : δ i j = 0 := by cat_disch
 

From 6da11b4e10597d18cfac4e1790a20fb9c7e38fc0 Mon Sep 17 00:00:00 2001
From: Jacob Scharmberg <hi@jacobscharmberg.net>
Date: Tue, 12 May 2026 14:04:32 +0200
Subject: [PATCH 03/12] shorten module docstring

---
 Mathlib/AlgebraicTopology/EilenbergSteenrod.lean | 12 +-----------
 1 file changed, 1 insertion(+), 11 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
index 5756f85ed349a3..5f84cacee49772 100644
--- a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
+++ b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
@@ -20,17 +20,7 @@ respectively, (indexed by a `ComplexShape`) and a proof that they agree on `TopC
 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`.
 
-TODO: We introduce a type class for each axiom. In addition, there are bundled type classes
-`IsExtraordinaryEilenbergSteenrod` with the homotopy, excision, additivity, and exactness axioms and
-`IsEilenbergSteenrod` on a `HomologyPretheory` on `ComplexShape.down ℕ : ComplexShape ℕ` which
-extends the former by the dimension axiom.
-
-TODO: Excision is formulated in terms of complements of topological pairs: Suppose `U` and `V` are
-complements of a topological pair `X` with embeddings `f : U ⟶ X` and `g : V ⟶ X`. Suppose further
-that the closure of `Hom.fst f (U.fst)` is a subset of the interior of the image of `X.snd` in
-`X.fst`. Then the excision axiom postulates that the homology of `X` is isomorphic to that of `V`.
-Note that this closure condition a priori seems weaker than in the literature. However, we prove
-that under these assumptions, `U` is actually an isomorphism.
+We introduce a typeclass `IsHomotopyInvariant` for the first axiom.
 -/
 
 @[expose] public section

From 9db444977b27fe483888ef915abbe9bf67d059aa Mon Sep 17 00:00:00 2001
From: Jacob Scharmberg <hi@jacobscharmberg.net>
Date: Tue, 12 May 2026 14:08:18 +0200
Subject: [PATCH 04/12] move category instance

---
 .../AlgebraicTopology/EilenbergSteenrod.lean  | 24 +++++++++----------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
index 5f84cacee49772..d8ddd94fc47871 100644
--- a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
+++ b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
@@ -68,44 +68,44 @@ structure Hom (HP HP' : HomologyPretheory C c) where
 attribute [reassoc (attr := simp)] Hom.iso_comm
 attribute [reassoc (attr := local simp)] Hom.w
 
+@[simps]
+instance : Category (HomologyPretheory C c) where
+  Hom := HomologyPretheory.Hom
+  id _ := { homₚ _ := 𝟙 _ }
+  comp f g := { homₚ _ := f.homₚ _ ≫ g.homₚ _ }
+
 variable {HP HP' : HomologyPretheory C c}
 
 @[reassoc]
-lemma Hom.iso_comm_congr_app (f : HP.Hom HP') (i : ι) (X : TopCat.{u}) :
+lemma Hom.iso_comm_congr_app (f : HP ⟶ HP') (i : ι) (X : TopCat.{u}) :
     dsimp% (HP.iso i).hom.app X ≫ (incl.whiskerLeft (f.homₚ i)).app X =
     (f.hom i).app X ≫ (HP'.iso i).hom.app X :=
   congr($(f.iso_comm _).app _)
 
 @[reassoc]
-lemma Hom.w_congr_app (f : HP.Hom HP') (i j : ι) (X : TopPair) :
+lemma Hom.w_congr_app (f : HP ⟶ HP') (i j : ι) (X : TopPair) :
     dsimp% (HP.δ i j).app X ≫ (f.hom j).app X.left = (f.homₚ i).app X ≫ (HP'.δ i j).app X :=
   congr($(f.w _ _).app _)
 
 @[reassoc]
-lemma iso_homₚ_inv_hom (f : HP.Hom HP') (i : ι) :
+lemma iso_homₚ_inv_hom (f : HP ⟶ HP') (i : ι) :
     (HP.iso i).hom ≫ incl.whiskerLeft (f.homₚ i) ≫ (HP'.iso i).inv = f.hom i := by simp
 
 @[reassoc (attr := simp)]
-lemma iso_homₚ_inv_hom_congr_app (f : HP.Hom HP') (i : ι) (X : TopCat) :
+lemma iso_homₚ_inv_hom_congr_app (f : HP ⟶ HP') (i : ι) (X : TopCat) :
     dsimp% (HP.iso i).hom.app X ≫ (f.homₚ i).app (ofTopCat X) ≫ (HP'.iso i).inv.app X =
     (f.hom i).app X := congr($(iso_homₚ_inv_hom _ _).app _)
 
 @[reassoc (attr := simp)]
-lemma inv_hom_iso_homₚ (f : HP.Hom HP') (i : ι) :
+lemma inv_hom_iso_homₚ (f : HP ⟶ HP') (i : ι) :
     (HP.iso i).inv ≫ f.hom i ≫ (HP'.iso i).hom = incl.whiskerLeft (f.homₚ i) :=
   ((Iso.inv_comp_eq (HP.iso i)).mpr (f.iso_comm i).symm)
 
 @[reassoc (attr := simp)]
-lemma inv_hom_iso_homₚ_congr_app (f : HP.Hom HP') (i : ι) (X : TopCat) :
+lemma inv_hom_iso_homₚ_congr_app (f : HP ⟶ HP') (i : ι) (X : TopCat) :
     dsimp% (HP.iso i).inv.app X ≫ (f.hom i).app X ≫ (HP'.iso i).hom.app X =
     (f.homₚ i).app (ofTopCat X) := congr($(inv_hom_iso_homₚ _ _).app _)
 
-@[simps]
-instance : Category (HomologyPretheory C c) where
-  Hom := HomologyPretheory.Hom
-  id _ := { homₚ _ := 𝟙 _ }
-  comp f g := { homₚ _ := f.homₚ _ ≫ g.homₚ _ }
-
 /-- The forgetful functor that sends a `HomologyPretheory` to it's relative homology functor `Hₚ`.
 -/
 @[simps]

From eb457acb141e9050ef6f6aef008392d625f39fce Mon Sep 17 00:00:00 2001
From: Jacob Scharmberg <hi@jacobscharmberg.net>
Date: Tue, 12 May 2026 14:10:12 +0200
Subject: [PATCH 05/12] rename some lemmas

---
 Mathlib/AlgebraicTopology/EilenbergSteenrod.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
index d8ddd94fc47871..6e6c872edc6d10 100644
--- a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
+++ b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
@@ -77,13 +77,13 @@ instance : Category (HomologyPretheory C c) where
 variable {HP HP' : HomologyPretheory C c}
 
 @[reassoc]
-lemma Hom.iso_comm_congr_app (f : HP ⟶ HP') (i : ι) (X : TopCat.{u}) :
+lemma Hom.iso_comm_app (f : HP ⟶ HP') (i : ι) (X : TopCat.{u}) :
     dsimp% (HP.iso i).hom.app X ≫ (incl.whiskerLeft (f.homₚ i)).app X =
     (f.hom i).app X ≫ (HP'.iso i).hom.app X :=
   congr($(f.iso_comm _).app _)
 
 @[reassoc]
-lemma Hom.w_congr_app (f : HP ⟶ HP') (i j : ι) (X : TopPair) :
+lemma Hom.w_app (f : HP ⟶ HP') (i j : ι) (X : TopPair) :
     dsimp% (HP.δ i j).app X ≫ (f.hom j).app X.left = (f.homₚ i).app X ≫ (HP'.δ i j).app X :=
   congr($(f.w _ _).app _)
 
@@ -92,7 +92,7 @@ lemma iso_homₚ_inv_hom (f : HP ⟶ HP') (i : ι) :
     (HP.iso i).hom ≫ incl.whiskerLeft (f.homₚ i) ≫ (HP'.iso i).inv = f.hom i := by simp
 
 @[reassoc (attr := simp)]
-lemma iso_homₚ_inv_hom_congr_app (f : HP ⟶ HP') (i : ι) (X : TopCat) :
+lemma iso_homₚ_inv_hom_app (f : HP ⟶ HP') (i : ι) (X : TopCat) :
     dsimp% (HP.iso i).hom.app X ≫ (f.homₚ i).app (ofTopCat X) ≫ (HP'.iso i).inv.app X =
     (f.hom i).app X := congr($(iso_homₚ_inv_hom _ _).app _)
 
@@ -102,7 +102,7 @@ lemma inv_hom_iso_homₚ (f : HP ⟶ HP') (i : ι) :
   ((Iso.inv_comp_eq (HP.iso i)).mpr (f.iso_comm i).symm)
 
 @[reassoc (attr := simp)]
-lemma inv_hom_iso_homₚ_congr_app (f : HP ⟶ HP') (i : ι) (X : TopCat) :
+lemma inv_hom_iso_homₚ_app (f : HP ⟶ HP') (i : ι) (X : TopCat) :
     dsimp% (HP.iso i).inv.app X ≫ (f.hom i).app X ≫ (HP'.iso i).hom.app X =
     (f.homₚ i).app (ofTopCat X) := congr($(inv_hom_iso_homₚ _ _).app _)
 

From 24f83fd70efe7baff7a9c41bbb632654b41be042 Mon Sep 17 00:00:00 2001
From: Jacob Scharmberg <hi@jacobscharmberg.net>
Date: Tue, 12 May 2026 14:10:58 +0200
Subject: [PATCH 06/12] dsimp statement of `Hom.iso_comm_app`

---
 Mathlib/AlgebraicTopology/EilenbergSteenrod.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
index 6e6c872edc6d10..b262e7123f00bf 100644
--- a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
+++ b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
@@ -78,7 +78,7 @@ variable {HP HP' : HomologyPretheory C c}
 
 @[reassoc]
 lemma Hom.iso_comm_app (f : HP ⟶ HP') (i : ι) (X : TopCat.{u}) :
-    dsimp% (HP.iso i).hom.app X ≫ (incl.whiskerLeft (f.homₚ i)).app X =
+    dsimp% (HP.iso i).hom.app X ≫ (f.homₚ i).app (ofTopCat X) =
     (f.hom i).app X ≫ (HP'.iso i).hom.app X :=
   congr($(f.iso_comm _).app _)
 

From 717942afc0fb43187805e64923dfbea90e0fd9c6 Mon Sep 17 00:00:00 2001
From: Jacob Scharmberg <hi@jacobscharmberg.net>
Date: Tue, 12 May 2026 14:14:37 +0200
Subject: [PATCH 07/12] =?UTF-8?q?add=20`IsIso`=20instance=20on=20`hom?=
 =?UTF-8?q?=E2=82=9A`=20and=20`hom`=20of=20an=20iso=20between=20`HomologyP?=
 =?UTF-8?q?retheory`s.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Mathlib/AlgebraicTopology/EilenbergSteenrod.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
index b262e7123f00bf..f0de307795d1d3 100644
--- a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
+++ b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
@@ -113,12 +113,18 @@ protected def forgetₚ (i : ι) : HomologyPretheory C c ⥤ TopPair.{u} ⥤ C w
   obj HP := HP.Hₚ i
   map f := f.homₚ i
 
+instance (f : HP ⟶ HP') [IsIso f] (i : ι) : IsIso (f.homₚ i) :=
+  inferInstanceAs (IsIso ((HomologyPretheory.forgetₚ i).map f))
+
 /-- The forgetful functor that sends a `HomologyPretheory` to it's homology functor `H`. -/
 @[simps]
 protected def forget (i : ι) : HomologyPretheory C c ⥤ TopCat.{u} ⥤ C where
   obj HP := HP.H i
   map f := f.hom i
 
+instance (f : HP ⟶ HP') [IsIso f] (i : ι) : IsIso (f.hom i) :=
+  inferInstanceAs (IsIso ((HomologyPretheory.forget i).map f))
+
 end HomologyPretheory
 
 end TopPair

From 6b520019965583768bab73b6c0620c49c9e3e0cd Mon Sep 17 00:00:00 2001
From: Jacob Scharmberg <hi@jacobscharmberg.net>
Date: Tue, 12 May 2026 14:21:17 +0200
Subject: [PATCH 08/12] move `IsHomotopyInvariant` to `HomologyPretheory`
 namespace

---
 Mathlib/AlgebraicTopology/EilenbergSteenrod.lean | 15 ++++-----------
 1 file changed, 4 insertions(+), 11 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
index f0de307795d1d3..4db37061cc76cc 100644
--- a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
+++ b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
@@ -125,16 +125,7 @@ protected def forget (i : ι) : HomologyPretheory C c ⥤ TopCat.{u} ⥤ C where
 instance (f : HP ⟶ HP') [IsIso f] (i : ι) : IsIso (f.hom i) :=
   inferInstanceAs (IsIso ((HomologyPretheory.forget i).map f))
 
-end HomologyPretheory
-
-end TopPair
-
-namespace EilenbergSteenrod
-
-open HomologyPretheory
-
-variable {C : Type v} [Category C] [Limits.HasZeroMorphisms C] {ι : Type*} {c : ComplexShape ι}
-  (HP HP' : HomologyPretheory.{u} C c)
+variable (HP HP' : HomologyPretheory.{u} C c)
 
 /-- A `HomologyPretheory` is homotopy-invariant if its homology functor `Hₚ` takes homotopic maps to
 the same map in homology -/
@@ -152,4 +143,6 @@ instance : IsClosedUnderIsomorphisms (C := HomologyPretheory C c) IsHomotopyInva
       forgetₚ_map, ← (e.hom.homₚ _).naturality]
     cat_disch⟩
 
-end EilenbergSteenrod
+end HomologyPretheory
+
+end TopPair

From d6b6cb412b75c3275c7ec39ff610a73d4c400e8c Mon Sep 17 00:00:00 2001
From: Jacob Scharmberg <hi@jacobscharmberg.net>
Date: Tue, 12 May 2026 14:41:21 +0200
Subject: [PATCH 09/12] improve `IsHomotopyInvariant` API

---
 Mathlib/AlgebraicTopology/EilenbergSteenrod.lean | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
index 2c500a7523c88f..aab8d83ea1059d 100644
--- a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
+++ b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
@@ -129,14 +129,16 @@ variable (HP HP' : HomologyPretheory.{u} C c)
 
 /-- A `HomologyPretheory` is homotopy-invariant if its homology functor `Hₚ` takes homotopic maps to
 the same map in homology -/
-class IsHomotopyInvariant where
-  homotopy ⦃X Y : TopPair⦄ (f g : X ⟶ Y) (hfg : Homotopic f g) :
-      ∀ (i : ι), (HP.Hₚ i).map f = (HP.Hₚ i).map g := by cat_disch
+class IsHomotopyInvariant (HP : HomologyPretheory.{u} C c) where
+  map_eq_of_homotopy (HP) {X Y : TopPair} {f g : X ⟶ Y} (F : Homotopy f g) (i : ι) :
+    (HP.Hₚ i).map f = (HP.Hₚ i).map g := by cat_disch
+
+export IsHomotopyInvariant (map_eq_of_homotopy)
 
 instance : IsClosedUnderIsomorphisms (C := HomologyPretheory C c) IsHomotopyInvariant where
-  of_iso {HP HP'} e hHP := ⟨by
-    intro _ _ _ _ hfg _
-    have := hHP.homotopy _ _ hfg
+  of_iso {HP HP'} e _ := ⟨by
+    intro _ _ _ _ F _
+    have := HP.map_eq_of_homotopy F
     apply ((((HomologyPretheory.forgetₚ _).mapIso e).app _).cancel_iso_hom_left
       ((HP'.Hₚ _).map _) ((HP'.Hₚ _).map _)).mp
     simp only [CategoryTheory.Iso.app_hom, HomologyPretheory.forgetₚ_obj, Functor.mapIso_hom,

From 9c610625b1fc0b7a17b906e9930fad50694733e9 Mon Sep 17 00:00:00 2001
From: Jacob Scharmberg <hi@jacobscharmberg.net>
Date: Tue, 12 May 2026 15:09:44 +0200
Subject: [PATCH 10/12] add abbrev `isHomotopyInvariant` for an
 `ObjectProperty`

---
 .../AlgebraicTopology/EilenbergSteenrod.lean    | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
index aab8d83ea1059d..d96b5585c0860e 100644
--- a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
+++ b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
@@ -135,15 +135,14 @@ class IsHomotopyInvariant (HP : HomologyPretheory.{u} C c) where
 
 export IsHomotopyInvariant (map_eq_of_homotopy)
 
-instance : IsClosedUnderIsomorphisms (C := HomologyPretheory C c) IsHomotopyInvariant where
-  of_iso {HP HP'} e _ := ⟨by
-    intro _ _ _ _ F _
-    have := HP.map_eq_of_homotopy F
-    apply ((((HomologyPretheory.forgetₚ _).mapIso e).app _).cancel_iso_hom_left
-      ((HP'.Hₚ _).map _) ((HP'.Hₚ _).map _)).mp
-    simp only [CategoryTheory.Iso.app_hom, HomologyPretheory.forgetₚ_obj, Functor.mapIso_hom,
-      forgetₚ_map, ← (e.hom.homₚ _).naturality]
-    cat_disch⟩
+variable (C c) in
+abbrev isHomotopyInvariant : ObjectProperty (HomologyPretheory C c) :=
+  IsHomotopyInvariant
+
+instance : IsClosedUnderIsomorphisms (isHomotopyInvariant C c) where
+  of_iso e _ := ⟨fun F _ ↦ by
+    simp only [← cancel_epi ((e.hom.homₚ _).app _), ← NatTrans.naturality,
+      map_eq_of_homotopy _ F _]⟩
 
 end HomologyPretheory
 

From b626117c1b381c460ea946fc1fe1fa7e5ce399e2 Mon Sep 17 00:00:00 2001
From: Jacob Scharmberg <hi@jacobscharmberg.net>
Date: Tue, 12 May 2026 15:23:52 +0200
Subject: [PATCH 11/12] add missing docstring

---
 Mathlib/AlgebraicTopology/EilenbergSteenrod.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
index d96b5585c0860e..196433db71678b 100644
--- a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
+++ b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
@@ -136,6 +136,7 @@ class IsHomotopyInvariant (HP : HomologyPretheory.{u} C c) where
 export IsHomotopyInvariant (map_eq_of_homotopy)
 
 variable (C c) in
+/-- An abbreviation for `HomologyPretheory.IsHomotopyInvariant` as `ObjectProperty`. -/
 abbrev isHomotopyInvariant : ObjectProperty (HomologyPretheory C c) :=
   IsHomotopyInvariant
 

From 954e43d051800f093975621b1e7cc398677fcc56 Mon Sep 17 00:00:00 2001
From: quantumsnow <205372035+quantumsnow@users.noreply.github.com>
Date: Wed, 13 May 2026 07:30:17 +0000
Subject: [PATCH 12/12] remove explicit universe naming for `C`
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
---
 Mathlib/AlgebraicTopology/EilenbergSteenrod.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
index 196433db71678b..48e437f6c9a778 100644
--- a/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
+++ b/Mathlib/AlgebraicTopology/EilenbergSteenrod.lean
@@ -27,14 +27,14 @@ We introduce a typeclass `IsHomotopyInvariant` for the first axiom.
 
 open CategoryTheory TopPair ObjectProperty
 
-universe u v
+universe u
 
 namespace TopPair
 
 /-- A `HomologyPretheory` is the data of an Eilenberg-Steenrod homology theory. -/
 @[ext]
 structure HomologyPretheory
-    (C : Type v) [Category C] [Limits.HasZeroMorphisms C] {ι : Type*} (c : ComplexShape ι) where
+    (C : Type*) [Category* C] [Limits.HasZeroMorphisms C] {ι : Type*} (c : ComplexShape ι) where
   /-- The relative homology functor of a `HomologyPretheory`. -/
   Hₚ (i : ι) : TopPair.{u} ⥤ C
   /-- The regular homology functor of a `HomologyPretheory`. -/
@@ -48,7 +48,7 @@ structure HomologyPretheory
 
 namespace HomologyPretheory
 
-variable {C : Type v} [Category C] [Limits.HasZeroMorphisms C] {ι : Type*} {c : ComplexShape ι}
+variable {C : Type*} [Category* C] [Limits.HasZeroMorphisms C] {ι : Type*} {c : ComplexShape ι}
 
 /-- A morphism in the category `HomologyPretheory`. -/
 @[ext]