Documentation

Mathlib.RingTheory.Kaehler.Basic

The module of kaehler differentials #

Main results #

Future project #

@[reducible, inline]
noncomputable abbrev KaehlerDifferential.ideal (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :

The kernel of the multiplication map S ⊗[R] S →ₐ[R] S.

Equations
Instances For
    noncomputable def Derivation.tensorProductTo {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) :

    For a R-derivation S → M, this is the map S ⊗[R] S →ₗ[S] M sending s ⊗ₜ t ↦ s • D t.

    Equations
    Instances For
      theorem Derivation.tensorProductTo_tmul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) (s : S) (t : S) :
      D.tensorProductTo (s ⊗ₜ[R] t) = s D t
      theorem Derivation.tensorProductTo_mul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) (x : TensorProduct R S S) (y : TensorProduct R S S) :
      D.tensorProductTo (x * y) = (Algebra.TensorProduct.lmul' R) x D.tensorProductTo y + (Algebra.TensorProduct.lmul' R) y D.tensorProductTo x

      The kernel of S ⊗[R] S →ₐ[R] S is generated by 1 ⊗ s - s ⊗ 1 as a S-module.

      noncomputable def KaehlerDifferential (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :

      The module of Kähler differentials (Kahler differentials, Kaehler differentials). This is implemented as I / I ^ 2 with I the kernel of the multiplication map S ⊗[R] S →ₐ[R] S. To view elements as a linear combination of the form s • D s', use KaehlerDifferential.tensorProductTo_surjective and Derivation.tensorProductTo_tmul.

      We also provide the notation Ω[S⁄R] for KaehlerDifferential R S. Note that the slash is \textfractionsolidus.

      Equations
      Instances For

        The module of Kähler differentials (Kahler differentials, Kaehler differentials). This is implemented as I / I ^ 2 with I the kernel of the multiplication map S ⊗[R] S →ₐ[R] S. To view elements as a linear combination of the form s • D s', use KaehlerDifferential.tensorProductTo_surjective and Derivation.tensorProductTo_tmul.

        We also provide the notation Ω[S⁄R] for KaehlerDifferential R S. Note that the slash is \textfractionsolidus.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          noncomputable instance instNonemptyKaehlerDifferential (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :
          Equations
          • =
          noncomputable instance instIsScalarTowerTensorProductKaehlerDifferential (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :
          Equations
          • =
          noncomputable instance KaehlerDifferential.isScalarTower_of_tower (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {R₁ : Type u_2} {R₂ : Type u_3} [CommRing R₁] [CommRing R₂] [Algebra R₁ S] [Algebra R₂ S] [SMul R₁ R₂] [SMulCommClass R R₁ S] [SMulCommClass R R₂ S] [IsScalarTower R₁ R₂ S] :
          IsScalarTower R₁ R₂ (Ω[SR])
          Equations
          • =
          noncomputable instance KaehlerDifferential.isScalarTower' (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :
          Equations
          • =

          The quotient map I → Ω[S⁄R] with I being the kernel of S ⊗[R] S → S.

          Equations
          Instances For
            noncomputable def KaehlerDifferential.DLinearMap (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :

            (Implementation) The underlying linear map of the derivation into Ω[S⁄R].

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem KaehlerDifferential.DLinearMap_apply (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (s : S) :
              (KaehlerDifferential.DLinearMap R S) s = (KaehlerDifferential.ideal R S).toCotangent 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1,
              noncomputable def KaehlerDifferential.D (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :

              The universal derivation into Ω[S⁄R].

              Equations
              Instances For
                theorem KaehlerDifferential.D_apply (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (s : S) :
                (KaehlerDifferential.D R S) s = (KaehlerDifferential.ideal R S).toCotangent 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1,

                Ω[S⁄R] is trivial if R → S is surjective. Also see Algebra.FormallyUnramified.iff_subsingleton_kaehlerDifferential.

                noncomputable def Derivation.liftKaehlerDifferential {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) :

                The linear map from Ω[S⁄R], associated with a derivation.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem Derivation.liftKaehlerDifferential_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) (x : (KaehlerDifferential.ideal R S)) :
                  D.liftKaehlerDifferential ((KaehlerDifferential.ideal R S).toCotangent x) = D.tensorProductTo x
                  theorem Derivation.liftKaehlerDifferential_comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) :
                  D.liftKaehlerDifferential.compDer (KaehlerDifferential.D R S) = D
                  @[simp]
                  theorem Derivation.liftKaehlerDifferential_comp_D {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D' : Derivation R S M) (x : S) :
                  D'.liftKaehlerDifferential ((KaehlerDifferential.D R S) x) = D' x
                  theorem Derivation.liftKaehlerDifferential_unique_iff {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] {f : Ω[SR] →ₗ[S] M} {f' : Ω[SR] →ₗ[S] M} :
                  f = f' f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
                  theorem Derivation.liftKaehlerDifferential_unique {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (f : Ω[SR] →ₗ[S] M) (f' : Ω[SR] →ₗ[S] M) (hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)) :
                  f = f'
                  theorem Derivation.liftKaehlerDifferential_D (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :
                  (KaehlerDifferential.D R S).liftKaehlerDifferential = LinearMap.id
                  theorem KaehlerDifferential.D_tensorProductTo {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (x : (KaehlerDifferential.ideal R S)) :
                  (KaehlerDifferential.D R S).tensorProductTo x = (KaehlerDifferential.ideal R S).toCotangent x
                  noncomputable def KaehlerDifferential.linearMapEquivDerivation (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] :

                  The S-linear maps from Ω[S⁄R] to M are (S-linearly) equivalent to R-derivations from S to M.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem KaehlerDifferential.linearMapEquivDerivation_symm_apply (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) :
                    (KaehlerDifferential.linearMapEquivDerivation R S).symm D = D.liftKaehlerDifferential
                    @[simp]

                    The quotient ring of S ⊗ S ⧸ J ^ 2 by Ω[S⁄R] is isomorphic to S.

                    Equations
                    Instances For
                      noncomputable def KaehlerDifferential.quotientCotangentIdeal (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :

                      The quotient ring of S ⊗ S ⧸ J ^ 2 by Ω[S⁄R] is isomorphic to S as an S-algebra.

                      Equations
                      Instances For
                        noncomputable def smul_SSmod_SSmod (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :

                        A shortcut instance to prevent timing out. Hopefully to be removed in the future.

                        Equations
                        Instances For

                          A shortcut instance to prevent timing out. Hopefully to be removed in the future.

                          Equations
                          • =
                          Instances For

                            A shortcut instance to prevent timing out. Hopefully to be removed in the future.

                            Equations
                            • =
                            Instances For

                              A shortcut instance to prevent timing out. Hopefully to be removed in the future.

                              Equations
                              • =
                              Instances For
                                noncomputable def instS (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :
                                Module S (KaehlerDifferential.ideal R S).cotangentIdeal

                                A shortcut instance to prevent timing out. Hopefully to be removed in the future.

                                Equations
                                Instances For
                                  noncomputable def instR (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :
                                  Module R (KaehlerDifferential.ideal R S).cotangentIdeal

                                  A shortcut instance to prevent timing out. Hopefully to be removed in the future.

                                  Equations
                                  Instances For
                                    noncomputable def instSS (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :
                                    Module (TensorProduct R S S) (KaehlerDifferential.ideal R S).cotangentIdeal

                                    A shortcut instance to prevent timing out. Hopefully to be removed in the future.

                                    Equations
                                    Instances For
                                      noncomputable def KaehlerDifferential.endEquivDerivation' (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :
                                      Derivation R S (Ω[SR]) ≃ₗ[R] Derivation R S (KaehlerDifferential.ideal R S).cotangentIdeal

                                      Derivations into Ω[S⁄R] is equivalent to derivations into (KaehlerDifferential.ideal R S).cotangentIdeal.

                                      Equations
                                      Instances For
                                        noncomputable def KaehlerDifferential.endEquivAuxEquiv (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :

                                        (Implementation) An Equiv version of KaehlerDifferential.End_equiv_aux. Used in KaehlerDifferential.endEquiv.

                                        Equations
                                        Instances For
                                          noncomputable def KaehlerDifferential.endEquiv (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :
                                          Module.End S (Ω[SR]) { f : S →ₐ[R] TensorProduct R S S RingHom.ker (Algebra.TensorProduct.lmul' R).toRingHom ^ 2 // (Algebra.TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S }

                                          The endomorphisms of Ω[S⁄R] corresponds to sections of the surjection S ⊗[R] S ⧸ J ^ 2 →ₐ[R] S, with J being the kernel of the multiplication map S ⊗[R] S →ₐ[R] S.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            noncomputable instance KaehlerDifferential.finite (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] [Algebra.EssFiniteType R S] :
                                            Equations
                                            • =
                                            noncomputable def KaehlerDifferential.kerTotal (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :

                                            The S-submodule of S →₀ S (the direct sum of copies of S indexed by S) generated by the relations:

                                            1. dx + dy = d(x + y)
                                            2. x dy + y dx = d(x * y)
                                            3. dr = 0 for r ∈ R where db is the unit in the copy of S with index b.

                                            This is the kernel of the surjection Finsupp.linearCombination S Ω[S⁄R] S (KaehlerDifferential.D R S). See KaehlerDifferential.kerTotal_eq and KaehlerDifferential.linearCombination_surjective.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For

                                              The (universal) derivation into (S →₀ S) ⧸ KaehlerDifferential.kerTotal R S.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[deprecated KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination]

                                                Alias of KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination.

                                                @[deprecated KaehlerDifferential.linearCombination_surjective]

                                                Alias of KaehlerDifferential.linearCombination_surjective.

                                                Ω[S⁄R] is isomorphic to S copies of S with kernel KaehlerDifferential.kerTotal.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

                                                  Given the commutative diagram

                                                  A --→ B
                                                  ↑     ↑
                                                  |     |
                                                  R --→ S
                                                  

                                                  The kernel of the presentation ⊕ₓ B dx ↠ Ω_{B/S} is spanned by the image of the kernel of ⊕ₓ A dx ↠ Ω_{A/R} and all ds with s : S. See kerTotal_map' for the special case where R = S.

                                                  This is a special case of kerTotal_map where R = S. The kernel of the presentation ⊕ₓ B dx ↠ Ω_{B/R} is spanned by the image of the kernel of ⊕ₓ A dx ↠ Ω_{A/R} and all da with a : A.

                                                  noncomputable def KaehlerDifferential.map (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra S B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] :

                                                  The map Ω[A⁄R] →ₗ[A] Ω[B⁄S] given a square

                                                  A --→ B
                                                  ↑     ↑
                                                  |     |
                                                  R --→ S
                                                  
                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem KaehlerDifferential.map_D (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra S B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] (x : A) :
                                                    noncomputable def KaehlerDifferential.mapBaseChange (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] :

                                                    The lift of the map Ω[A⁄R] →ₗ[A] Ω[B⁄R] to the base change along A → B. This is the first map in the exact sequence B ⊗[A] Ω[A⁄R] → Ω[B⁄R] → Ω[B⁄A] → 0.

                                                    Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem KaehlerDifferential.mapBaseChange_tmul (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (x : B) (y : Ω[AR]) :

                                                      The sequence B ⊗[A] Ω[A⁄R] → Ω[B⁄R] → Ω[B⁄A] → 0 is exact. Also see KaehlerDifferential.map_surjective.

                                                      noncomputable def KaehlerDifferential.kerToTensor (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] :

                                                      The map I → B ⊗[A] B ⊗[A] Ω[A⁄R] where I = ker(A → B).

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem KaehlerDifferential.kerToTensor_apply (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] (x : (RingHom.ker (algebraMap A B))) :
                                                        noncomputable def KaehlerDifferential.kerCotangentToTensor (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] :

                                                        The map I/I² → B ⊗[A] B ⊗[A] Ω[A⁄R] where I = ker(A → B).

                                                        Equations
                                                        Instances For
                                                          @[simp]