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 B : CommRingCat} (M : ModuleCat ↑B) (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

• M.Derivation f = Derivation ↑A ↑B ↑M

def ModuleCat.Derivation.mk {A B : CommRingCat} {M : ModuleCat ↑B} {f : A ⟶ B} (d : ↑B → ↑M) (d_add : ∀ (b b' : ↑B), d (b + b') = d b + d b' := by simp) (d_mul : ∀ (b b' : ↑B), d (b * b') = b • d b' + b' • d b := by simp) (d_map : ∀ (a : ↑A), d ((CategoryTheory.ConcreteCategory.hom f) a) = 0 := by simp) : 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 }

def ModuleCat.Derivation.d {A B : CommRingCat} {M : ModuleCat ↑B} {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

@[simp]

theorem ModuleCat.Derivation.d_add {A B : CommRingCat} {M : ModuleCat ↑B} {f : A ⟶ B} (D : M.Derivation f) (b b' : ↑B) : D.d (b + b') = D.d b + D.d b'

@[simp]

theorem ModuleCat.Derivation.d_mul {A B : CommRingCat} {M : ModuleCat ↑B} {f : A ⟶ B} (D : M.Derivation f) (b b' : ↑B) : D.d (b * b') = b • D.d b' + b' • D.d b

@[simp]

theorem ModuleCat.Derivation.d_map {A B : CommRingCat} {M : ModuleCat ↑B} {f : A ⟶ B} (D : M.Derivation f) (a : ↑A) : D.d ((CategoryTheory.ConcreteCategory.hom f) a) = 0

noncomputable def CommRingCat.KaehlerDifferential {A B : CommRingCat} (f : A ⟶ B) : ModuleCat ↑B

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

Equations

• CommRingCat.KaehlerDifferential f = ModuleCat.of (↑B) (Ω[↑B⁄↑A])

noncomputable def CommRingCat.KaehlerDifferential.D {A B : CommRingCat} (f : A ⟶ B) : (KaehlerDifferential f).Derivation f

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

Equations

• CommRingCat.KaehlerDifferential.D f = ModuleCat.Derivation.mk (fun (b : ↑B) => (KaehlerDifferential.D ↑A ↑B) b) ⋯ ⋯ ⋯

@[reducible, inline]

noncomputable abbrev CommRingCat.KaehlerDifferential.d {A B : CommRingCat} {f : A ⟶ B} (b : ↑B) : ↑(KaehlerDifferential f)

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

Equations

• CommRingCat.KaehlerDifferential.d b = (CommRingCat.KaehlerDifferential.D f).d b

theorem CommRingCat.KaehlerDifferential.ext {A B : CommRingCat} {f : A ⟶ B} {M : ModuleCat ↑B} {α β : KaehlerDifferential f ⟶ M} (h : ∀ (b : ↑B), (CategoryTheory.ConcreteCategory.hom α) (d b) = (CategoryTheory.ConcreteCategory.hom β) (d b)) : α = β

theorem CommRingCat.KaehlerDifferential.ext_iff {A B : CommRingCat} {f : A ⟶ B} {M : ModuleCat ↑B} {α β : KaehlerDifferential f ⟶ M} : α = β ↔ ∀ (b : ↑B), (CategoryTheory.ConcreteCategory.hom α) (d b) = (CategoryTheory.ConcreteCategory.hom β) (d b)

noncomputable def CommRingCat.KaehlerDifferential.map {A B A' B' : CommRingCat} {f : A ⟶ B} {f' : A' ⟶ B'} {g : A ⟶ A'} {g' : B ⟶ B'} (fac : CategoryTheory.CategoryStruct.comp g f' = CategoryTheory.CategoryStruct.comp f g') : KaehlerDifferential f ⟶ (ModuleCat.restrictScalars (Hom.hom g')).obj (KaehlerDifferential f')

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

• CommRingCat.KaehlerDifferential.map fac = ModuleCat.ofHom { toFun := fun (x : Ω[↑B⁄↑A]) => (KaehlerDifferential.map ↑A ↑A' ↑B ↑B') x, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem CommRingCat.KaehlerDifferential.map_d {A B A' B' : CommRingCat} {f : A ⟶ B} {f' : A' ⟶ B'} {g : A ⟶ A'} {g' : B ⟶ B'} (fac : CategoryTheory.CategoryStruct.comp g f' = CategoryTheory.CategoryStruct.comp f g') (b : ↑B) : (CategoryTheory.ConcreteCategory.hom (map fac)) (d b) = d ((CategoryTheory.ConcreteCategory.hom g') b)

noncomputable def ModuleCat.Derivation.desc {A B : CommRingCat} {f : A ⟶ B} {M : ModuleCat ↑B} (D : M.Derivation f) : CommRingCat.KaehlerDifferential f ⟶ M

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

• D.desc = ModuleCat.ofHom (Derivation.liftKaehlerDifferential D)

@[simp]

theorem ModuleCat.Derivation.desc_d {A B : CommRingCat} {f : A ⟶ B} {M : ModuleCat ↑B} (D : M.Derivation f) (b : ↑B) : (CategoryTheory.ConcreteCategory.hom D.desc) (CommRingCat.KaehlerDifferential.d b) = D.d b