Commit 2025-06-18 19:19 1ac9e993

View on Github →

chore(CategoryTheory/Limits): add equiv variant of Limits.Fork.isLimitOfIsos and other API lemmas (#26117) In particular, adds simp lemmas for isomorphisms of (co)cones.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Cones.lean

added theorem CategoryTheory.Limits.CoconeMorphism.hom_inv_id

added theorem CategoryTheory.Limits.CoconeMorphism.inv_hom_id

added theorem CategoryTheory.Limits.ConeMorphism.hom_inv_id

added theorem CategoryTheory.Limits.ConeMorphism.inv_hom_id

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

added theorem CategoryTheory.Limits.opCoproductIsoProduct'_hom_comp_proj

added theorem CategoryTheory.Limits.opCoproductIsoProduct_hom_comp_π

Modified Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean

added def CategoryTheory.Limits.Cofork.isColimitEquivOfIsos

added def CategoryTheory.Limits.Cofork.isColimitOfIsos

added def CategoryTheory.Limits.Fork.isLimitEquivOfIsos

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean

added theorem CategoryTheory.Limits.Cofan.IsColimit.inj_desc

added theorem CategoryTheory.Limits.Fan.IsLimit.lift_proj