Commit 2026-03-06 08:34 844193d3

View on Github →

refactor(CategoryTheory/Sites): redefine the category of sheaves using ObjectProperty.FullSubcategory (#36081) This PR refactors Sheaf so that it becomes a fullsubcategory of the category of presheaves. Mostly it changes val into obj or hom (deprecated alias have been added for the non-automatically generated lemmas). Functors to categories of sheaves are now constructed using ObectProperty.lift. (I have used the output of Claude from #36129 only in order to fix the single remaining sorry in Condensed.Discrete.LocallyConstant).

Estimated changes

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

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

modified theorem PresheafOfModules.Sheafify.map_smul_eq

modified theorem PresheafOfModules.comp_toPresheaf_map_sheafifyHomEquiv'_symm_hom

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

modified def SheafOfModules.evaluation

modified def SheafOfModules.forget

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

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

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

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

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

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

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

modified theorem SheafOfModules.unitToPushforwardObjUnit_val_app_apply

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

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

Modified Mathlib/AlgebraicGeometry/GluingOneHypercover.lean

modified theorem AlgebraicGeometry.Scheme.GlueData.sheafValGluedMk_val

Modified Mathlib/AlgebraicGeometry/Modules/Presheaf.lean

Modified Mathlib/AlgebraicGeometry/Modules/Sheaf.lean

Modified Mathlib/AlgebraicGeometry/Modules/Tilde.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean

Modified Mathlib/AlgebraicGeometry/Sites/Representability.lean

Modified Mathlib/AlgebraicGeometry/Spec.lean

Modified Mathlib/AlgebraicGeometry/SpreadingOut.lean

Modified Mathlib/AlgebraicGeometry/StructureSheaf.lean

Modified Mathlib/CategoryTheory/Generator/Sheaf.lean

Modified Mathlib/CategoryTheory/Sites/Adjunction.lean

added theorem CategoryTheory.Sheaf.adjunction_counit_app_hom

deleted theorem CategoryTheory.Sheaf.adjunction_counit_app_val

added theorem CategoryTheory.Sheaf.adjunction_unit_app_hom

deleted theorem CategoryTheory.Sheaf.adjunction_unit_app_val

Modified Mathlib/CategoryTheory/Sites/CartesianClosed.lean

Modified Mathlib/CategoryTheory/Sites/CartesianMonoidal.lean

added theorem CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_hom

deleted theorem CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_val

added theorem CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_hom

deleted theorem CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_val

added theorem CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_hom

deleted theorem CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_val

added theorem CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_hom

deleted theorem CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_val

added theorem CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_hom

deleted theorem CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_val

modified theorem CategoryTheory.Sheaf.tensorProd_isSheaf

Modified Mathlib/CategoryTheory/Sites/Coherent/Equivalence.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/ExtensiveColimits.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/LocallySurjective.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/SequentialLimit.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean

Modified Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean

Modified Mathlib/CategoryTheory/Sites/ConstantSheaf.lean

added theorem CategoryTheory.constantCommuteCompose_hom_app_hom

deleted theorem CategoryTheory.constantCommuteCompose_hom_app_val

Modified Mathlib/CategoryTheory/Sites/Continuous.lean

modified def CategoryTheory.Functor.sheafPushforwardContinuous

Modified Mathlib/CategoryTheory/Sites/CoverLifting.lean

added theorem CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_hom

deleted theorem CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val

added theorem CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_hom

deleted theorem CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_val

added theorem CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_hom

deleted theorem CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_val

added theorem CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_hom

deleted theorem CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_val

modified def CategoryTheory.Functor.sheafPushforwardCocontinuous

Modified Mathlib/CategoryTheory/Sites/CoverPreserving.lean

Modified Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean

modified theorem CategoryTheory.Functor.IsCoverDense.ext

modified def CategoryTheory.Functor.IsCoverDense.homOver

modified def CategoryTheory.Functor.IsCoverDense.isoOver

modified theorem CategoryTheory.Functor.IsCoverDense.iso_of_restrict_iso

modified theorem CategoryTheory.Functor.IsCoverDense.sheafHom_eq

modified theorem CategoryTheory.Functor.IsCoverDense.sheafHom_restrict_eq

Modified Mathlib/CategoryTheory/Sites/DenseSubsite/OneHypercoverDense.lean

Modified Mathlib/CategoryTheory/Sites/DenseSubsite/SheafEquiv.lean

Modified Mathlib/CategoryTheory/Sites/Descent/IsPrestack.lean

Modified Mathlib/CategoryTheory/Sites/Equivalence.lean

modified def CategoryTheory.Equivalence.sheafCongr.functor

modified def CategoryTheory.Equivalence.sheafCongr.inverse

Modified Mathlib/CategoryTheory/Sites/GlobalSections.lean

Modified Mathlib/CategoryTheory/Sites/Hypercover/One.lean

modified theorem CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map

Modified Mathlib/CategoryTheory/Sites/Limits.lean

Modified Mathlib/CategoryTheory/Sites/Localization.lean

Modified Mathlib/CategoryTheory/Sites/LocallyBijective.lean

Modified Mathlib/CategoryTheory/Sites/LocallyFullyFaithful.lean

Modified Mathlib/CategoryTheory/Sites/LocallyInjective.lean

Modified Mathlib/CategoryTheory/Sites/LocallySurjective.lean

Modified Mathlib/CategoryTheory/Sites/MayerVietorisSquare.lean

Modified Mathlib/CategoryTheory/Sites/Over.lean

Modified Mathlib/CategoryTheory/Sites/Point/Conservative.lean

Modified Mathlib/CategoryTheory/Sites/Point/Skyscraper.lean

added theorem CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_apply_hom

deleted theorem CategoryTheory.GrothendieckTopology.Point.skyscraperSheafAdjunction_homEquiv_apply_val

Modified Mathlib/CategoryTheory/Sites/PreservesSheafification.lean

Modified Mathlib/CategoryTheory/Sites/RegularEpi.lean

Modified Mathlib/CategoryTheory/Sites/Sheaf.lean

modified theorem CategoryTheory.Sheaf.Hom.add_app

deleted structure CategoryTheory.Sheaf.Hom

added theorem CategoryTheory.Sheaf.cond

modified theorem CategoryTheory.Sheaf.hom_ext

added theorem CategoryTheory.Sheaf.hom_ext_iff

deleted structure CategoryTheory.Sheaf

deleted def CategoryTheory.fullyFaithfulSheafToPresheaf

deleted def CategoryTheory.sheafToPresheaf

Modified Mathlib/CategoryTheory/Sites/SheafHom.lean

Modified Mathlib/CategoryTheory/Sites/Sheafification.lean

Modified Mathlib/CategoryTheory/Sites/Subcanonical.lean

modified def CategoryTheory.GrothendieckTopology.yonedaEquiv

modified theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_app_apply

modified theorem CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_map

Modified Mathlib/CategoryTheory/Sites/Subsheaf.lean

Modified Mathlib/CategoryTheory/Sites/Types.lean

Modified Mathlib/CategoryTheory/Sites/Whiskering.lean

modified def CategoryTheory.sheafCompose

Modified Mathlib/Condensed/Basic.lean

added theorem Condensed.comp_hom

deleted theorem Condensed.comp_val

modified theorem Condensed.hom_ext

added theorem Condensed.id_hom

deleted theorem Condensed.id_val

Modified Mathlib/Condensed/CartesianClosed.lean

Modified Mathlib/Condensed/Discrete/Characterization.lean

Modified Mathlib/Condensed/Discrete/Colimit.lean

Modified Mathlib/Condensed/Discrete/LocallyConstant.lean

Modified Mathlib/Condensed/Discrete/Module.lean

Modified Mathlib/Condensed/Epi.lean

Modified Mathlib/Condensed/Equivalence.lean

Modified Mathlib/Condensed/Explicit.lean

modified theorem Condensed.equalizerCondition

Modified Mathlib/Condensed/Light/Basic.lean

added theorem LightCondensed.comp_hom

deleted theorem LightCondensed.comp_val

modified theorem LightCondensed.hom_ext

added theorem LightCondensed.id_hom

deleted theorem LightCondensed.id_val

Modified Mathlib/Condensed/Light/CartesianClosed.lean

Modified Mathlib/Condensed/Light/Epi.lean

Modified Mathlib/Condensed/Light/Explicit.lean

modified theorem LightCondensed.equalizerCondition

Modified Mathlib/Condensed/Light/InternallyProjective.lean

Modified Mathlib/Condensed/Light/Module.lean

Modified Mathlib/Condensed/Light/TopCatAdjunction.lean

modified theorem LightCondSet.continuous_coinducingCoprod

Modified Mathlib/Condensed/Module.lean

Modified Mathlib/Condensed/TopCatAdjunction.lean

modified theorem CondensedSet.continuous_coinducingCoprod

Modified Mathlib/Condensed/TopComparison.lean

Modified Mathlib/Geometry/Manifold/Sheaf/Basic.lean

Modified Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean

Modified Mathlib/Geometry/Manifold/Sheaf/Smooth.lean

modified def smoothSheafCommRing

modified def smoothSheafRing

Modified Mathlib/Geometry/RingedSpace/Basic.lean

Modified Mathlib/Topology/Sheaves/CommRingCat.lean

Modified Mathlib/Topology/Sheaves/Functors.lean

Modified Mathlib/Topology/Sheaves/Sheaf.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/Sites.lean

modified def TopCat.Sheaf.isTerminalOfEmpty

Modified Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean

Modified Mathlib/Topology/Sheaves/Skyscraper.lean

Modified Mathlib/Topology/Sheaves/Stalks.lean