Commit 2025-03-13 16:39 d27218a8

View on Github →

chore: review of porting notes in CategoryTheory/ (#22899) This covers the "easy" porting notes in "the top half" of CategoryTheory/.

Estimated changes

Modified Mathlib/CategoryTheory/Abelian/Basic.lean

Modified Mathlib/CategoryTheory/Abelian/Ext.lean

Modified Mathlib/CategoryTheory/Abelian/FunctorCategory.lean

Modified Mathlib/CategoryTheory/Abelian/Opposite.lean

Modified Mathlib/CategoryTheory/Action/Limits.lean

Modified Mathlib/CategoryTheory/Adjunction/Basic.lean

Modified Mathlib/CategoryTheory/Bicategory/Free.lean

Modified Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean

Modified Mathlib/CategoryTheory/Category/Basic.lean

Modified Mathlib/CategoryTheory/Category/Preorder.lean

Modified Mathlib/CategoryTheory/Category/ULift.lean

Modified Mathlib/CategoryTheory/Closed/Cartesian.lean

Modified Mathlib/CategoryTheory/Comma/Arrow.lean

modified theorem CategoryTheory.Arrow.w

Modified Mathlib/CategoryTheory/Comma/Over/Basic.lean

Modified Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean

Modified Mathlib/CategoryTheory/DiscreteCategory.lean

Modified Mathlib/CategoryTheory/Enriched/Basic.lean

Modified Mathlib/CategoryTheory/EqToHom.lean

Modified Mathlib/CategoryTheory/EssentialImage.lean

modified def CategoryTheory.Functor.essImage.getIso

Modified Mathlib/CategoryTheory/Filtered/Basic.lean

Modified Mathlib/CategoryTheory/FintypeCat.lean

Modified Mathlib/CategoryTheory/Functor/FullyFaithful.lean

Modified Mathlib/CategoryTheory/Generator/Basic.lean

Modified Mathlib/CategoryTheory/GradedObject.lean

Modified Mathlib/CategoryTheory/Grothendieck.lean

Modified Mathlib/CategoryTheory/Idempotents/Karoubi.lean

modified theorem CategoryTheory.Idempotents.Karoubi.coe_X

Modified Mathlib/CategoryTheory/Iso.lean

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

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

Modified Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean

Modified Mathlib/CategoryTheory/Limits/Fubini.lean

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

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

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

Modified Mathlib/CategoryTheory/Limits/Preserves/FunctorCategory.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/Types.lean

Modified Mathlib/CategoryTheory/Simple.lean

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

Modified Mathlib/CategoryTheory/Skeletal.lean

Modified Mathlib/CategoryTheory/Subterminal.lean

Modified Mathlib/CategoryTheory/Types.lean

Modified Mathlib/CategoryTheory/Whiskering.lean

Modified Mathlib/CategoryTheory/WithTerminal.lean