Commit 2026-09-03 18:31 369aeb92

View on Github →

feat(Algebra/Category/ModuleCat/Differentials): refactor the presheaf of differentials to use PresheafOfModulesOfCommRing (#43195)

Estimated changes

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

deleted def PresheafOfModules.Derivation'.Universal.mk

deleted theorem PresheafOfModules.Derivation'.app_apply

deleted theorem PresheafOfModules.Derivation'.d_app

deleted def PresheafOfModules.Derivation'.mk

deleted theorem PresheafOfModules.Derivation'.mk_app

deleted structure PresheafOfModules.Derivation.Universal

deleted theorem PresheafOfModules.Derivation.congr_d

deleted theorem PresheafOfModules.Derivation.d_one

deleted def PresheafOfModules.Derivation.postcomp

deleted structure PresheafOfModules.Derivation

deleted theorem PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map_d

added def PresheafOfModulesOfCommRing.Derivation'.Universal.mk

added theorem PresheafOfModulesOfCommRing.Derivation'.app_apply

added theorem PresheafOfModulesOfCommRing.Derivation'.d_app

added def PresheafOfModulesOfCommRing.Derivation'.mk

added theorem PresheafOfModulesOfCommRing.Derivation'.mk_app

added structure PresheafOfModulesOfCommRing.Derivation.Universal

added theorem PresheafOfModulesOfCommRing.Derivation.congr_d

added theorem PresheafOfModulesOfCommRing.Derivation.d_one

added def PresheafOfModulesOfCommRing.Derivation.postcomp

added structure PresheafOfModulesOfCommRing.Derivation

added theorem PresheafOfModulesOfCommRing.DifferentialsConstruction.relativeDifferentials'_map_d