Commit 2024-10-27 16:51 8c2c97e8

View on Github →

chore: fix lemma names for preservesLimitIso (#18288)

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean

Modified Mathlib/CategoryTheory/GlueData.lean

Modified Mathlib/CategoryTheory/Limits/Elements.lean

Modified Mathlib/CategoryTheory/Limits/IndYoneda.lean

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

added theorem CategoryTheory.lift_comp_preservesLimitIso_hom

deleted theorem CategoryTheory.lift_comp_preservesLimitsIso_hom

added theorem CategoryTheory.preservesColimitIso_inv_comp_desc

deleted theorem CategoryTheory.preservesColimitsIso_inv_comp_desc

added theorem CategoryTheory.preservesLimitIso_hom_π

added theorem CategoryTheory.preservesLimitIso_inv_π

deleted theorem CategoryTheory.preservesLimitsIso_hom_π

deleted theorem CategoryTheory.preservesLimitsIso_inv_π

added theorem CategoryTheory.ι_preservesColimitIso_hom

added theorem CategoryTheory.ι_preservesColimitIso_inv

deleted theorem CategoryTheory.ι_preservesColimitsIso_hom

deleted theorem CategoryTheory.ι_preservesColimitsIso_inv

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

Modified Mathlib/Geometry/Manifold/Sheaf/Smooth.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean

Modified Mathlib/Topology/Gluing.lean