Commit 2026-06-23 12:20 f4001a93

View on Github →

feat(CategoryTheory/Limits/IsLimit): use to_dual on IsLimit (#36572) This PR makes a start at translating IsLimit using to_dual.

Estimated changes

Modified Mathlib/Algebra/Category/Grp/LargeColimits.lean

Modified Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean

Modified Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Colim.lean

Modified Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Connected.lean

Modified Mathlib/CategoryTheory/Limits/Cones.lean

Modified Mathlib/CategoryTheory/Limits/IsLimit.lean

deleted def CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso

deleted theorem CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc

deleted theorem CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_inv_desc

deleted def CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence

deleted def CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso

deleted theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom_desc

deleted theorem CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv_desc

deleted theorem CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom

deleted theorem CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv

deleted theorem CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_hom

deleted theorem CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_inv

deleted def CategoryTheory.Limits.IsColimit.descCoconeMorphism

deleted theorem CategoryTheory.Limits.IsColimit.desc_self

deleted def CategoryTheory.Limits.IsColimit.equivIsoColimit

deleted theorem CategoryTheory.Limits.IsColimit.equivIsoColimit_apply

deleted theorem CategoryTheory.Limits.IsColimit.equivIsoColimit_symm_apply

deleted def CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso

deleted theorem CategoryTheory.Limits.IsColimit.existsUnique

deleted def CategoryTheory.Limits.IsColimit.extendIso

deleted def CategoryTheory.Limits.IsColimit.extendIsoEquiv

deleted def CategoryTheory.Limits.IsColimit.homEquiv

deleted theorem CategoryTheory.Limits.IsColimit.homEquiv_apply

deleted theorem CategoryTheory.Limits.IsColimit.homEquiv_symm_naturality

deleted def CategoryTheory.Limits.IsColimit.homIso

deleted theorem CategoryTheory.Limits.IsColimit.hom_desc

deleted theorem CategoryTheory.Limits.IsColimit.hom_ext

deleted theorem CategoryTheory.Limits.IsColimit.hom_isIso

deleted def CategoryTheory.Limits.IsColimit.map

deleted def CategoryTheory.Limits.IsColimit.mapCoconeEquiv

deleted def CategoryTheory.Limits.IsColimit.mkCoconeMorphism

deleted theorem CategoryTheory.Limits.IsColimit.nonempty_isColimit_iff_isIso_desc

modified def CategoryTheory.Limits.IsColimit.ofCoconeEquiv

deleted theorem CategoryTheory.Limits.IsColimit.ofCoconeEquiv_apply_desc

deleted theorem CategoryTheory.Limits.IsColimit.ofCoconeEquiv_symm_apply_desc

deleted def CategoryTheory.Limits.IsColimit.ofExistsUnique

deleted def CategoryTheory.Limits.IsColimit.ofExtendIso

deleted def CategoryTheory.Limits.IsColimit.ofFaithful

deleted def CategoryTheory.Limits.IsColimit.ofIsoColimit

deleted theorem CategoryTheory.Limits.IsColimit.ofIsoColimit_desc

deleted def CategoryTheory.Limits.IsColimit.ofLeftAdjoint

deleted def CategoryTheory.Limits.IsColimit.ofPointIso

modified def CategoryTheory.Limits.IsColimit.ofWhiskerEquivalence

deleted def CategoryTheory.Limits.IsColimit.precomposeHomEquiv

deleted def CategoryTheory.Limits.IsColimit.precomposeInvEquiv

deleted theorem CategoryTheory.Limits.IsColimit.uniq_cocone_morphism

deleted def CategoryTheory.Limits.IsColimit.uniqueUpToIso

modified def CategoryTheory.Limits.IsColimit.whiskerEquivalence

deleted def CategoryTheory.Limits.IsColimit.whiskerEquivalenceEquiv

deleted theorem CategoryTheory.Limits.IsColimit.ι_app_homEquiv_symm

deleted theorem CategoryTheory.Limits.IsColimit.ι_map

modified def CategoryTheory.Limits.IsLimit.homIso

deleted theorem CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_desc

added theorem CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_lift

deleted theorem CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_desc

added theorem CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_lift

Modified Mathlib/CategoryTheory/Limits/MonoCoprod.lean

Modified Mathlib/CategoryTheory/Limits/MorphismProperty.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Bifunctor.lean

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

Modified Mathlib/CategoryTheory/Limits/Types/Colimits.lean

Modified Mathlib/CategoryTheory/Monad/Limits.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

Modified Mathlib/CategoryTheory/Presentable/ColimitPresentation.lean

Modified Mathlib/Condensed/Discrete/Colimit.lean