Commit 2025-09-03 10:11 140e7413

View on Github →

chore(CategoryTheory): process porting notes, part 2 (#28776) Go through all the porting notes in CategoryTheory, from Limits to Monoidal. Lots of them can be fixed, others are of the format "Lean 4 does this better" and a few are more TODOs which do not really depend on the port.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/FilteredColimitCommutesProduct.lean

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

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

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

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

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

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

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

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

added theorem CategoryTheory.Limits.image.lift_mk_comp

added theorem CategoryTheory.Limits.image.lift_mk_factorThruImage

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

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

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

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

Modified Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.lean

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

added theorem CategoryTheory.NormalEpiCategory.hasColimit_parallelPair

deleted def CategoryTheory.NormalEpiCategory.hasColimit_parallelPair

added theorem CategoryTheory.NormalEpiCategory.pushout_of_epi

deleted def CategoryTheory.NormalEpiCategory.pushout_of_epi

added theorem CategoryTheory.NormalMonoCategory.hasLimit_parallelPair

deleted def CategoryTheory.NormalMonoCategory.hasLimit_parallelPair

added theorem CategoryTheory.NormalMonoCategory.pullback_of_mono

deleted def CategoryTheory.NormalMonoCategory.pullback_of_mono

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

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

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

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

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

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

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

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

deleted theorem CategoryTheory.Limits.Types.Colimit.w_apply'

deleted theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply'

deleted theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply'

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

Modified Mathlib/CategoryTheory/Localization/Adjunction.lean

Modified Mathlib/CategoryTheory/Localization/Bifunctor.lean

Modified Mathlib/CategoryTheory/Localization/Predicate.lean

deleted theorem CategoryTheory.Localization.Lifting.compLeft_iso

deleted def CategoryTheory.Localization.Lifting.iso

Modified Mathlib/CategoryTheory/Localization/Trifunctor.lean

Modified Mathlib/CategoryTheory/Monad/Algebra.lean

Modified Mathlib/CategoryTheory/Monad/Basic.lean

Modified Mathlib/CategoryTheory/Monad/Kleisli.lean

Modified Mathlib/CategoryTheory/Monad/Monadicity.lean

Modified Mathlib/CategoryTheory/Monad/Types.lean

Modified Mathlib/CategoryTheory/Monoidal/Bimod.lean

Modified Mathlib/CategoryTheory/Monoidal/CommMon_.lean

Modified Mathlib/CategoryTheory/Monoidal/Free/Basic.lean

Modified Mathlib/Topology/Sheaves/LocalPredicate.lean