Coefficient fields of complete local rings

Let R be a local ring which is complete for the adic topology of its maximal ideal 𝔪, and let k → R be a ring homomorphism such that the residue field R ⧸ 𝔪 is formally étale over k; the main case is a field k over which R ⧸ 𝔪 is separable (Algebra.FormallyEtale.of_isSeparable). Then reduction R → R ⧸ 𝔪 has a unique k-algebra section: the residue field lifts to a coefficient field of R containing the image of k.

Existence is Hensel's lemma in the guise of formal smoothness: the identity of R ⧸ 𝔪 lifts along the 𝔪-adically complete ring R (Algebra.FormallySmooth.exists_mkₐ_comp_eq_of_isAdicComplete). Uniqueness only needs formal unramifiedness and the Krull intersection ⋂ 𝔪 ^ n = 0.

Without separability the section need not exist over k: in 𝔽_p(s)[[T]], viewed as an 𝔽_p(u)-algebra through u ↦ s ^ p + T, a section would send s to a p-th root of s ^ p + T, and there is none, since every p-th power in 𝔽_p(s)[[T]] is a power series in T ^ p.

Over a perfect field k every residue field is formally smooth (TauCeti.formallySmooth_of_perfectField), so a k-algebra section always exists, although it need no longer be unique. Applied to the prime field, this is Cohen's theorem that a complete local ring containing a field has a coefficient field (TauCeti.exists_residueFieldSection). Such a coefficient field need not contain the image of the given field.

In the theory of algebraic function fields this is the device that turns the completion of the function field at a place with residue field F_P into a field of Laurent series over F_P, and so gives F_P-valued expansion coefficients and residues at places that are not rational.

Any coefficient field, together with finitely many generators of 𝔪, presents R as a quotient of a power series ring over its residue field: this is MvPowerSeries.exists_surjective_ringHom_of_isAdicComplete with I := 𝔪. Together with Cohen's theorem it gives the Cohen structure theorem for complete local rings containing a field (TauCeti.exists_surjective_mvPowerSeries_of_span_eq_maximalIdeal). The number of variables can be taken to be the minimal number of generators of 𝔪 (TauCeti.exists_surjective_mvPowerSeries_spanFinrank). A ring of prime characteristic p contains the field 𝔽_p, so this applies to every complete Noetherian local ring of characteristic p. No regularity is involved: for instance k[ε]/(ε²) is the quotient k⟦X⟧/(X²).

Main definitions

• TauCeti.residueFieldSection: the coefficient field, as a k-algebra map ResidueField R →ₐ[k] R.

Main results

• TauCeti.residue_residueFieldSection: it is a section of reduction.
• TauCeti.eq_residueFieldSection: it is the only k-algebra section of reduction.
• TauCeti.exists_residueFieldSection: Cohen's theorem, a complete local ring containing a field has a coefficient field.
• TauCeti.exists_surjective_mvPowerSeries_of_span_eq_maximalIdeal: the Cohen structure theorem, such a ring is a quotient of a power series ring over its residue field, with the variables sent to any given finite generating family of 𝔪.
• TauCeti.exists_surjective_mvPowerSeries_spanFinrank: the same with spanFinrank 𝔪 variables.

References

• I. S. Cohen, On the structure and ideal theory of complete local rings, Trans. Amer. Math. Soc. 59 (1946), 54–106.
• J.-P. Serre, Local Fields, GTM 67, Springer, 1979, Chapter II, §4.
• Stacks Project, Tag 032A, the Cohen structure theorem.

noncomputable def TauCeti.residueFieldSection (k : Type u_1) (R : Type u_2) [CommRing k] [CommRing R] [IsLocalRing R] [Algebra k R] [IsAdicComplete (IsLocalRing.maximalIdeal R) R] [Algebra.FormallySmooth k (IsLocalRing.ResidueField R)] : IsLocalRing.ResidueField R →ₐ[k] R

The coefficient field of a complete local k-algebra R whose residue field is formally smooth over k (for instance a field separable over a field k): a k-algebra section ResidueField R →ₐ[k] R of reduction (TauCeti.residue_residueFieldSection). When the residue field is moreover formally unramified over k it is the only one (TauCeti.eq_residueFieldSection).

@[simp]

theorem TauCeti.residue_residueFieldSection (k : Type u_1) (R : Type u_2) [CommRing k] [CommRing R] [IsLocalRing R] [Algebra k R] [IsAdicComplete (IsLocalRing.maximalIdeal R) R] [Algebra.FormallySmooth k (IsLocalRing.ResidueField R)] (a : IsLocalRing.ResidueField R) : (IsLocalRing.residue R) ((residueFieldSection k R) a) = a

The coefficient field is a section of reduction.

theorem TauCeti.eq_residueFieldSection (k : Type u_1) (R : Type u_2) [CommRing k] [CommRing R] [IsLocalRing R] [Algebra k R] [IsAdicComplete (IsLocalRing.maximalIdeal R) R] [Algebra.FormallySmooth k (IsLocalRing.ResidueField R)] [Algebra.FormallyUnramified k (IsLocalRing.ResidueField R)] {s : IsLocalRing.ResidueField R →ₐ[k] R} (hs : ∀ (a : IsLocalRing.ResidueField R), (IsLocalRing.residue R) (s a) = a) : s = residueFieldSection k R

The coefficient field is the only k-algebra section of reduction when the residue field is formally étale over k. Uniqueness uses only the Krull intersection ⋂ 𝔪 ^ n = 0.

theorem TauCeti.exists_residueFieldSection (k : Type u_1) (R : Type u_2) [Field k] [CommRing R] [IsLocalRing R] [Algebra k R] [IsAdicComplete (IsLocalRing.maximalIdeal R) R] : ∃ (s : IsLocalRing.ResidueField R →+* R), ∀ (a : IsLocalRing.ResidueField R), (IsLocalRing.residue R) (s a) = a

Cohen's theorem: a complete local ring containing a field has a coefficient field. If the complete local ring R is an algebra over some field k, then reduction R → ResidueField R has a ring homomorphism section. When k is perfect, TauCeti.residueFieldSection k R is even a k-algebra section. In general a k-linear section need not exist.

theorem TauCeti.exists_surjective_mvPowerSeries_of_span_eq_maximalIdeal (k : Type u_1) (R : Type u_2) [Field k] [CommRing R] [IsLocalRing R] [Algebra k R] [IsAdicComplete (IsLocalRing.maximalIdeal R) R] {σ : Type u_3} [Finite σ] (x : σ → R) (hx : Ideal.span (Set.range x) = IsLocalRing.maximalIdeal R) : ∃ (s : IsLocalRing.ResidueField R →+* R), (∀ (a : IsLocalRing.ResidueField R), (IsLocalRing.residue R) (s a) = a) ∧ ∃ (φ : MvPowerSeries σ (IsLocalRing.ResidueField R) →+* R), Function.Surjective ⇑φ ∧ φ.comp MvPowerSeries.C = s ∧ ∀ (i : σ), φ (MvPowerSeries.X i) = x i

Cohen structure theorem for complete local rings containing a field. Let R be a complete local ring containing a field, and let a finite family x generate its maximal ideal. Then R has a coefficient field s, and there is a surjective ring homomorphism from the power series ring over the residue field onto R that is s on constants and sends each variable X i to x i. Such a surjection exists for every coefficient field (MvPowerSeries.exists_surjective_ringHom_of_isAdicComplete).

theorem TauCeti.exists_surjective_mvPowerSeries_spanFinrank (k : Type u_1) (R : Type u_2) [Field k] [CommRing R] [IsLocalRing R] [Algebra k R] [IsAdicComplete (IsLocalRing.maximalIdeal R) R] (hfg : (IsLocalRing.maximalIdeal R).FG) : ∃ (s : IsLocalRing.ResidueField R →+* R), (∀ (a : IsLocalRing.ResidueField R), (IsLocalRing.residue R) (s a) = a) ∧ ∃ (φ : MvPowerSeries (Fin (Submodule.spanFinrank (IsLocalRing.maximalIdeal R))) (IsLocalRing.ResidueField R) →+* R), Function.Surjective ⇑φ ∧ φ.comp MvPowerSeries.C = s ∧ Ideal.span (Set.range fun (i : Fin (Submodule.spanFinrank (IsLocalRing.maximalIdeal R))) => φ (MvPowerSeries.X i)) = IsLocalRing.maximalIdeal R

Cohen structure theorem with the minimal number of variables. A complete local ring containing a field whose maximal ideal 𝔪 is finitely generated has a coefficient field s and is a quotient of the power series ring over its residue field in spanFinrank 𝔪 variables, by a surjection which is s on constants and sends the variables to generators of 𝔪.