Documentation

Mathlib.RingTheory.Kaehler.CotangentComplex

Naive cotangent complex associated to a presentation. #

Given a presentation 0 → I → R[x₁,...,xₙ] → S → 0 (or equivalently a closed embedding S ↪ Aⁿ defined by I), we may define the (naive) cotangent complex I/I² → ⨁ᵢ S dxᵢ → Ω[S/R] → 0.

Main results #

Implementation detail #

We actually develop these material for general extensions (i.e. surjection P → S) so that we can apply them to infinitesimal smooth (or versal) extensions later.

@[reducible, inline]
abbrev Algebra.Extension.CotangentSpace {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) :
Type (max w v)

The cotangent space on P = R[X]. This is isomorphic to Sⁿ with n being the number of variables of P.

Equations
Instances For
    noncomputable def Algebra.Extension.cotangentComplex {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) :
    P.Cotangent →ₗ[S] P.CotangentSpace

    The cotangent complex given by a presentation R[X] → S (i.e. a closed embedding S ↪ Aⁿ).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem Algebra.Extension.cotangentComplex_mk {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) (x : P.ker) :
      P.cotangentComplex (Algebra.Extension.Cotangent.mk x) = 1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x
      noncomputable def Algebra.Extension.CotangentSpace.map {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') :
      P.CotangentSpace →ₗ[S] P'.CotangentSpace

      This is the map on the cotangent space associated to a map of presentation. The matrix associated to this map is the Jacobian matrix. See CotangentSpace.repr_map.

      Equations
      Instances For
        @[simp]
        theorem Algebra.Extension.CotangentSpace.map_tmul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') (x : S) (y : P.Ring) :
        (Algebra.Extension.CotangentSpace.map f) (x ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) y) = (algebraMap S S') x ⊗ₜ[P'.Ring] (KaehlerDifferential.D R' P'.Ring) (f.toAlgHom y)
        theorem Algebra.Extension.CotangentSpace.map_comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] {R'' : Type u''} {S'' : Type v''} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [Algebra R R''] [Algebra S S''] [Algebra R S''] [IsScalarTower R R'' S''] [Algebra R' R''] [Algebra S' S''] [Algebra R' S''] [IsScalarTower R' R'' S''] [IsScalarTower R R' R''] [IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P'') :
        theorem Algebra.Extension.CotangentSpace.map_comp_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] {R'' : Type u''} {S'' : Type v''} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [Algebra R R''] [Algebra S S''] [Algebra R S''] [IsScalarTower R R'' S''] [Algebra R' R''] [Algebra S' S''] [Algebra R' S''] [IsScalarTower R' R'' S''] [IsScalarTower R R' R''] [IsScalarTower S S' S''] (f : P.Hom P') (g : P'.Hom P'') (x : P.CotangentSpace) :
        theorem Algebra.Extension.CotangentSpace.map_cotangentComplex {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') (x : P.Cotangent) :
        (Algebra.Extension.CotangentSpace.map f) (P.cotangentComplex x) = P'.cotangentComplex ((Algebra.Extension.Cotangent.map f) x)
        theorem Algebra.Extension.CotangentSpace.map_comp_cotangentComplex {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f : P.Hom P') :
        Algebra.Extension.CotangentSpace.map f ∘ₗ P.cotangentComplex = S P'.cotangentComplex ∘ₗ Algebra.Extension.Cotangent.map f
        theorem Algebra.Extension.Hom.sub_aux {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f g : P.Hom P') (x y : P.Ring) :
        f.toAlgHom (x * y) - g.toAlgHom (x * y) - (P' ((algebraMap P.Ring S') x) * (f.toAlgHom y - g.toAlgHom y) + P' ((algebraMap P.Ring S') y) * (f.toAlgHom x - g.toAlgHom x)) P'.ker ^ 2
        noncomputable def Algebra.Extension.Hom.subToKer {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f g : P.Hom P') :
        P.Ring →ₗ[R] P'.ker

        If f and g are two maps P → P' between presentations, then the image of f - g is in the kernel of P' → S.

        Equations
        Instances For
          @[simp]
          theorem Algebra.Extension.Hom.subToKer_apply_coe {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] (f g : P.Hom P') (c : P.Ring) :
          ((f.subToKer g) c) = f.toRingHom c - g.toRingHom c
          noncomputable def Algebra.Extension.Hom.sub {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f g : P.Hom P') :
          P.CotangentSpace →ₗ[S] P'.Cotangent

          If f and g are two maps P → P' between presentations, their difference induces a map P.CotangentSpace →ₗ[S] P'.Cotangent that makes two maps between the cotangent complexes homotopic.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem Algebra.Extension.Hom.sub_one_tmul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f g : P.Hom P') (x : P.Ring) :
            (f.sub g) (1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x) = Algebra.Extension.Cotangent.mk ((f.subToKer g) x)
            @[simp]
            theorem Algebra.Extension.Hom.sub_tmul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f g : P.Hom P') (r : S) (x : P.Ring) :
            (f.sub g) (r ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x) = r Algebra.Extension.Cotangent.mk ((f.subToKer g) x)
            theorem Algebra.Extension.CotangentSpace.map_sub_map {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f g : P.Hom P') :
            theorem Algebra.Extension.Cotangent.map_sub_map {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f g : P.Hom P') :
            @[reducible, inline]
            noncomputable abbrev Algebra.Extension.toKaehler {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) :
            P.CotangentSpace →ₗ[S] Ω[SR]

            The projection map from the relative cotangent space to the module of differentials.

            Equations
            Instances For
              theorem Algebra.Extension.exact_cotangentComplex_toKaehler {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} :
              Function.Exact P.cotangentComplex P.toKaehler
              noncomputable def Algebra.Extension.H1Cotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) :

              The first homology of the (naive) cotangent complex of S over R, induced by a given presentation 0 → I → P → R → 0, defined as the kernel of I/I² → S ⊗[P] Ω[P⁄R].

              Equations
              Instances For
                noncomputable instance Algebra.Extension.instAddCommGroupH1Cotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} :
                AddCommGroup P.H1Cotangent
                Equations
                • Algebra.Extension.instAddCommGroupH1Cotangent = id inferInstance
                noncomputable instance Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R₀ : Type u_2} [CommRing R₀] [Algebra R₀ S] [Module R₀ P.Cotangent] [IsScalarTower R₀ S P.Cotangent] :
                Module R₀ P.H1Cotangent
                Equations
                • Algebra.Extension.instModuleH1CotangentOfIsScalarTowerCotangent = id inferInstance
                @[simp]
                theorem Algebra.Extension.H1Cotangent.val_add {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} (x y : P.H1Cotangent) :
                (x + y) = x + y
                @[simp]
                theorem Algebra.Extension.H1Cotangent.val_zero {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} :
                0 = 0
                @[simp]
                theorem Algebra.Extension.H1Cotangent.val_smul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R₀ : Type u_1} [CommRing R₀] [Algebra R₀ S] [Module R₀ P.Cotangent] [IsScalarTower R₀ S P.Cotangent] (r : R₀) (x : P.H1Cotangent) :
                (r x) = r x
                noncomputable instance Algebra.Extension.instIsScalarTowerH1CotangentOfCotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} {R₁ : Type u_1} {R₂ : Type u_2} [CommRing R₁] [CommRing R₂] [Algebra R₁ R₂] [Algebra R₁ S] [Algebra R₂ S] [Module R₁ P.Cotangent] [IsScalarTower R₁ S P.Cotangent] [Module R₂ P.Cotangent] [IsScalarTower R₂ S P.Cotangent] [IsScalarTower R₁ R₂ P.Cotangent] :
                IsScalarTower R₁ R₂ P.H1Cotangent
                Equations
                • =
                theorem Algebra.Extension.subsingleton_h1Cotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Extension R S) :
                Subsingleton P.H1Cotangent Function.Injective P.cotangentComplex
                def Algebra.Extension.h1Cotangentι {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} :
                P.H1Cotangent →ₗ[S] P.Cotangent

                The inclusion of H¹(L_{S/R}) into the conormal space of a presentation.

                Equations
                • Algebra.Extension.h1Cotangentι = (LinearMap.ker P.cotangentComplex).subtype
                Instances For
                  @[simp]
                  theorem Algebra.Extension.h1Cotangentι_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} (self : (LinearMap.ker P.cotangentComplex)) :
                  Algebra.Extension.h1Cotangentι self = self
                  theorem Algebra.Extension.h1Cotangentι_injective {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} :
                  Function.Injective Algebra.Extension.h1Cotangentι
                  theorem Algebra.Extension.h1Cotangentι_ext {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Extension R S} (x y : P.H1Cotangent) (e : x = y) :
                  x = y
                  noncomputable def Algebra.Extension.H1Cotangent.map {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] {P : Algebra.Extension R S} (f : P.Hom P') :
                  P.H1Cotangent →ₗ[S] P'.H1Cotangent

                  The induced map on the first homology of the (naive) cotangent complex.

                  Equations
                  Instances For
                    @[simp]
                    theorem Algebra.Extension.H1Cotangent.map_apply_coe {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] {P : Algebra.Extension R S} (f : P.Hom P') (c : (LinearMap.ker P.cotangentComplex)) :
                    theorem Algebra.Extension.H1Cotangent.map_eq {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] {P : Algebra.Extension R S} (f g : P.Hom P') :
                    theorem Algebra.Extension.H1Cotangent.map_comp {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Extension R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] {R'' : Type u''} {S'' : Type v''} [CommRing R''] [CommRing S''] [Algebra R'' S''] {P'' : Algebra.Extension R'' S''} [Algebra R R''] [Algebra S S''] [Algebra R S''] [IsScalarTower R R'' S''] [Algebra R' R''] [Algebra S' S''] [Algebra R' S''] [IsScalarTower R' R'' S''] [IsScalarTower R R' R''] [IsScalarTower S S' S''] {P : Algebra.Extension R S} (f : P.Hom P') (g : P'.Hom P'') :
                    noncomputable def Algebra.Generators.cotangentSpaceBasis {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) :
                    Basis P.vars S P.toExtension.CotangentSpace

                    The canonical basis on the CotangentSpace.

                    Equations
                    Instances For
                      @[simp]
                      theorem Algebra.Generators.cotangentSpaceBasis_repr_tmul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) (r : S) (x : P.Ring) (i : P.vars) :
                      (P.cotangentSpaceBasis.repr (r ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x)) i = r * (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv i) x)
                      theorem Algebra.Generators.cotangentSpaceBasis_repr_one_tmul {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) (x : P.toExtension.Ring) (i : P.vars) :
                      (P.cotangentSpaceBasis.repr (1 ⊗ₜ[P.toExtension.Ring] (KaehlerDifferential.D R P.toExtension.Ring) x)) i = (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv i) x)
                      theorem Algebra.Generators.cotangentSpaceBasis_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) (i : P.vars) :
                      P.cotangentSpaceBasis i = 1 ⊗ₜ[P.toExtension.Ring] (KaehlerDifferential.D R P.toExtension.Ring) (MvPolynomial.X i)
                      @[simp]
                      theorem Algebra.Generators.repr_CotangentSpaceMap {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {P : Algebra.Generators R S} {R' : Type u'} {S' : Type v'} [CommRing R'] [CommRing S'] [Algebra R' S'] {P' : Algebra.Generators R' S'} [Algebra R R'] [Algebra S S'] [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f : P.Hom P') (i : P.vars) (j : P'.vars) :
                      (P'.cotangentSpaceBasis.repr ((Algebra.Extension.CotangentSpace.map f.toExtensionHom) (P.cotangentSpaceBasis i))) j = (MvPolynomial.aeval P'.val) ((MvPolynomial.pderiv j) (f.val i))
                      noncomputable def Algebra.Generators.H1Cotangent.equiv {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) (P' : Algebra.Generators R S) :
                      P.toExtension.H1Cotangent ≃ₗ[S] P'.toExtension.H1Cotangent

                      H¹(L_{S/R}) is independent of the presentation chosen.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem Algebra.Generators.H1Cotangent.equiv_apply {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) (P' : Algebra.Generators R S) (c : (LinearMap.ker P.toExtension.cotangentComplex)) :
                        (Algebra.Generators.H1Cotangent.equiv P P') c = (Algebra.Extension.Cotangent.map (P.defaultHom P').toExtensionHom) c,
                        @[reducible, inline]
                        abbrev Algebra.H1Cotangent (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] :
                        Type (max u v)

                        H¹(L_{S/R}), the first homology of the (naive) cotangent complex of S over R.

                        Equations
                        Instances For
                          noncomputable def Algebra.H1Cotangent.map (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (S' : Type u_1) [CommRing S'] [Algebra R S'] (T : Type w) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra S' T] [IsScalarTower R S' T] :

                          The induced map on the first homology of the (naive) cotangent complex of S over R.

                          Equations
                          Instances For
                            @[reducible, inline]
                            noncomputable abbrev Algebra.Generators.equivH1Cotangent {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.Generators R S) :
                            P.toExtension.H1Cotangent ≃ₗ[S] Algebra.H1Cotangent R S

                            H¹(L_{S/R}) is independent of the presentation chosen.

                            Equations
                            Instances For