Commit 2026-09-07 10:31 c74949bb

View on Github →

chore(CategoryTheory/Limits/HasLimits): use to_dual more (#42872) This PR continues the work of #41017 to use to_dual in CategoryTheory.Limits.HasLimits. Notes:

A few theorems like ι_isoOfEquivalence_hom has their type changed, because the old version wasn't actually dual to the supposed dual version. As a result, a proof in Mathlib/CategoryTheory/Limits/Shapes/Products.lean could be simplified.
A few theorems like isoOfNatIso_ι_hom were renamed to ι_isoOfNatIso_hom, which is a more accurate name.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Final.lean

Modified Mathlib/CategoryTheory/Limits/Fubini.lean

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

deleted def CategoryTheory.Limits.HasColimit.isoOfEquivalence

deleted theorem CategoryTheory.Limits.HasColimit.isoOfNatIso_hom_desc

deleted theorem CategoryTheory.Limits.HasColimit.isoOfNatIso_inv_desc

deleted theorem CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom

deleted theorem CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_inv

deleted theorem CategoryTheory.Limits.HasColimit.ι_isoOfEquivalence_hom

deleted theorem CategoryTheory.Limits.HasColimit.ι_isoOfEquivalence_inv

deleted theorem CategoryTheory.Limits.HasColimitsOfShape.of_essentiallySmall

deleted theorem CategoryTheory.Limits.HasColimitsOfShape.of_small

deleted def CategoryTheory.Limits.IsColimit.op

deleted def CategoryTheory.Limits.IsColimit.unop

deleted def CategoryTheory.Limits.colim.ι

deleted def CategoryTheory.Limits.colim

deleted theorem CategoryTheory.Limits.colimMap_eq

deleted theorem CategoryTheory.Limits.colimit.map_post

deleted def CategoryTheory.Limits.colimit.post

deleted theorem CategoryTheory.Limits.colimit.post_desc

deleted theorem CategoryTheory.Limits.colimit.post_post

deleted def CategoryTheory.Limits.colimit.pre

deleted theorem CategoryTheory.Limits.colimit.pre_desc

deleted theorem CategoryTheory.Limits.colimit.pre_eq

deleted theorem CategoryTheory.Limits.colimit.pre_id

deleted theorem CategoryTheory.Limits.colimit.pre_map'

deleted theorem CategoryTheory.Limits.colimit.pre_map

deleted theorem CategoryTheory.Limits.colimit.pre_post

deleted theorem CategoryTheory.Limits.colimit.pre_pre

deleted theorem CategoryTheory.Limits.colimit.ι_inv_pre

deleted theorem CategoryTheory.Limits.colimit.ι_map

deleted theorem CategoryTheory.Limits.colimit.ι_post

deleted theorem CategoryTheory.Limits.colimit.ι_pre

deleted theorem CategoryTheory.Limits.hasColimit_equivalence_comp_iff

deleted theorem CategoryTheory.Limits.hasColimit_inverse_equivalence_comp_iff

deleted theorem CategoryTheory.Limits.hasColimit_of_equivalence_comp

deleted theorem CategoryTheory.Limits.hasColimitsOfShape_of_equivalence

deleted theorem CategoryTheory.Limits.hasColimitsOfSizeOfUnivLE

deleted theorem CategoryTheory.Limits.hasColimitsOfSizeShrink

deleted def CategoryTheory.Limits.isColimitEquivIsLimitOp

deleted def CategoryTheory.Limits.isColimitOfOp

deleted def CategoryTheory.Limits.isColimitOfUnop

deleted theorem CategoryTheory.Limits.limit.id_pre

added theorem CategoryTheory.Limits.limit.inv_pre_π

added theorem CategoryTheory.Limits.limit.map_π

added theorem CategoryTheory.Limits.limit.pre_id

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

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

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

Modified Mathlib/CategoryTheory/Sites/CompatiblePlus.lean

Modified Mathlib/CategoryTheory/Sites/LeftExact.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean