The presheaf of differentials of a presheaf of modules

In this file, 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. We formalize the notion of universal derivation.

Geometrically, if f : X ⟶ S is a morphisms of schemes (or more generally a morphism of commutative ringed spaces), we would like to apply these definitions in the case where F is the pullback functors from open subsets of S to open subsets of X and φ is the morphism $O_S ⟶ f_* O_X$.

In order to prove that there exists a universal derivation, the target of which shall be called the presheaf of relative differentials of φ, we first study the case where F is the identity functor. In this case where we have a morphism of presheaves of commutative rings φ' : S' ⟶ R, we construct a derivation DifferentialsConstruction.derivation' which is universal. Then, the general case (TODO) shall be obtained by observing that derivations for S ⟶ F.op ⋙ R identify to derivations for S' ⟶ R where S' is the pullback by F of the presheaf of commutative rings S (the data is the same: it suffices to show that the two vanishing conditions d_app are equivalent).

structure PresheafOfModules.Derivation {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (φ : S ⟶ F.op.comp R) : Type (max (max u u₂) v)

Given a morphism of presheaves of commutative rings φ : S ⟶ F.op ⋙ R, this is the type of relative φ-derivation of a presheaf of R-modules M.

• d : {X : Dᵒᵖ} → ↑(R.obj X) →+ ↑(M.obj X)

  the underlying additive map R.obj X →+ M.obj X of a derivation

• d_mul : ∀ {X : Dᵒᵖ} (a b : ↑(R.obj X)), self.d (a * b) = a • self.d b + b • self.d a
• d_map : ∀ {X Y : Dᵒᵖ} (f : X ⟶ Y) (x : ↑(R.obj X)), self.d ((R.map f) x) = (M.map f) (self.d x)
• d_app : ∀ {X : Cᵒᵖ} (a : ↑(S.obj X)), self.d ((φ.app X) a) = 0

theorem PresheafOfModules.Derivation.ext {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R} {x y : M.Derivation φ} (d : @PresheafOfModules.Derivation.d C inst✝ D inst✝¹ S F R M φ x = @PresheafOfModules.Derivation.d C inst✝ D inst✝¹ S F R M φ y) : x = y

theorem PresheafOfModules.Derivation.congr_d {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R} {d d' : M.Derivation φ} (h : d = d') {X : Dᵒᵖ} (b : ↑(R.obj X)) : d.d b = d'.d b

@[simp]

theorem PresheafOfModules.Derivation.d_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R} (d : M.Derivation φ) (X : Dᵒᵖ) : d.d 1 = 0

def PresheafOfModules.Derivation.postcomp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M N : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R} (d : M.Derivation φ) (f : M ⟶ N) : N.Derivation φ

The postcomposition of a derivation by a morphism of presheaves of modules.

Equations

• d.postcomp f = { d := fun {X : Dᵒᵖ} => (LinearMap.toAddMonoidHom (f.app X)).comp d.d, d_mul := ⋯, d_map := ⋯, d_app := ⋯ }

@[simp]

theorem PresheafOfModules.Derivation.postcomp_d_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M N : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R} (d : M.Derivation φ) (f : M ⟶ N) {X✝ : Dᵒᵖ} (a✝ : ↑(R.obj X✝)) : (d.postcomp f).d a✝ = (f.app X✝) (d.d a✝)

structure PresheafOfModules.Derivation.Universal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R} (d : M.Derivation φ) : Type (max (max (max u u₂) (v + 1)) v₂)

The universal property that a derivation d : M.Derivation φ must satisfy so that the presheaf of modules M can be considered as the presheaf of (relative) differentials of a presheaf of commutative rings φ : S ⟶ F.op ⋙ R.

• desc : {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} → M'.Derivation φ → (M ⟶ M')

  An absolyte derivation of M' descends as a morphism M ⟶ M'.

• fac : ∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (d' : M'.Derivation φ), d.postcomp (self.desc d') = d'
• postcomp_injective : ∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (φ_1 φ' : M ⟶ M'), d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ'

instance PresheafOfModules.Derivation.instSubsingletonUniversal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R} (d : M.Derivation φ) : Subsingleton d.Universal

Equations

• ⋯ = ⋯

class PresheafOfModules.HasDifferentials {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (φ : S ⟶ F.op.comp R) : Prop

The property that there exists a universal derivation for a morphism of presheaves of commutative rings S ⟶ F.op ⋙ R.

• exists_universal_derivation : ∃ (M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (d : M.Derivation φ), Nonempty d.Universal

@[reducible, inline]

abbrev PresheafOfModules.Derivation' {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (φ' : S' ⟶ R) : Type (max (max u₂ u) v)

Given a morphism of presheaves of commutative rings φ : S ⟶ R, this is the type of relative φ-derivation of a presheaf of R-modules M.

Equations

• M.Derivation' φ' = M.Derivation φ'

@[simp]

theorem PresheafOfModules.Derivation'.d_app {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ' : S' ⟶ R} (d : M.Derivation' φ') {X : Dᵒᵖ} (a : ↑(S'.obj X)) : d.d ((φ'.app X) a) = 0

noncomputable def PresheafOfModules.Derivation'.app {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ' : S' ⟶ R} (d : M.Derivation' φ') (X : Dᵒᵖ) : (M.obj X).Derivation (φ'.app X)

The derivation relative to the morphism of commutative rings φ'.app X induced by a derivation relative to a morphism of presheaves of commutative rings.

Equations

• d.app X = ModuleCat.Derivation.mk (fun (b : ↑(R.obj X)) => d.d b) ⋯ ⋯ ⋯

@[simp]

theorem PresheafOfModules.Derivation'.app_apply {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ' : S' ⟶ R} (d : M.Derivation' φ') {X : Dᵒᵖ} (b : ↑(R.obj X)) : (d.app X).d b = d.d b

def PresheafOfModules.Derivation'.mk {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ' : S' ⟶ R} (d : (X : Dᵒᵖ) → (M.obj X).Derivation (φ'.app X)) (d_map : ∀ ⦃X Y : Dᵒᵖ⦄ (f : X ⟶ Y) (x : ↑(R.obj X)), (d Y).d ((R.map f) x) = (M.map f) ((d X).d x)) : M.Derivation' φ'

Given a morphism of presheaves of commutative rings φ', this is the in derivation M.Derivation' φ' that is given by a compatible family of derivations with values in the modules M.obj X for all X.

Equations

• PresheafOfModules.Derivation'.mk d d_map = { d := fun {X : Dᵒᵖ} => AddMonoidHom.mk' (d X).d ⋯, d_mul := ⋯, d_map := ⋯, d_app := ⋯ }

@[simp]

theorem PresheafOfModules.Derivation'.mk_app {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ' : S' ⟶ R} (d : (X : Dᵒᵖ) → (M.obj X).Derivation (φ'.app X)) (d_map : ∀ ⦃X Y : Dᵒᵖ⦄ (f : X ⟶ Y) (x : ↑(R.obj X)), (d Y).d ((R.map f) x) = (M.map f) ((d X).d x)) (X : Dᵒᵖ) : (PresheafOfModules.Derivation'.mk d d_map).app X = d X

def PresheafOfModules.Derivation'.Universal.mk {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ' : S' ⟶ R} {d : M.Derivation' φ'} (desc : {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} → M'.Derivation' φ' → (M ⟶ M')) (fac : ∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (d' : M'.Derivation' φ'), PresheafOfModules.Derivation.postcomp d (desc d') = d') (postcomp_injective : ∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (α β : M ⟶ M'), PresheafOfModules.Derivation.postcomp d α = PresheafOfModules.Derivation.postcomp d β → α = β) : PresheafOfModules.Derivation.Universal d

Constructor for Derivation.Universal in the case F is the identity functor.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PresheafOfModules.DifferentialsConstruction.relativeDifferentials' {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (φ' : S' ⟶ R) : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))

The presheaf of relative differentials of a morphism of presheaves of commutative rings.

Equations

• One or more equations did not get rendered due to their size.

theorem PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (φ' : S' ⟶ R) {X✝ Y✝ : Dᵒᵖ} (f : X✝ ⟶ Y✝) : (PresheafOfModules.DifferentialsConstruction.relativeDifferentials' φ').map f = CommRingCat.KaehlerDifferential.map ⋯

@[simp]

theorem PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_obj {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (φ' : S' ⟶ R) (X : Dᵒᵖ) : (PresheafOfModules.DifferentialsConstruction.relativeDifferentials' φ').obj X = CommRingCat.KaehlerDifferential (φ'.app X)

@[simp]

theorem PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map_d {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (φ' : S' ⟶ R) {X Y : Dᵒᵖ} (f : X ⟶ Y) (x : ↑(R.obj X)) : ((PresheafOfModules.DifferentialsConstruction.relativeDifferentials' φ').map f) (CommRingCat.KaehlerDifferential.d x) = CommRingCat.KaehlerDifferential.d ((R.map f) x)

noncomputable def PresheafOfModules.DifferentialsConstruction.derivation' {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (φ' : S' ⟶ R) : (PresheafOfModules.DifferentialsConstruction.relativeDifferentials' φ').Derivation' φ'

The universal derivation.

Equations

• PresheafOfModules.DifferentialsConstruction.derivation' φ' = PresheafOfModules.Derivation'.mk (fun (X : Dᵒᵖ) => CommRingCat.KaehlerDifferential.D (φ'.app X)) ⋯

noncomputable def PresheafOfModules.DifferentialsConstruction.isUniversal' {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (φ' : S' ⟶ R) : PresheafOfModules.Derivation.Universal (PresheafOfModules.DifferentialsConstruction.derivation' φ')

The derivation Derivation' φ' is universal.

Equations

• One or more equations did not get rendered due to their size.

instance PresheafOfModules.DifferentialsConstruction.instHasDifferentials {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (φ' : S' ⟶ R) : PresheafOfModules.HasDifferentials φ'

Equations

• ⋯ = ⋯