Commit 2024-12-06 07:03 ec0985ae

View on Github →

feat(CategoryTheory): retracts of objects and morphisms (#19233) Defines retracts of objects and morphisms, and basic API. Used in #19135.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/MorphismProperty/Retract.lean

added theorem CategoryTheory.MorphismProperty.of_retract

Created Mathlib/CategoryTheory/Retract.lean

added def CategoryTheory.Retract.map

added def CategoryTheory.Retract.splitEpi

added def CategoryTheory.Retract.splitMono

added structure CategoryTheory.Retract

added theorem CategoryTheory.RetractArrow.i_w

added def CategoryTheory.RetractArrow.left

added theorem CategoryTheory.RetractArrow.r_w

added theorem CategoryTheory.RetractArrow.retract_left

added theorem CategoryTheory.RetractArrow.retract_right

added def CategoryTheory.RetractArrow.right