A coefficient field of the completion

Kollár identifies Ô_{p,X} with k(p)⟦x₁, …, xₙ⟧ [Kol07, Definition 55]; the first step is a coefficient field: a subfield k' ⊆ R̂ mapping isomorphically onto the residue field K = R̂/𝔪R̂ = R/𝔪. Kollár obtains it for K/k finite by Hensel's lemma; the route taken here, valid for every residue field of characteristic zero, uses formal smoothness: in characteristic zero every field extension K/ℚ is separably generated, hence formally smooth over ℚ (Algebra.FormallySmooth.of_algebraicIndependent_of_isSeparable applied to a transcendence basis; [TSPA, Tag 0322]), and a formally smooth algebra lifts along the surjection R̂ → R̂/𝔪R̂ of the 𝔪R̂-adically complete ring R̂ (Algebra.FormallySmooth.exists_mkₐ_comp_eq_of_isAdicComplete). The lift K → R̂ of the identification K = R/𝔪 ≅ R̂/𝔪R̂ is the coefficient field.

This confines the route to regular local rings containing ℚ ([Algebra ℚ R]), the equicharacteristic-zero case of the sources. The Cohen structure theorem itself (Hironaka/Algebra/Local/CohenMap.lean, Cohen.lean, CohenIso.lean) is stated for an arbitrary coefficient field, IsCoefficientAlgebra R below, because the completed chart map (Hironaka/Algebra/Local/ChartCompletion.lean) needs it for the coefficient field of the chart's local ring transported from that of R̂; the ℚ-hypothesis is used only to produce one (coefficientField).

theorem IsLocalRing.formallySmooth_rat_of_field (K : Type u_1) [Field K] [Algebra ℚ K] : Algebra.FormallySmooth ℚ K

A field of characteristic zero is formally smooth over ℚ, being separably generated ([TSPA, Tag 0322]): algebraic extensions in characteristic zero are separable.

noncomputable def IsLocalRing.residueFieldEquiv (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] : ResidueField R ≃+* ResidueField (AdicCompletion (maximalIdeal R) R)

The residue field of R̂ is that of R, as a ring isomorphism.

Equations

• IsLocalRing.residueFieldEquiv R = RingEquiv.ofBijective (IsLocalRing.ResidueField.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R))) ⋯

@[reducible, inline]

abbrev IsLocalRing.IsCoefficientAlgebra (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)] : Prop

A coefficient field of R̂ (Kollár's "field of representatives", [Kol07, Definition 55]) is a subfield mapping isomorphically onto the residue field K = R̂/𝔪R̂ = R/𝔪. Here it is a K-algebra structure on R̂ which is a section of the residue map (any such structure; one exists for ℚ ⊆ R, coefficientField below). The Cohen structure theorem is stated for an arbitrary coefficient field because the completed chart map needs it for the coefficient field of R'_{𝔪'} transported from that of R̂.

Equations

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

theorem IsLocalRing.sub_algebraMap_mem_maximalIdeal (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)] (hι : IsCoefficientAlgebra R) (y : AdicCompletion (maximalIdeal R) R) : y - (algebraMap (ResidueField R) (AdicCompletion (maximalIdeal R) R)) ((residueFieldEquiv R).symm ((residue (AdicCompletion (maximalIdeal R) R)) y)) ∈ maximalIdeal (AdicCompletion (maximalIdeal R) R)

Every element of R̂ is a constant from the coefficient field plus an element of 𝔪R̂: R̂ = σ(K) + 𝔪R̂, for any coefficient field.

theorem IsLocalRing.exists_coefficientField (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [Algebra ℚ R] : ∃ (σ : ResidueField R →+* AdicCompletion (maximalIdeal R) R), ∀ (k : ResidueField R), (residue (AdicCompletion (maximalIdeal R) R)) (σ k) = (residueFieldEquiv R) k

A coefficient field of R̂ exists — a ring map K → R̂ from the residue field which is a section of the residue map R̂ → R̂/𝔪R̂ = K — when R contains ℚ.

noncomputable def IsLocalRing.coefficientField (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [Algebra ℚ R] : ResidueField R →+* AdicCompletion (maximalIdeal R) R

A chosen coefficient field σ : K → R̂.

Equations

• IsLocalRing.coefficientField R = Classical.choose ⋯

theorem IsLocalRing.residue_coefficientField (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [Algebra ℚ R] (k : ResidueField R) : (residue (AdicCompletion (maximalIdeal R) R)) ((coefficientField R) k) = (residueFieldEquiv R) k

theorem IsLocalRing.sub_coefficientField_mem_maximalIdeal (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [Algebra ℚ R] (y : AdicCompletion (maximalIdeal R) R) : y - (coefficientField R) ((residueFieldEquiv R).symm ((residue (AdicCompletion (maximalIdeal R) R)) y)) ∈ maximalIdeal (AdicCompletion (maximalIdeal R) R)

Every element of R̂ is a constant from the coefficient field plus an element of 𝔪R̂: R̂ = σ(K) + 𝔪R̂.