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.

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.

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.

@[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.

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.

@[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.

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.

@[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.

@[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