Commit 2024-06-25 14:40 6d4ab88d

View on Github →

feat: relative differentials as a presheaf of modules (#14014) In this PR, we define the type M.Derivation φ of derivations with values in a presheaf of R-modules M relative to a morphism of φ : S ⟶ F.op ⋙ R of presheaves of commutative rings over categories C and D that are related by a functor F : C ⥤ D. In the particular case F is the identity functor, we construct the universal derivation.

Estimated changes

Modified Mathlib.lean

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

added def PresheafOfModules.Derivation'.Universal.mk

added theorem PresheafOfModules.Derivation'.app_apply

added def PresheafOfModules.Derivation'.mk

added theorem PresheafOfModules.Derivation'.mk_app

added structure PresheafOfModules.Derivation.Universal

added theorem PresheafOfModules.Derivation.congr_d

added theorem PresheafOfModules.Derivation.d_one

added def PresheafOfModules.Derivation.postcomp

added structure PresheafOfModules.Derivation

added theorem PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map_apply

added theorem PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map_d

added theorem PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_obj

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