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.

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
    def ModuleCat.Derivation.mk {A : CommRingCat} {B : CommRingCat} {M : ModuleCat B} {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 : 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
        @[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'
        @[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
        @[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
        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) :

          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

              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
              Instances For
                noncomputable def ModuleCat.Derivation.desc {A : CommRingCat} {B : CommRingCat} {f : A B} {M : ModuleCat B} (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 : ModuleCat B} (D : M.Derivation f) (b : B) :