Commit 2025-05-13 00:25 06711512

View on Github →

chore(CategoryTheory): redo IsLimit.ofNatIso with RepresentableBy. (#24718)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

Modified Mathlib/CategoryTheory/Limits/IsLimit.lean

added theorem CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone_coconeOfHom

deleted theorem CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone_cooneOfHom

added def CategoryTheory.Limits.IsColimit.corepresentableBy

modified def CategoryTheory.Limits.IsColimit.homEquiv

added def CategoryTheory.Limits.IsColimit.ofCorepresentableBy

deleted def CategoryTheory.Limits.IsColimit.ofNatIso

modified theorem CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone_coneOfHom

deleted def CategoryTheory.Limits.IsLimit.ofNatIso

added def CategoryTheory.Limits.IsLimit.ofRepresentableBy

added def CategoryTheory.Limits.IsLimit.representableBy

Modified Mathlib/CategoryTheory/Limits/Presheaf.lean