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