Differentials and regularity of a localized polynomial ring

The ambient ring of the Jacobian arguments of this directory is P = k[x_i]_Q, the polynomial ring over the field k localized at a prime Q. Two facts about it [TSPA, Tags 00RX, 00RT]: Ω[P⁄k] is free on the d x_i, because Ω of a polynomial ring is free on the d x_i and Ω commutes with localization (Mathlib's mvPolynomialBasis and isLocalizedModule_map, combined by Basis.ofIsLocalizedModule); and κ(Q) ⊗[P] Ω[P⁄k] has the basis 1 ⊗ d x_i (base change of a basis). Third, P is a regular local ring: a field is a regular ring (Mathlib, through its instance chain for Dedekind domains), a polynomial ring over a regular ring is regular (Mathlib), and a localization of a regular ring at a prime is regular local by definition of IsRegularRing.

theorem KaehlerDifferential.mvPolynomialBasis_repr_D_apply {R : Type u} [CommRing R] {σ : Type v} (x : MvPolynomial σ R) (i : σ) : ((mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) x)) i = (MvPolynomial.pderiv i) x

The i-th coordinate of d x in the basis d x_j of Ω[R[x_j] ⁄ R] is ∂x/∂x_i ([TSPA, Tag 00RX], "d f = ∑ (∂f/∂x_i) d x_i").

noncomputable def KaehlerDifferential.mvPolynomialLocalizationBasis {k : Type u} [CommRing k] {ι : Type v} (Q : Ideal (MvPolynomial ι k)) [Q.IsPrime] : Module.Basis ι (Localization.AtPrime Q) Ω[Localization.AtPrime Q⁄k]

The basis d x_i of Ω[k[x_i]_Q ⁄ k], the localization of the basis d x_i of Ω[k[x_i] ⁄ k] [TSPA, Tags 00RX, 00RT].

Equations

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

@[simp]

theorem KaehlerDifferential.mvPolynomialLocalizationBasis_apply {k : Type u} [CommRing k] {ι : Type v} (Q : Ideal (MvPolynomial ι k)) [Q.IsPrime] (i : ι) : (mvPolynomialLocalizationBasis Q) i = (D k (Localization.AtPrime Q)) ((algebraMap (MvPolynomial ι k) (Localization.AtPrime Q)) (MvPolynomial.X i))

theorem KaehlerDifferential.mvPolynomialLocalizationBasis_repr_D {k : Type u} [CommRing k] {ι : Type v} (Q : Ideal (MvPolynomial ι k)) [Q.IsPrime] (x : MvPolynomial ι k) (i : ι) : ((mvPolynomialLocalizationBasis Q).repr ((D k (Localization.AtPrime Q)) ((algebraMap (MvPolynomial ι k) (Localization.AtPrime Q)) x))) i = (algebraMap (MvPolynomial ι k) (Localization.AtPrime Q)) ((MvPolynomial.pderiv i) x)

The coordinates of d f in the basis d x_i of Ω[k[x]_Q ⁄ k] are the partial derivatives ∂f/∂x_i [TSPA, Tag 00RX].

noncomputable def KaehlerDifferential.residueFieldTensorMvPolynomialLocalizationBasis {k : Type u} [CommRing k] {ι : Type v} (Q : Ideal (MvPolynomial ι k)) [Q.IsPrime] : Module.Basis ι Q.ResidueField (TensorProduct (Localization.AtPrime Q) Q.ResidueField Ω[Localization.AtPrime Q⁄k])

The basis 1 ⊗ d x_i of κ(Q) ⊗[P] Ω[P⁄k], P = k[x_i]_Q (base change of a basis).

Equations

• KaehlerDifferential.residueFieldTensorMvPolynomialLocalizationBasis Q = Module.Basis.baseChange Q.ResidueField (KaehlerDifferential.mvPolynomialLocalizationBasis Q)

@[simp]

theorem KaehlerDifferential.residueFieldTensorMvPolynomialLocalizationBasis_apply {k : Type u} [CommRing k] {ι : Type v} (Q : Ideal (MvPolynomial ι k)) [Q.IsPrime] (i : ι) : (residueFieldTensorMvPolynomialLocalizationBasis Q) i = 1 ⊗ₜ[Localization.AtPrime Q] (D k (Localization.AtPrime Q)) ((algebraMap (MvPolynomial ι k) (Localization.AtPrime Q)) (MvPolynomial.X i))

theorem KaehlerDifferential.residueFieldTensorMvPolynomialLocalizationBasis_repr_tmul_D {k : Type u} [CommRing k] {ι : Type v} (Q : Ideal (MvPolynomial ι k)) [Q.IsPrime] (x : MvPolynomial ι k) (i : ι) : ((residueFieldTensorMvPolynomialLocalizationBasis Q).repr (1 ⊗ₜ[Localization.AtPrime Q] (D k (Localization.AtPrime Q)) ((algebraMap (MvPolynomial ι k) (Localization.AtPrime Q)) x))) i = (algebraMap (MvPolynomial ι k) Q.ResidueField) ((MvPolynomial.pderiv i) x)

The coordinates of 1 ⊗ d f in the basis 1 ⊗ d x_i of κ(Q) ⊗[P] Ω[P⁄k] are the residues ∂f/∂x_i mod Q; this is how the Jacobian minor enters the proof that smooth implies regular.

theorem MvPolynomial.isRegularLocalRing_localization_atPrime {k : Type u} [Field k] {ι : Type v} [Finite ι] (Q : Ideal (MvPolynomial ι k)) [Q.IsPrime] : IsRegularLocalRing (Localization.AtPrime Q)

For a field k and a prime Q of k[x_1, …, x_N], the localization k[x]_Q is a regular local ring (the regularity of the ambient ring in the proof of [TSPA, Tag 00TS]).