The map Φ : K⟦X₁, …, X_d⟧ → R̂ of the Cohen structure theorem: construction

Kollár's identification Ô_{p,X} ≅ k(p)⟦x₁, …, xₙ⟧ [Kol07, Definition 55]: with local coordinates x₁, …, x_d and a coefficient field K → R̂ (Hironaka/Algebra/Local/CoefficientField.lean), power series in the Xᵢ are evaluated at the ι(xᵢ) ∈ 𝔪R̂. Mathlib's MvPowerSeries.aeval is a topological construction and AdicCompletion carries no adic topology in Mathlib, so Φ is assembled from its finite levels: for each n, F ↦ (truncTotal n F)(ι x₁, …, ι x_d) is a K-algebra map K⟦X⟧ → R̂/𝔪̂ⁿ (the variables are nilpotent there, so the truncation is harmless — the two polynomials truncTotal n (F G) and truncTotal n F · truncTotal n G agree below degree n and every monomial of degree ≥ n in the ι xᵢ vanishes in R̂/𝔪̂ⁿ), the levels are compatible, and R̂ is 𝔪̂-adically complete (IsAdicComplete.liftAlgHom). The resulting Φ = cohenMap satisfies Φ(C k) = σ(k), Φ(Xᵢ) = ι(xᵢ) and Φ(F) ≡ (truncTotal n F)(ι x) (mod 𝔪̂ⁿ); its surjectivity is proved in Hironaka/Algebra/Local/Cohen.lean and its injectivity in Hironaka/Algebra/Local/CohenIso.lean. The construction takes any K-algebra structure on R̂ ([Algebra (ResidueField R) R̂]), the chosen coefficient field being the instance coefficientAlgebra for ℚ ⊆ R; the completed chart map (Hironaka/Algebra/Local/ChartCompletion.lean) applies it to the transported coefficient field of the chart's local ring.

Polynomials whose variables lie in an ideal

theorem IsLocalRing.aeval_mem_pow_of_degree_le {σ : Type u_1} {K : Type u_2} {B : Type u_3} [CommRing K] [CommRing B] [Algebra K B] {J : Ideal B} {a : σ → B} (ha : ∀ (i : σ), a i ∈ J) {n : ℕ} {P : MvPolynomial σ K} (hP : ∀ α ∈ P.support, n ≤ Finsupp.degree α) : (MvPolynomial.aeval a) P ∈ J ^ n

If the variables lie in J and every monomial of P has degree ≥ n, then P(a) ∈ Jⁿ.

theorem IsLocalRing.aeval_eq_of_coeff_eq {σ : Type u_1} {K : Type u_2} {B : Type u_3} [CommRing K] [CommRing B] [Algebra K B] {J : Ideal B} {a : σ → B} (ha : ∀ (i : σ), a i ∈ J) {n : ℕ} (hJ : J ^ n = ⊥) {P Q : MvPolynomial σ K} (h : ∀ (α : σ →₀ ℕ), Finsupp.degree α < n → P.coeff α = Q.coeff α) : (MvPolynomial.aeval a) P = (MvPolynomial.aeval a) Q

If the variables lie in J with Jⁿ = 0, two polynomials that agree below degree n have the same value.

theorem IsLocalRing.eq_of_pow_zero {S : Type u_4} [CommRing S] (I : Ideal S) (a b : S ⧸ I ^ 0) : a = b

theorem IsLocalRing.eq_of_forall_mk_pow_eq {S : Type u_4} [CommRing S] (I : Ideal S) [IsHausdorff I S] {a b : S} (h : ∀ (n : ℕ), (Ideal.Quotient.mk (I ^ n)) a = (Ideal.Quotient.mk (I ^ n)) b) : a = b

In an I-adically separated ring, elements agreeing modulo every Iⁿ are equal.

The finite levels and the lift

noncomputable def IsLocalRing.levelVar (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {d : ℕ} (x : Fin d → R) (n : ℕ) (i : Fin d) : AdicCompletion (maximalIdeal R) R ⧸ maximalIdeal (AdicCompletion (maximalIdeal R) R) ^ n

The class of ι(xᵢ) in R̂/𝔪̂ⁿ.

Equations

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

theorem IsLocalRing.levelVar_mem (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {d : ℕ} (x : Fin d → R) (hx : ∀ (i : Fin d), x i ∈ maximalIdeal R) (n : ℕ) (i : Fin d) : levelVar R x n i ∈ Ideal.map (Ideal.Quotient.mk (maximalIdeal (AdicCompletion (maximalIdeal R) R) ^ n)) (maximalIdeal (AdicCompletion (maximalIdeal R) R))

theorem IsLocalRing.map_maximalIdeal_pow_eq_bot (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] (n : ℕ) : Ideal.map (Ideal.Quotient.mk (maximalIdeal (AdicCompletion (maximalIdeal R) R) ^ n)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) ^ n = ⊥

The coefficient field enters as a K-algebra structure on R̂, K = ResidueField R: any [Algebra (ResidueField R) R̂] serves for the construction of Φ; the section property IsCoefficientAlgebra R is needed only from the surjectivity on (Hironaka/Algebra/Local/Cohen.lean). The chosen coefficient field is the instance coefficientAlgebra below.

noncomputable def IsLocalRing.levelEval (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {d : ℕ} (x : Fin d → R) [Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)] (hx : ∀ (i : Fin d), x i ∈ maximalIdeal R) (n : ℕ) : MvPowerSeries (Fin d) (ResidueField R) →ₐ[ResidueField R] AdicCompletion (maximalIdeal R) R ⧸ maximalIdeal (AdicCompletion (maximalIdeal R) R) ^ n

The level-n evaluation F ↦ (truncTotal n F)(ι x) in R̂/𝔪̂ⁿ.

Equations

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

theorem IsLocalRing.levelEval_apply (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {d : ℕ} (x : Fin d → R) [Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)] (hx : ∀ (i : Fin d), x i ∈ maximalIdeal R) (n : ℕ) (F : MvPowerSeries (Fin d) (ResidueField R)) : (levelEval R x hx n) F = (MvPolynomial.aeval (levelVar R x n)) ((MvPowerSeries.truncTotal n) F)

theorem IsLocalRing.factorₐ_comp_levelVar (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {d : ℕ} (x : Fin d → R) [Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)] {m n : ℕ} (hle : m ≤ n) : (fun (i : Fin d) => (Ideal.Quotient.factorₐ (ResidueField R) ⋯) (levelVar R x n i)) = levelVar R x m

theorem IsLocalRing.levelEval_compat (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {d : ℕ} (x : Fin d → R) [Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)] (hx : ∀ (i : Fin d), x i ∈ maximalIdeal R) {m n : ℕ} (hle : m ≤ n) : (Ideal.Quotient.factorₐ (ResidueField R) ⋯).comp (levelEval R x hx n) = levelEval R x hx m

The levels are compatible.

noncomputable def IsLocalRing.cohenMap (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {d : ℕ} (x : Fin d → R) [Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)] (hx : ∀ (i : Fin d), x i ∈ maximalIdeal R) : MvPowerSeries (Fin d) (ResidueField R) →ₐ[ResidueField R] AdicCompletion (maximalIdeal R) R

The map Φ : K⟦X₁, …, X_d⟧ → R̂, Xᵢ ↦ ι(xᵢ), K through the coefficient field: the identification of [Kol07, Definition 55], as a map.

Equations

• IsLocalRing.cohenMap R x hx = IsAdicComplete.liftAlgHom (IsLocalRing.maximalIdeal (AdicCompletion (IsLocalRing.maximalIdeal R) R)) (IsLocalRing.levelEval R x hx) ⋯

theorem IsLocalRing.mk_cohenMap (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {d : ℕ} (x : Fin d → R) [Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)] (hx : ∀ (i : Fin d), x i ∈ maximalIdeal R) (n : ℕ) (F : MvPowerSeries (Fin d) (ResidueField R)) : (Ideal.Quotient.mk (maximalIdeal (AdicCompletion (maximalIdeal R) R) ^ n)) ((cohenMap R x hx) F) = (levelEval R x hx n) F

theorem IsLocalRing.cohenMap_C (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {d : ℕ} (x : Fin d → R) [Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)] (hx : ∀ (i : Fin d), x i ∈ maximalIdeal R) (k : ResidueField R) : (cohenMap R x hx) (MvPowerSeries.C k) = (algebraMap (ResidueField R) (AdicCompletion (maximalIdeal R) R)) k

Φ(C k) = σ(k) — the constants go to the coefficient field.

theorem IsLocalRing.cohenMap_X (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {d : ℕ} (x : Fin d → R) [Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)] (hx : ∀ (i : Fin d), x i ∈ maximalIdeal R) (i : Fin d) : (cohenMap R x hx) (MvPowerSeries.X i) = (algebraMap R (AdicCompletion (maximalIdeal R) R)) (x i)

Φ(Xᵢ) = ι(xᵢ).

@[instance_reducible]

noncomputable instance IsLocalRing.coefficientAlgebra (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [Algebra ℚ R] : Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)

R̂ as an algebra over the residue field through the chosen coefficient field (ℚ ⊆ R).

Equations

• IsLocalRing.coefficientAlgebra R = (IsLocalRing.coefficientField R).toAlgebra

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

theorem IsLocalRing.isCoefficientAlgebra_coefficientAlgebra (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [Algebra ℚ R] : IsCoefficientAlgebra R

The chosen coefficient field is a section of the residue map.

theorem IsLocalRing.cohenMap_C_coefficientField (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [Algebra ℚ R] {d : ℕ} (x : Fin d → R) (hx : ∀ (i : Fin d), x i ∈ maximalIdeal R) (k : ResidueField R) : (cohenMap R x hx) (MvPowerSeries.C k) = (coefficientField R) k

Φ(C k) = σ(k) for the chosen coefficient field.