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.
the underlying additive map
R.obj X →+ M.obj Xof a derivation
Instances For
theorem
PresheafOfModules.Derivation.ext
{C : Type u₁}
:
∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : 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 φ},
@PresheafOfModules.Derivation.d C inst D inst_1 S F R M φ x = @PresheafOfModules.Derivation.d C inst D inst_1 S F R M φ y →
x = y
@[simp]
theorem
PresheafOfModules.Derivation.d_mul
{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}
(self : M.Derivation φ)
{X : Dᵒᵖ}
(a : ↑(R.obj X))
(b : ↑(R.obj X))
:
@[simp]
theorem
PresheafOfModules.Derivation.d_map
{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}
(self : M.Derivation φ)
{X : Dᵒᵖ}
{Y : Dᵒᵖ}
(f : X ⟶ Y)
(x : ↑(R.obj X))
:
self.d ((R.map f) x) = (M.map f) (self.d x)
theorem
PresheafOfModules.Derivation.d_app
{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}
(self : M.Derivation φ)
{X : Cᵒᵖ}
(a : ↑(S.obj X))
:
self.d ((φ.app X) a) = 0
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 : M.Derivation φ}
{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 : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))}
{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 := ⋯ }
Instances For
@[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 : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))}
{N : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))}
{φ : S ⟶ F.op.comp R}
(d : M.Derivation φ)
(f : M ⟶ N)
:
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 morphismM ⟶ 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 = φ'
Instances For
@[simp]
theorem
PresheafOfModules.Derivation.Universal.fac
{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 φ}
(self : d.Universal)
{M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))}
(d' : M'.Derivation φ)
:
d.postcomp (self.desc d') = d'
theorem
PresheafOfModules.Derivation.Universal.postcomp_injective
{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 φ✝}
(self : d.Universal)
{M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))}
(φ : M ⟶ M')
(φ' : M ⟶ M')
(h : d.postcomp φ = d.postcomp φ')
:
φ = φ'
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)
:
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
Instances
theorem
PresheafOfModules.HasDifferentials.exists_universal_derivation
{C : Type u₁}
:
∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : 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} [self : PresheafOfModules.HasDifferentials φ],
∃ (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' : CategoryTheory.Functor Dᵒᵖ CommRingCat}
{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 φ'
Instances For
@[simp]
theorem
PresheafOfModules.Derivation'.d_app
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S' : CategoryTheory.Functor Dᵒᵖ CommRingCat}
{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' : CategoryTheory.Functor Dᵒᵖ CommRingCat}
{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) ⋯ ⋯ ⋯
Instances For
@[simp]
theorem
PresheafOfModules.Derivation'.app_apply
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S' : CategoryTheory.Functor Dᵒᵖ CommRingCat}
{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' : CategoryTheory.Functor Dᵒᵖ CommRingCat}
{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 := ⋯ }
Instances For
@[simp]
theorem
PresheafOfModules.Derivation'.mk_app
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S' : CategoryTheory.Functor Dᵒᵖ CommRingCat}
{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' : CategoryTheory.Functor Dᵒᵖ CommRingCat}
{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 β → α = β)
:
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.
Instances For
noncomputable def
PresheafOfModules.DifferentialsConstruction.relativeDifferentials'
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S' : CategoryTheory.Functor Dᵒᵖ CommRingCat}
{R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
(φ' : S' ⟶ R)
:
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.
Instances For
theorem
PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S' : CategoryTheory.Functor Dᵒᵖ CommRingCat}
{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' : CategoryTheory.Functor Dᵒᵖ CommRingCat}
{R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
(φ' : S' ⟶ R)
(X : Dᵒᵖ)
:
@[simp]
theorem
PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map_d
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S' : CategoryTheory.Functor Dᵒᵖ CommRingCat}
{R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
(φ' : S' ⟶ R)
{X : Dᵒᵖ}
{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' : CategoryTheory.Functor Dᵒᵖ CommRingCat}
{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)) ⋯
Instances For
noncomputable def
PresheafOfModules.DifferentialsConstruction.isUniversal'
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S' : CategoryTheory.Functor Dᵒᵖ CommRingCat}
{R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
(φ' : S' ⟶ R)
:
The derivation Derivation' φ' is universal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
PresheafOfModules.DifferentialsConstruction.instHasDifferentials
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{S' : CategoryTheory.Functor Dᵒᵖ CommRingCat}
{R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
(φ' : S' ⟶ R)
:
Equations
- ⋯ = ⋯