Documentation

Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

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.

source
def ModuleCat.Derivation {A : CommRingCat} {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
Instances For
    source
    def ModuleCat.Derivation.mk {A : CommRingCat} {B : CommRingCat} {M : ModuleCat ↑B} {f : A ⟶ B} (d : ↑B → ↑M) (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
      source
      def ModuleCat.Derivation.d {A : CommRingCat} {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
      Instances For
        source
        @[simp]
        theorem ModuleCat.Derivation.d_add {A : CommRingCat} {B : CommRingCat} {M : ModuleCat ↑B} {f : A ⟶ B} (D : M.Derivation f) (b : ↑B) (b' : ↑B) :
        D.d (b + b') = D.d b + D.d b'
        source
        @[simp]
        theorem ModuleCat.Derivation.d_mul {A : CommRingCat} {B : CommRingCat} {M : ModuleCat ↑B} {f : A ⟶ B} (D : M.Derivation f) (b : ↑B) (b' : ↑B) :
        D.d (b * b') = b • D.d b' + b' • D.d b
        source
        @[simp]
        theorem ModuleCat.Derivation.d_map {A : CommRingCat} {B : CommRingCat} {M : ModuleCat ↑B} {f : A ⟶ B} (D : M.Derivation f) (a : ↑A) :
        D.d (f a) = 0
        source
        noncomputable def CommRingCat.KaehlerDifferential {A : CommRingCat} {B : CommRingCat} (f : A ⟶ B) :
        ModuleCat ↑B

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

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

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

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

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

            Equations
            Instances For
              source
              theorem CommRingCat.KaehlerDifferential.ext {A : CommRingCat} {B : CommRingCat} {f : A ⟶ B} {M : ModuleCat ↑B} {α : CommRingCat.KaehlerDifferential f ⟶ M} {β : CommRingCat.KaehlerDifferential f ⟶ M} (h : ∀ (b : ↑B), α (CommRingCat.KaehlerDifferential.d b) = β (CommRingCat.KaehlerDifferential.d b)) :
              α = β
              source
              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 : CategoryTheory.CategoryStruct.comp g f' = CategoryTheory.CategoryStruct.comp f g') :
              CommRingCat.KaehlerDifferential f ⟶ (ModuleCat.restrictScalars g').obj (CommRingCat.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
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[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 : CategoryTheory.CategoryStruct.comp g f' = CategoryTheory.CategoryStruct.comp f g') (b : ↑B) :
                (CommRingCat.KaehlerDifferential.map fac) (CommRingCat.KaehlerDifferential.d b) = CommRingCat.KaehlerDifferential.d (g' b)
                source
                noncomputable def ModuleCat.Derivation.desc {A : CommRingCat} {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
                Instances For
                  source
                  @[simp]
                  theorem ModuleCat.Derivation.desc_d {A : CommRingCat} {B : CommRingCat} {f : A ⟶ B} {M : ModuleCat ↑B} (D : M.Derivation f) (b : ↑B) :
                  D.desc (CommRingCat.KaehlerDifferential.d b) = D.d b