The Cohen isomorphism over the ground field

Kollár, in the proof of the formal equivalence theorem [Kol07, 95], identifies the completed local ring Ô_{p,X} of a k-variety at a point with residue field K with K⟦x₁, …, xₙ⟧ by the Cohen structure theorem ([Kol07, Definition 55]), so that the computations of Proposition 94 apply to it; and Notation 93 views R = K⟦x⟧ "as a k-algebra" [Kol07, Notation 93]. For the automorphism of X̂ = Spec_k Ô_{p,X} of [Kol07, Definition 91] (a k-algebra automorphism) to be produced by a substitution on K⟦x⟧, the Cohen isomorphism K⟦x⟧ ≅ Ô_{p,X} must be k-linear: its coefficient field K → Ô must be a k-algebra map. Hironaka/Algebra/Local/CoefficientField.lean produces a coefficient field over ℚ; this file gives the general form over a ground field k of characteristic zero:

• formallySmooth_of_charZero: a field extension K/k in characteristic zero is formally smooth ([TSPA, Tag 0322]: separably generated) — formallySmooth_rat_of_field with ℚ replaced by k: a transcendence basis, over which K is algebraic, hence separable in characteristic zero.
• exists_coefficientField_over: a k-linear coefficient field σ : K →ₐ[k] R̂ of the completion of a Noetherian local k-algebra R with residue field K — the lift of the (k-linear) residue isomorphism K ≅ R̂/𝔪R̂ through the 𝔪R̂-adically complete R̂.
• cohenAlgEquivOver σ hσ x hx hd : K⟦X₁, …, X_d⟧ ≃ₐ[k] R̂ for a regular system of parameters x: cohenEquivOfResidue of Hironaka/Algebra/Local/CohenIso.lean for the coefficient field σ, which is k-linear because the constants go to σ (cohenMap_C) and σ is k-linear. cohenAlgEquivOver_X, cohenAlgEquivOver_C are Kollár's xᵢ ↦ ι(xᵢ), constants to the coefficient field.
• exists_algEquiv_of_regularSystems (Kollár's automorphism φ^* with φ^*(x₁', x₂, …, xₙ) = (x₁, x₂, …, xₙ), defined because both are coordinate systems, [Kol07, 95]): for two regular systems of parameters x, x' there is a k-algebra automorphism φ of R̂ with φ(ι x'ᵢ) = ι xᵢ — the composite Φ ∘ Φ'⁻¹ of the Cohen isomorphisms of x and x' for one and the same coefficient field; the criterion of Notation 93 ("the linear parts of the gᵢ are linearly independent") is not needed, the two coordinate systems supply the two isomorphisms.

The k-linear Cohen isomorphism is used for the formal equivalence of points along a hypersurface of maximal contact (Hironaka/Resolution/Algebraic/MaximalContact/FormalEquivExists.lean).

theorem IsLocalRing.formallySmooth_of_charZero (k : Type u_1) (K : Type u_2) [Field k] [Field K] [CharZero k] [Algebra k K] : Algebra.FormallySmooth k K

A field extension of a field of characteristic zero is formally smooth ([TSPA, Tag 0322]) — formallySmooth_rat_of_field with ℚ replaced by k.

theorem IsLocalRing.residueFieldEquiv_algebraMap (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] (k : Type u_2) [Field k] [Algebra k R] (a : k) : (residueFieldEquiv R) ((algebraMap k (ResidueField R)) a) = (algebraMap k (ResidueField (AdicCompletion (maximalIdeal R) R))) a

The residue isomorphism K ≅ R̂/𝔪R̂ is k-linear.

theorem IsLocalRing.exists_coefficientField_over (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] (k : Type u_2) [Field k] [CharZero k] [Algebra k R] : ∃ (σ : ResidueField R →ₐ[k] AdicCompletion (maximalIdeal R) R), ∀ (a : ResidueField R), (residue (AdicCompletion (maximalIdeal R) R)) (σ a) = (residueFieldEquiv R) a

A k-linear coefficient field of R̂ exists — a k-algebra map σ : K → R̂ from the residue field which is a section of the residue map R̂ → R̂/𝔪R̂ = K.

noncomputable def IsLocalRing.cohenAlgEquivOver {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] (σ : ResidueField R →ₐ[k] AdicCompletion (maximalIdeal R) R) (hσ : ∀ (a : ResidueField R), (residue (AdicCompletion (maximalIdeal R) R)) (σ a) = (residueFieldEquiv R) a) {d : ℕ} (x : Fin d → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hd : ↑d = ringKrullDim R) : MvPowerSeries (Fin d) (ResidueField R) ≃ₐ[k] AdicCompletion (maximalIdeal R) R

The Cohen isomorphism K⟦X₁, …, X_d⟧ ≃ R̂ ([Kol07, Definition 55]; as used in [Kol07, 95]) for the k-linear coefficient field σ, as a k-algebra isomorphism.

Equations

• IsLocalRing.cohenAlgEquivOver σ hσ x hx hd = AlgEquiv.ofRingEquiv ⋯

theorem IsLocalRing.cohenAlgEquivOver_X {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] (σ : ResidueField R →ₐ[k] AdicCompletion (maximalIdeal R) R) (hσ : ∀ (a : ResidueField R), (residue (AdicCompletion (maximalIdeal R) R)) (σ a) = (residueFieldEquiv R) a) {d : ℕ} (x : Fin d → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hd : ↑d = ringKrullDim R) (i : Fin d) : (cohenAlgEquivOver σ hσ x hx hd) (MvPowerSeries.X i) = (algebraMap R (AdicCompletion (maximalIdeal R) R)) (x i)

Kollár's xᵢ ↦ ι(xᵢ).

theorem IsLocalRing.cohenAlgEquivOver_C {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] (σ : ResidueField R →ₐ[k] AdicCompletion (maximalIdeal R) R) (hσ : ∀ (a : ResidueField R), (residue (AdicCompletion (maximalIdeal R) R)) (σ a) = (residueFieldEquiv R) a) {d : ℕ} (x : Fin d → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hd : ↑d = ringKrullDim R) (a : ResidueField R) : (cohenAlgEquivOver σ hσ x hx hd) (MvPowerSeries.C a) = σ a

The constants go to the coefficient field.

theorem IsLocalRing.residue_cohenAlgEquivOver_C {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {k : Type u_2} [Field k] [Algebra k R] (σ : ResidueField R →ₐ[k] AdicCompletion (maximalIdeal R) R) (hσ : ∀ (a : ResidueField R), (residue (AdicCompletion (maximalIdeal R) R)) (σ a) = (residueFieldEquiv R) a) {d : ℕ} (x : Fin d → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hd : ↑d = ringKrullDim R) (a : ResidueField R) : (residue (AdicCompletion (maximalIdeal R) R)) ((cohenAlgEquivOver σ hσ x hx hd) (MvPowerSeries.C a)) = (residueFieldEquiv R) a

The constants of the Cohen isomorphism form a coefficient field: residue (Φ (C a)) = a.

theorem IsLocalRing.exists_cohenAlgEquiv_over {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {k : Type u_2} [Field k] [CharZero k] [Algebra k R] {d : ℕ} (x : Fin d → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hd : ↑d = ringKrullDim R) : ∃ (Φ : MvPowerSeries (Fin d) (ResidueField R) ≃ₐ[k] AdicCompletion (maximalIdeal R) R), (∀ (i : Fin d), Φ (MvPowerSeries.X i) = (algebraMap R (AdicCompletion (maximalIdeal R) R)) (x i)) ∧ ∀ (a : ResidueField R), (residue (AdicCompletion (maximalIdeal R) R)) (Φ (MvPowerSeries.C a)) = (residueFieldEquiv R) a

For a regular system of parameters x of the Noetherian local k-algebra R there is a k-algebra isomorphism Φ : K⟦X⟧ ≃ₐ[k] R̂ with Φ(Xᵢ) = ι(xᵢ) whose constants form a coefficient field: "Ô_{p,X} ≅ K⟦x₁, …, xₙ⟧ by (55)" as a k-algebra, [Kol07, 95].

theorem IsLocalRing.exists_algEquiv_of_regularSystems {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {k : Type u_2} [Field k] [CharZero k] [Algebra k R] {d : ℕ} (x x' : Fin d → R) (hx : maximalIdeal R = Ideal.span (Set.range x)) (hx' : maximalIdeal R = Ideal.span (Set.range x')) (hd : ↑d = ringKrullDim R) : ∃ (φ : AdicCompletion (maximalIdeal R) R ≃ₐ[k] AdicCompletion (maximalIdeal R) R), ∀ (i : Fin d), φ ((algebraMap R (AdicCompletion (maximalIdeal R) R)) (x' i)) = (algebraMap R (AdicCompletion (maximalIdeal R) R)) (x i)

For two regular systems of parameters x, x' of R there is a k-algebra automorphism φ of R̂ with φ(ι x'ᵢ) = ι xᵢ for every i — the composite of the Cohen isomorphisms of x and x' for one coefficient field (Kollár's automorphism φ^* with φ^*(x₁', x₂, …, xₙ) = (x₁, x₂, …, xₙ), defined because both are coordinate systems, [Kol07, 95]).