The conormal map of a local algebra at its residue field

Let R be a local k-algebra with maximal ideal 𝔪 and residue field κ. The conormal map d̄ : 𝔪/𝔪² → κ ⊗[R] Ω[R⁄k], f̄ ↦ 1 ⊗ d f, is Mathlib's kerCotangentToTensor k R κ, and it sits in the conormal exact sequence 𝔪/𝔪² → κ ⊗[R] Ω[R⁄k] → Ω[κ⁄k] → 0 ([TSPA, Tag 00RU]; Mathlib's exact_kerCotangentToTensor_mapBaseChange).

Injectivity. [TSPA, Tag 00TU] says that d̄ is injective when κ is a finitely generated separable extension of the field k. Here separability is used only through formal smoothness of κ over k [TSPA, Tag 0322], and formal smoothness produces, by lifting the identity of κ along the square-zero surjection R/𝔪² → κ, a k-algebra section σ : κ → R/𝔪². Mathlib's retractionKerCotangentToTensorEquivSection turns such a section into an R-linear retraction of d̄, so d̄ is split injective. This is [TSPA, Tag 02HP] ("a right inverse of S → S' splits the conormal sequence") with the right inverse supplied by formal smoothness instead of the explicit Hensel adjustment in the printed proof of [TSPA, Tag 00TU]. Noetherianity of R is not used.

The dimension count (the first display in the proof of [TSPA, Tag 00TV]): once d̄ is injective the conormal sequence is short exact, 0 → 𝔪/𝔪² → κ ⊗[R] Ω[R⁄k] → Ω[κ⁄k] → 0, so for R essentially of finite type over k (which makes Ω[R⁄k] a finite module) dim_κ κ ⊗[R] Ω[R⁄k] = dim_κ 𝔪/𝔪² + dim_κ Ω[κ⁄k]. To speak of κ-dimensions we repackage d̄ as the κ-linear map cotangentSpaceToTensor k R : CotangentSpace R →ₗ[κ] κ ⊗[R] Ω[R⁄k] on Mathlib's cotangent space 𝔪/𝔪² (the domain of kerCotangentToTensor is the cotangent module of ker (R → κ), which is 𝔪 by IsLocalRing.ker_residue; the transport is Ideal.cotangentEquivOfEq).

def Ideal.cotangentEquivOfEq {R : Type u} [CommRing R] {I J : Ideal R} (h : I = J) : I.Cotangent ≃ₗ[R] J.Cotangent

Transport of the cotangent module I/I² along an equality of ideals.

Equations

• Ideal.cotangentEquivOfEq h = h ▸ LinearEquiv.refl R I.Cotangent

@[simp]

theorem Ideal.cotangentEquivOfEq_toCotangent {R : Type u} [CommRing R] {I J : Ideal R} (h : I = J) (x : ↥I) : (cotangentEquivOfEq h) (I.toCotangent x) = J.toCotangent ⟨↑x, ⋯⟩

theorem IsLocalRing.ker_algebraMap_residueField (R : Type u) [CommRing R] [IsLocalRing R] : RingHom.ker (algebraMap R (ResidueField R)) = maximalIdeal R

IsLocalRing.ker_residue stated for the structure map R → κ (the same map).

theorem KaehlerDifferential.injective_kerCotangentToTensor_residueField_of_formallySmooth (k R : Type u) [CommRing k] [CommRing R] [IsLocalRing R] [Algebra k R] [Algebra.FormallySmooth k (IsLocalRing.ResidueField R)] : Function.Injective ⇑(kerCotangentToTensor k R (IsLocalRing.ResidueField R))

If the residue field κ of the local k-algebra R is formally smooth over k, the conormal map d̄ : 𝔪/𝔪² → κ ⊗[R] Ω[R⁄k] is injective ([TSPA, Tag 00TU], proved through [TSPA, Tag 02HP] with the section supplied by formal smoothness). Formal smoothness lifts the identity of κ along the square-zero surjection R/𝔪² → κ to a k-algebra section, and Mathlib's retractionKerCotangentToTensorEquivSection converts the section into a retraction of d̄.

theorem KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange_residueField (k R : Type u) [CommRing k] [CommRing R] [IsLocalRing R] [Algebra k R] : Function.Exact ⇑(kerCotangentToTensor k R (IsLocalRing.ResidueField R)) ⇑(mapBaseChange k R (IsLocalRing.ResidueField R))

The conormal sequence 𝔪/𝔪² → κ ⊗[R] Ω[R⁄k] → Ω[κ⁄k] is exact in the middle [TSPA, Tag 00RU].

theorem KaehlerDifferential.mapBaseChange_residueField_surjective (k R : Type u) [CommRing k] [CommRing R] [IsLocalRing R] [Algebra k R] : Function.Surjective ⇑(mapBaseChange k R (IsLocalRing.ResidueField R))

The map κ ⊗[R] Ω[R⁄k] → Ω[κ⁄k] of the conormal sequence is surjective [TSPA, Tag 00RU].

noncomputable def KaehlerDifferential.cotangentSpaceToTensor (k R : Type u) [CommRing k] [CommRing R] [IsLocalRing R] [Algebra k R] : IsLocalRing.CotangentSpace R →ₗ[IsLocalRing.ResidueField R] TensorProduct R (IsLocalRing.ResidueField R) Ω[R⁄k]

The conormal map d̄ as a κ-linear map on Mathlib's cotangent space 𝔪/𝔪²: the domain of kerCotangentToTensor k R κ is the cotangent module of ker (R → κ) = 𝔪.

Equations

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

theorem KaehlerDifferential.cotangentSpaceToTensor_apply (k R : Type u) [CommRing k] [CommRing R] [IsLocalRing R] [Algebra k R] (x : IsLocalRing.CotangentSpace R) : (cotangentSpaceToTensor k R) x = (kerCotangentToTensor k R (IsLocalRing.ResidueField R)) ((Ideal.cotangentEquivOfEq ⋯) x)

@[simp]

theorem KaehlerDifferential.cotangentSpaceToTensor_toCotangent (k R : Type u) [CommRing k] [CommRing R] [IsLocalRing R] [Algebra k R] (x : ↥(IsLocalRing.maximalIdeal R)) : (cotangentSpaceToTensor k R) ((IsLocalRing.maximalIdeal R).toCotangent x) = 1 ⊗ₜ[R] (D k R) ↑x

theorem KaehlerDifferential.injective_cotangentSpaceToTensor (k R : Type u) [CommRing k] [CommRing R] [IsLocalRing R] [Algebra k R] [Algebra.FormallySmooth k (IsLocalRing.ResidueField R)] : Function.Injective ⇑(cotangentSpaceToTensor k R)

theorem KaehlerDifferential.exact_cotangentSpaceToTensor_mapBaseChange (k R : Type u) [CommRing k] [CommRing R] [IsLocalRing R] [Algebra k R] : Function.Exact ⇑(cotangentSpaceToTensor k R) ⇑(mapBaseChange k R (IsLocalRing.ResidueField R))

theorem KaehlerDifferential.finrank_residueField_tensor_kaehlerDifferential (k R : Type u) [CommRing k] [CommRing R] [IsLocalRing R] [Algebra k R] [Algebra.EssFiniteType k R] [Algebra.FormallySmooth k (IsLocalRing.ResidueField R)] : Module.finrank (IsLocalRing.ResidueField R) (TensorProduct R (IsLocalRing.ResidueField R) Ω[R⁄k]) = Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R) + Module.finrank (IsLocalRing.ResidueField R) Ω[IsLocalRing.ResidueField R⁄k]

With d̄ injective (κ formally smooth over k) the conormal sequence is short exact, so dim_κ κ ⊗[R] Ω[R⁄k] = dim_κ 𝔪/𝔪² + dim_κ Ω[κ⁄k] for R essentially of finite type over k (the first display in the proof of [TSPA, Tag 00TV]).