Commit 2025-04-01 10:14 307de592

View on Github →

feat: the essential image of a functor is closed under the limits it preserves (#23480) From Toric

Estimated changes

Modified Mathlib/CategoryTheory/EssentialImage.lean

added def CategoryTheory.Functor.essImage.liftFunctor

added def CategoryTheory.Functor.essImage.liftFunctorCompIso

Modified Mathlib/CategoryTheory/Limits/FullSubcategory.lean

deleted theorem CategoryTheory.Limits.ClosedUnderColimitsOfShape.colimit

deleted theorem CategoryTheory.Limits.ClosedUnderLimitsOfShape.limit