feat(AlgebraicTopology): `HomologyPretheory` for Eilenberg-Steenrod homology by quantumsnow · Pull Request #39236 · leanprover-community/mathlib4

quantumsnow · 2026-05-12T08:45:00Z

This splits out a part of #38369 into a separate PR.

It includes a structure TopPair.HomologyPretheory containing the data for an Eilenberg-Steenrod homology theory and the first Eilenberg-Steenrod axiom as a typeclass EilenbergSteenrod.IsHomotopyInvariant.

…riant`

github-actions · 2026-05-12T08:45:15Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-05-12T08:46:15Z

PR summary a7c945e01f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.AlgebraicTopology.EilenbergSteenrod` (new file)	1377

Declarations diff

+ Hom
+ Hom.iso_comm_app
+ Hom.w_app
+ HomologyPretheory
+ IsHomotopyInvariant
+ forget
+ forgetₚ
+ instance (f : HP ⟶ HP') [IsIso f] (i : ι) : IsIso (f.hom i)
+ instance (f : HP ⟶ HP') [IsIso f] (i : ι) : IsIso (f.homₚ i)
+ instance : Category (HomologyPretheory C c)
+ instance : IsClosedUnderIsomorphisms (isHomotopyInvariant C c)
+ inv_hom_iso_homₚ
+ inv_hom_iso_homₚ_app
+ isHomotopyInvariant
+ iso_homₚ_inv_hom
+ iso_homₚ_inv_hom_app

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.

No changes to weak technical debt.

joelriou · 2026-05-12T10:19:14Z

+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


Suggested change

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} (hfg : Homotopy f g) (i : ι) :

(HP.Hₚ i).map f = (HP.Hₚ i).map g := by cat_disch

Then, we can directly use IsHomotopyInvariant.map_eq_of_homotopy HP hfg i (and after doing export IsHomotopyInvariant (map_eq_of_homotopy) and the change of namespace above, we could use dot notation more easily as map_eq_of_homotopy would have HP as an explicit variable).

Thanks, I have also exported map_eq_of_homotopy as you suggested. I hope this is what you meant.

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

…retheory`s.

…into homology-pretheory

quantumsnow · 2026-05-12T13:14:06Z

-awaiting-author

joelriou · 2026-05-12T14:59:49Z

+/-- 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


Suggested change

(C : Type v) [Category C] [Limits.HasZeroMorphisms C] {ι : Type*} (c : ComplexShape ι) where

(C : Type*) [Category* C] [Limits.HasZeroMorphisms C] {ι : Type*} (c : ComplexShape ι) where

joelriou · 2026-05-12T14:59:55Z

+
+open CategoryTheory TopPair ObjectProperty
+
+universe u v


Suggested change

universe u v

universe u

joelriou · 2026-05-12T15:00:26Z

+
+namespace HomologyPretheory
+
+variable {C : Type v} [Category C] [Limits.HasZeroMorphisms C] {ι : Type*} {c : ComplexShape ι}


Suggested change

variable {C : Type v} [Category C] [Limits.HasZeroMorphisms C] {ι : Type*} {c : ComplexShape ι}

variable {C : Type*} [Category* C] [Limits.HasZeroMorphisms C] {ι : Type*} {c : ComplexShape ι}

joelriou · 2026-05-12T15:00:40Z

+
+/-- A morphism in the category `HomologyPretheory`. -/
+@[ext]
+structure Hom (HP HP' : HomologyPretheory C c) where


Suggested change

structure Hom (HP HP' : HomologyPretheory C c) where

structure Hom (HP HP' : HomologyPretheory.{u} C c) where

joelriou · 2026-05-12T15:00:55Z

+attribute [reassoc (attr := local simp)] Hom.w
+
+@[simps]
+instance : Category (HomologyPretheory C c) where


Suggested change

instance : Category (HomologyPretheory C c) where

instance : Category (HomologyPretheory.{u} C c) where

joelriou · 2026-05-12T15:01:07Z

+  id _ := { homₚ _ := 𝟙 _ }
+  comp f g := { homₚ _ := f.homₚ _ ≫ g.homₚ _ }
+
+variable {HP HP' : HomologyPretheory C c}


Suggested change

variable {HP HP' : HomologyPretheory C c}

variable {HP HP' : HomologyPretheory.{u} C c}

add TopPair.HomologyPretheory and `EilenbergSteenrod.IsHomotopyInva…

d5f60e5

…riant`

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label May 12, 2026

github-actions Bot added the t-algebraic-topology Algebraic topology label May 12, 2026

quantumsnow mentioned this pull request May 12, 2026

feat(AlgebraicTopology): Eilenberg Steenrod axioms #38369

Open

2 tasks

joelriou reviewed May 12, 2026

View reviewed changes

Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean Outdated

joelriou reviewed May 12, 2026

View reviewed changes

Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean

joelriou reviewed May 12, 2026

View reviewed changes

Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean Outdated

joelriou reviewed May 12, 2026

View reviewed changes

Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean Outdated

joelriou reviewed May 12, 2026

View reviewed changes

Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean Outdated

joelriou reviewed May 12, 2026

View reviewed changes

Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean Outdated

joelriou reviewed May 12, 2026

View reviewed changes

Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean Outdated

joelriou reviewed May 12, 2026

View reviewed changes

Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean Outdated

joelriou reviewed May 12, 2026

View reviewed changes

Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean Outdated

joelriou reviewed May 12, 2026

View reviewed changes

Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean

joelriou reviewed May 12, 2026

View reviewed changes

Comment thread Mathlib/AlgebraicTopology/EilenbergSteenrod.lean Outdated

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label May 12, 2026

quantumsnow and others added 10 commits May 12, 2026 11:58

style fixes

2b7385f

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

shorten module docstring

6da11b4

move category instance

9db4449

rename some lemmas

eb457ac

dsimp statement of Hom.iso_comm_app

24f83fd

add IsIso instance on homₚ and hom of an iso between `HomologyP…

717942a

…retheory`s.

move IsHomotopyInvariant to HomologyPretheory namespace

6b52001

Merge branch 'homology-pretheory' of github.com:quantumsnow/mathlib4 …

1860d29

…into homology-pretheory

improve IsHomotopyInvariant API

d6b6cb4

add abbrev isHomotopyInvariant for an ObjectProperty

9c61062

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 12, 2026

add missing docstring

b626117

joelriou reviewed May 12, 2026

View reviewed changes

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes. label May 12, 2026

	(C : Type v) [Category C] [Limits.HasZeroMorphisms C] {ι : Type*} (c : ComplexShape ι) where
	(C : Type) [Category C] [Limits.HasZeroMorphisms C] {ι : Type*} (c : ComplexShape ι) where


		namespace HomologyPretheory

		variable {C : Type v} [Category C] [Limits.HasZeroMorphisms C] {ι : Type*} {c : ComplexShape ι}

	variable {C : Type v} [Category C] [Limits.HasZeroMorphisms C] {ι : Type*} {c : ComplexShape ι}
	variable {C : Type} [Category C] [Limits.HasZeroMorphisms C] {ι : Type*} {c : ComplexShape ι}

	structure Hom (HP HP' : HomologyPretheory C c) where
	structure Hom (HP HP' : HomologyPretheory.{u} C c) where

	instance : Category (HomologyPretheory C c) where
	instance : Category (HomologyPretheory.{u} C c) where

	variable {HP HP' : HomologyPretheory C c}
	variable {HP HP' : HomologyPretheory.{u} C c}

Conversation

quantumsnow commented May 12, 2026

Uh oh!

github-actions Bot commented May 12, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented May 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary a7c945e01f

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

quantumsnow commented May 12, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

github-actions Bot commented May 12, 2026 •

edited

Loading