# The differentials of a morphism in the category of commutative rings #

In this file, given a morphism f : A ⟶ B in the category CommRingCat, and M : ModuleCat B, we define the type M.Derivation f of derivations with values in M relative to f. We also construct the module of differentials CommRingCat.KaehlerDifferential f : ModuleCat B and the corresponding derivation.

def ModuleCat.Derivation {A : CommRingCat} {B : CommRingCat} (M : ) (f : A B) :
Type (max v u)

The type of derivations with values in a B-module M relative to a morphism f : A ⟶ B in the category CommRingCat.

Equations
Instances For
def ModuleCat.Derivation.mk {A : CommRingCat} {B : CommRingCat} {M : } {f : A B} (d : BM) (d_add : autoParam (∀ (b b' : B), d (b + b') = d b + d b') _auto✝) (d_mul : autoParam (∀ (b b' : B), d (b * b') = b d b' + b' d b) _auto✝) (d_map : autoParam (∀ (a : A), d (f a) = 0) _auto✝) :
M.Derivation f

Constructor for ModuleCat.Derivation.

Equations
• ModuleCat.Derivation.mk d d_add d_mul d_map = { toFun := d, map_add' := d_add, map_smul' := , map_one_eq_zero' := , leibniz' := d_mul }
Instances For
def ModuleCat.Derivation.d {A : CommRingCat} {B : CommRingCat} {M : } {f : A B} (D : M.Derivation f) (b : B) :
M

The underlying map B → M of a derivation M.Derivation f when M : ModuleCat B and f : A ⟶ B is a morphism in CommRingCat.

Equations
• D.d b = D b
Instances For
@[simp]
theorem ModuleCat.Derivation.d_add {A : CommRingCat} {B : CommRingCat} {M : } {f : A B} (D : M.Derivation f) (b : B) (b' : B) :
D.d (b + b') = D.d b + D.d b'
@[simp]
theorem ModuleCat.Derivation.d_mul {A : CommRingCat} {B : CommRingCat} {M : } {f : A B} (D : M.Derivation f) (b : B) (b' : B) :
D.d (b * b') = b D.d b' + b' D.d b
@[simp]
theorem ModuleCat.Derivation.d_map {A : CommRingCat} {B : CommRingCat} {M : } {f : A B} (D : M.Derivation f) (a : A) :
D.d (f a) = 0
noncomputable def CommRingCat.KaehlerDifferential {A : CommRingCat} {B : CommRingCat} (f : A B) :

The module of differentials of a morphism f : A ⟶ B in the category CommRingCat.

Equations
Instances For
noncomputable def CommRingCat.KaehlerDifferential.D {A : CommRingCat} {B : CommRingCat} (f : A B) :
.Derivation f

The (universal) derivation in (KaehlerDifferential f).Derivation f when f : A ⟶ B is a morphism in the category CommRingCat.

Equations
Instances For
@[reducible, inline]
noncomputable abbrev CommRingCat.KaehlerDifferential.d {A : CommRingCat} {B : CommRingCat} {f : A B} (b : B) :

When f : A ⟶ B is a morphism in the category CommRingCat, this is the differential map B → KaehlerDifferential f.

Equations
Instances For
theorem CommRingCat.KaehlerDifferential.ext {A : CommRingCat} {B : CommRingCat} {f : A B} {M : } {α : } {β : } (h : ∀ (b : B), ) :
α = β
noncomputable def CommRingCat.KaehlerDifferential.map {A : CommRingCat} {B : CommRingCat} {A' : CommRingCat} {B' : CommRingCat} {f : A B} {f' : A' B'} {g : A A'} {g' : B B'} (fac : ) :

The map KaehlerDifferential f ⟶ (ModuleCat.restrictScalars g').obj (KaehlerDifferential f') induced by a commutative square (given by an equality g ≫ f' = f ≫ g') in the category CommRingCat.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CommRingCat.KaehlerDifferential.map_d {A : CommRingCat} {B : CommRingCat} {A' : CommRingCat} {B' : CommRingCat} {f : A B} {f' : A' B'} {g : A A'} {g' : B B'} (fac : ) (b : B) :
noncomputable def ModuleCat.Derivation.desc {A : CommRingCat} {B : CommRingCat} {f : A B} {M : } (D : M.Derivation f) :

Given f : A ⟶ B a morphism in the category CommRingCat, M : ModuleCat B, and D : M.Derivation f, this is the induced morphism CommRingCat.KaehlerDifferential f ⟶ M.

Equations
Instances For
@[simp]
theorem ModuleCat.Derivation.desc_d {A : CommRingCat} {B : CommRingCat} {f : A B} {M : } (D : M.Derivation f) (b : B) :
D.desc = D.d b