Commit 2026-05-01 13:07 e6a5fb08

View on Github →

feat: add the category of topological pairs (#36621) This is needed for the Eilenberg-Steenrod axioms for a homology theory.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Category/TopCat/Basic.lean

added theorem TopCat.isEmbedding_iff

Modified Mathlib/Topology/Category/TopCat/Limits/Basic.lean

added theorem TopCat.IsInducing.empty

Created Mathlib/Topology/Category/TopPair.lean

added theorem TopPair.Hom.w

added theorem TopPair.Homotopic.equivalence

added def TopPair.Homotopic

added def TopPair.Homotopy.comp

added def TopPair.Homotopy.refl

added def TopPair.Homotopy.symm

added theorem TopPair.Homotopy.symm_bijective

added theorem TopPair.Homotopy.symm_symm

added theorem TopPair.Homotopy.symm_trans

added theorem TopPair.Homotopy.w_apply'

added structure TopPair.Homotopy

added def TopPair.incl

added def TopPair.inclAdjProj₁

added theorem TopPair.isEmbedding_map

added def TopPair.proj₁AdjDiag

Modified Mathlib/Topology/Homotopy/TopCat/Basic.lean

modified def TopCat.Homotopy.h

added theorem TopCat.Homotopy.h_comp

added theorem TopCat.Homotopy.h_hom_apply

added theorem TopCat.Homotopy.h_refl

added theorem TopCat.Homotopy.h_symm

modified theorem TopCat.Homotopy.ι₀_h

modified theorem TopCat.Homotopy.ι₁_h