Commit 2025-08-11 09:44 ba407fdd

View on Github →

refactor(CategoryTheory): have Functor not extend Prefunctor (#28106) All the resulting changes are improvements; we just get to remove a bunch of hacky projections which were otherwise necessary to steer elaboration.

Estimated changes

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

Modified Mathlib/AlgebraicGeometry/Modules/Tilde.lean

Modified Mathlib/AlgebraicGeometry/Scheme.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

Modified Mathlib/CategoryTheory/Closed/Cartesian.lean

added def CategoryTheory.exp.delabFunctorObjExp

deleted def CategoryTheory.exp.delabPrefunctorObjExp

Modified Mathlib/CategoryTheory/Comma/Presheaf/Colimit.lean

Modified Mathlib/CategoryTheory/EqToHom.lean

Modified Mathlib/CategoryTheory/Functor/Basic.lean

added theorem CategoryTheory.Functor.congr_map

added def CategoryTheory.Functor.toPrefunctor

Modified Mathlib/CategoryTheory/Functor/FullyFaithful.lean

Modified Mathlib/CategoryTheory/Functor/Functorial.lean

Modified Mathlib/CategoryTheory/Galois/Decomposition.lean

Modified Mathlib/CategoryTheory/Groupoid.lean

Modified Mathlib/CategoryTheory/Limits/IsLimit.lean

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

Modified Mathlib/CategoryTheory/Limits/Presheaf.lean

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

Modified Mathlib/CategoryTheory/Monoidal/Opposite.lean

modified def CategoryTheory.mopFunctor

modified def CategoryTheory.unmopFunctor

Modified Mathlib/CategoryTheory/PathCategory/Basic.lean

Modified Mathlib/CategoryTheory/Sites/PreservesLocallyBijective.lean

Modified Mathlib/CategoryTheory/Types.lean

Modified Mathlib/Topology/Sheaves/Presheaf.lean