Commit 2025-11-18 12:49 885688db

View on Github →

feat: lemmas for paths-up-to-homotopy (#31574) We introduce Path.Homotopic.Quotient.mk as the normal form (rather than _root_.Quotient.mk) for constructing a path-up-to-homotopy from a path. This enables us to work more easily in the quotient. We add simp lemmas corresponding to the basic homotopies relating refl / symm / trans / cast.

Estimated changes

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

modified theorem FundamentalGroupoid.comp_eq

added theorem Path.Homotopic.Quotient.refl_trans

added theorem Path.Homotopic.Quotient.symm_trans

added theorem Path.Homotopic.Quotient.trans_assoc

added theorem Path.Homotopic.Quotient.trans_refl

added theorem Path.Homotopic.Quotient.trans_symm

added theorem Path.Homotopic.refl_trans

added theorem Path.Homotopic.symm_trans

added theorem Path.Homotopic.trans_assoc

added theorem Path.Homotopic.trans_refl

added theorem Path.Homotopic.trans_symm

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean

Modified Mathlib/Topology/Homotopy/Lifting.lean

Modified Mathlib/Topology/Homotopy/Path.lean

added def Path.Homotopic.Quotient.cast

added theorem Path.Homotopic.Quotient.cast_cast

added theorem Path.Homotopic.Quotient.cast_rfl_rfl

deleted def Path.Homotopic.Quotient.comp

added theorem Path.Homotopic.Quotient.eq

added theorem Path.Homotopic.Quotient.exact

added def Path.Homotopic.Quotient.map

deleted def Path.Homotopic.Quotient.mapFn

added theorem Path.Homotopic.Quotient.mk''_eq_mk

added theorem Path.Homotopic.Quotient.mk'_eq_mk

added def Path.Homotopic.Quotient.mk

added theorem Path.Homotopic.Quotient.mk_cast

added theorem Path.Homotopic.Quotient.mk_map

added theorem Path.Homotopic.Quotient.mk_refl

added theorem Path.Homotopic.Quotient.mk_symm

added theorem Path.Homotopic.Quotient.mk_trans

added def Path.Homotopic.Quotient.refl

added def Path.Homotopic.Quotient.symm

added def Path.Homotopic.Quotient.trans

deleted theorem Path.Homotopic.comp_lift

deleted theorem Path.Homotopic.map_lift

added theorem Path.Homotopic.symm₂

Modified Mathlib/Topology/Homotopy/Product.lean

modified theorem Path.Homotopic.prod_lift