Commit 2025-03-04 05:26 630d5156

View on Github →

chore(CategoryTheory): fix hasLimitOfIso (#22514) hasLimitOfIso is renamed hasLimit_of_iso. A new lemma hasLimit_iff_of_iso is added.

Estimated changes

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

Modified Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean

Modified Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean

Modified Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

Modified Mathlib/CategoryTheory/Adjunction/Limits.lean

Modified Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean

Modified Mathlib/CategoryTheory/GlueData.lean

Modified Mathlib/CategoryTheory/GradedObject.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/Pullbacks.lean

Modified Mathlib/CategoryTheory/Limits/Fubini.lean

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

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

deleted theorem CategoryTheory.Limits.hasColimitOfIso

added theorem CategoryTheory.Limits.hasColimit_iff_of_iso

added theorem CategoryTheory.Limits.hasColimit_of_iso

deleted theorem CategoryTheory.Limits.hasLimitOfIso

added theorem CategoryTheory.Limits.hasLimit_iff_of_iso

added theorem CategoryTheory.Limits.hasLimit_of_iso

Modified Mathlib/CategoryTheory/Limits/Indization/Category.lean

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

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

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

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

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

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

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

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

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean

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

Modified Mathlib/CategoryTheory/Monad/Comonadicity.lean

Modified Mathlib/CategoryTheory/Monad/Limits.lean

Modified Mathlib/CategoryTheory/Monad/Monadicity.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/Order/Category/OmegaCompletePartialOrder.lean

Modified Mathlib/Topology/Category/CompHausLike/Limits.lean