Commit 2026-03-20 14:17 1f3cdaa7

View on Github →

chore(AlgebraicTopology): cleaning up ExtraDegeneracy.lean (#36857) This PR removes some erw in the API for extra-degeneracies. Automation is also improved. (We also add the fact that an extradegeneracy of an augmented simplicial object gives a section of the augmentation.)

Estimated changes

Modified Mathlib/Algebra/Homology/Single.lean

Modified Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

added def CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_

added theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_app_comp_hom_app

added theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_app_op_mk_zero

added theorem CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_comp_hom

added def CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.splitEpi

Modified Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean

modified def CategoryTheory.SimplicialObject.whiskering

added theorem CategoryTheory.SimplicialObject.whiskering_obj_obj_δ

added theorem CategoryTheory.SimplicialObject.whiskering_obj_obj_σ