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).
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 X
of a derivation
Instances For
The postcomposition of a derivation by a morphism of presheaves of modules.
Equations
Instances For
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
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
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
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
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
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
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
The universal derivation.
Equations
- PresheafOfModules.DifferentialsConstruction.derivation' φ' = PresheafOfModules.Derivation'.mk (fun (X : Dᵒᵖ) => CommRingCat.KaehlerDifferential.D (φ'.app X)) ⋯
Instances For
The derivation Derivation' φ'
is universal.
Equations
- One or more equations did not get rendered due to their size.