Surjectivity of Φ : K⟦X⟧ → R̂ #
The surjectivity half of Kollár's Ô_{p,X} ≅ k(p)⟦x₁, …, xₙ⟧ [Kol07, Definition 55], proved by
successive approximation. For ρ ∈ R̂ one chooses homogeneous polynomials H₀, H₁, … with H_a
of degree a and
ρ − Φ(H₀ + ⋯ + H_a) ∈ 𝔪̂^{a+1}: this is possible because 𝔪̂^a/𝔪̂^{a+1} is spanned over the
coefficient field by the degree-a monomials in the ι(xᵢ) — every element of R̂ is a constant
of the coefficient field plus an element of 𝔪̂ (sub_algebraMap_mem_maximalIdeal, the section
property IsCoefficientAlgebra R of the coefficient field, the only place it is used), and
𝔪̂ = ⟨ι x₁, …, ι x_d⟩. The power series H = ∑ H_a (coefficientwise: the degree-a part is
H_a) then satisfies Φ(H) ≡ Φ(H₀ + ⋯ + H_{a-1}) ≡ ρ (mod 𝔪̂^a) for every a, because Φ
computes modulo 𝔪̂^a through the truncation below degree a (mk_cohenMap), and R̂ is
Hausdorff.
Lifting coherently through the finite levels would instead need ker(K⟦X⟧ → R̂/𝔪̂^a) = (X)^a,
which is equivalent to the injectivity proved in Hironaka/Algebra/Local/CohenIso.lean; the
homogeneous construction avoids it.
theorem
IsLocalRing.x_mem_maximalIdeal_of_eq_span
(R : Type u_1)
[CommRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
(i : Fin d)
:
theorem
IsLocalRing.maximalIdeal_adicCompletion_eq_span
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
:
maximalIdeal (AdicCompletion (maximalIdeal R) R) = Ideal.span (Set.range fun (i : Fin d) => (algebraMap R (AdicCompletion (maximalIdeal R) R)) (x i))
@[reducible, inline]
noncomputable abbrev
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 : maximalIdeal R = Ideal.span (Set.range x))
:
The map Φ of Hironaka/Algebra/Local/CohenMap.lean for a generating family x of 𝔪.
Equations
- IsLocalRing.cohenMap' R x hx = IsLocalRing.cohenMap R x ⋯
Instances For
theorem
IsLocalRing.cohenMap_coe
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
[Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)]
(hx : maximalIdeal R = Ideal.span (Set.range x))
(P : MvPolynomial (Fin d) (ResidueField R))
:
(cohenMap' R x hx) ↑P = (MvPolynomial.aeval fun (i : Fin d) => (algebraMap R (AdicCompletion (maximalIdeal R) R)) (x i)) P
On polynomials, Φ is the evaluation at ι(x).
theorem
IsLocalRing.exists_isHomogeneous_sub_cohenMap_mem
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
[Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)]
(hι : IsCoefficientAlgebra R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
(a : ℕ)
(ρ : AdicCompletion (maximalIdeal R) R)
:
ρ ∈ maximalIdeal (AdicCompletion (maximalIdeal R) R) ^ a →
∃ (H : MvPolynomial (Fin d) (ResidueField R)),
H.IsHomogeneous a ∧ ρ - (cohenMap' R x hx) ↑H ∈ maximalIdeal (AdicCompletion (maximalIdeal R) R) ^ (a + 1)
One step of the successive approximation: an element of 𝔪̂^a is, modulo 𝔪̂^{a+1}, the
value of a homogeneous polynomial of degree a over the coefficient field.
noncomputable def
IsLocalRing.approxStep
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
[Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)]
(hι : IsCoefficientAlgebra R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
(a : ℕ)
(r : ↥(maximalIdeal (AdicCompletion (maximalIdeal R) R) ^ a))
:
MvPolynomial (Fin d) (ResidueField R)
One step of the successive approximation: the homogeneous polynomial of degree a chosen for
a remainder r ∈ 𝔪̂^a.
Equations
- IsLocalRing.approxStep R x hι hx a r = Classical.choose ⋯
Instances For
theorem
IsLocalRing.approxStep_spec
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
[Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)]
(hι : IsCoefficientAlgebra R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
(a : ℕ)
(r : ↥(maximalIdeal (AdicCompletion (maximalIdeal R) R) ^ a))
:
(approxStep R x hι hx a r).IsHomogeneous a ∧ ↑r - (cohenMap' R x hx) ↑(approxStep R x hι hx a r) ∈ maximalIdeal (AdicCompletion (maximalIdeal R) R) ^ (a + 1)
noncomputable def
IsLocalRing.approxRem
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
[Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)]
(hι : IsCoefficientAlgebra R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
(ρ : AdicCompletion (maximalIdeal R) R)
(a : ℕ)
:
↥(maximalIdeal (AdicCompletion (maximalIdeal R) R) ^ a)
The remainders of the successive approximation of ρ: rem₀ = ρ,
rem_{a+1} = rem_a − Φ(H_a) with H_a homogeneous of degree a and rem_a ∈ 𝔪̂^a.
Equations
- One or more equations did not get rendered due to their size.
- IsLocalRing.approxRem R x hι hx ρ 0 = ⟨ρ, ⋯⟩
Instances For
noncomputable def
IsLocalRing.approxPoly
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
[Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)]
(hι : IsCoefficientAlgebra R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
(ρ : AdicCompletion (maximalIdeal R) R)
(a : ℕ)
:
MvPolynomial (Fin d) (ResidueField R)
The homogeneous pieces H_a of the successive approximation of ρ.
Equations
- IsLocalRing.approxPoly R x hι hx ρ a = IsLocalRing.approxStep R x hι hx a (IsLocalRing.approxRem R x hι hx ρ a)
Instances For
theorem
IsLocalRing.approxPoly_isHomogeneous
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
[Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)]
(hι : IsCoefficientAlgebra R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
(ρ : AdicCompletion (maximalIdeal R) R)
(a : ℕ)
:
(approxPoly R x hι hx ρ a).IsHomogeneous a
theorem
IsLocalRing.approxRem_zero
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
[Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)]
(hι : IsCoefficientAlgebra R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
(ρ : AdicCompletion (maximalIdeal R) R)
:
theorem
IsLocalRing.approxRem_succ
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
[Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)]
(hι : IsCoefficientAlgebra R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
(ρ : AdicCompletion (maximalIdeal R) R)
(a : ℕ)
:
noncomputable def
IsLocalRing.approxPartial
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
[Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)]
(hι : IsCoefficientAlgebra R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
(ρ : AdicCompletion (maximalIdeal R) R)
(a : ℕ)
:
MvPolynomial (Fin d) (ResidueField R)
The partial sums H₀ + ⋯ + H_{a-1}.
Equations
- IsLocalRing.approxPartial R x hι hx ρ a = ∑ b ∈ Finset.range a, IsLocalRing.approxPoly R x hι hx ρ b
Instances For
theorem
IsLocalRing.approxRem_eq
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
[Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)]
(hι : IsCoefficientAlgebra R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
(ρ : AdicCompletion (maximalIdeal R) R)
(a : ℕ)
:
noncomputable def
IsLocalRing.approxSeries
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
[Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)]
(hι : IsCoefficientAlgebra R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
(ρ : AdicCompletion (maximalIdeal R) R)
:
MvPowerSeries (Fin d) (ResidueField R)
The power series ∑ₐ H_a of the successive approximation.
Equations
- IsLocalRing.approxSeries R x hι hx ρ α = (IsLocalRing.approxPoly R x hι hx ρ (Finsupp.degree α)).coeff α
Instances For
theorem
IsLocalRing.coeff_approxSeries
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
[Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)]
(hι : IsCoefficientAlgebra R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
(ρ : AdicCompletion (maximalIdeal R) R)
(α : Fin d →₀ ℕ)
:
(MvPowerSeries.coeff α) (approxSeries R x hι hx ρ) = (approxPoly R x hι hx ρ (Finsupp.degree α)).coeff α
theorem
IsLocalRing.coeff_approxPartial
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
[Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)]
(hι : IsCoefficientAlgebra R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
(ρ : AdicCompletion (maximalIdeal R) R)
(a : ℕ)
(α : Fin d →₀ ℕ)
:
(approxPartial R x hι hx ρ a).coeff α = if Finsupp.degree α < a then (approxPoly R x hι hx ρ (Finsupp.degree α)).coeff α else 0
theorem
IsLocalRing.truncTotal_approxSeries
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
[Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)]
(hι : IsCoefficientAlgebra R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
(ρ : AdicCompletion (maximalIdeal R) R)
(a : ℕ)
:
theorem
IsLocalRing.truncTotal_coe_approxPartial
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
[Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)]
(hι : IsCoefficientAlgebra R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
(ρ : AdicCompletion (maximalIdeal R) R)
(a : ℕ)
:
theorem
IsLocalRing.cohenMap_surjective_of_residue
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
{d : ℕ}
(x : Fin d → R)
[Algebra (ResidueField R) (AdicCompletion (maximalIdeal R) R)]
(hι : IsCoefficientAlgebra R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
:
Function.Surjective ⇑(cohenMap' R x hx)
Φ is surjective, for any coefficient field (the surjectivity half of
[Kol07, Definition 55], by successive approximation).
theorem
IsLocalRing.cohenMap_surjective
(R : Type u_1)
[CommRing R]
[IsNoetherianRing R]
[IsLocalRing R]
[Algebra ℚ R]
{d : ℕ}
(x : Fin d → R)
(hx : maximalIdeal R = Ideal.span (Set.range x))
:
Function.Surjective ⇑(cohenMap' R x hx)
Φ is surjective — the specialization of cohenMap_surjective_of_residue at the chosen
coefficient field (ℚ ⊆ R).