The Complete Local Domain T

Construction of T = C[[x,y,z]]/(x^2 - yz) and the proof that T is an integral domain.

noncomputable def conjI : Ideal (MvPowerSeries (Fin 3) ℂ)

The ideal (x² - yz) in ℂ[[x,y,z]] where x = X 0, y = X 1, z = X 2.

Equations

• conjI = Ideal.span {MvPowerSeries.X 0 ^ 2 - MvPowerSeries.X 1 * MvPowerSeries.X 2}

@[reducible, inline]

abbrev T : Type

T = ℂ[[x,y,z]]/(x²-yz), the main complete local domain.

Equations

• T = (MvPowerSeries (Fin 3) ℂ ⧸ conjI)

theorem conjI_ne_top : conjI ≠ ⊤

noncomputable def ψMap : Fin 3 → MvPowerSeries (Fin 2) ℂ

The substitution map ψ : ℂ[[x,y,z]] → ℂ[[u,v]] defined by x ↦ u·v, y ↦ u², z ↦ v².

Equations

• ψMap 0 = MvPowerSeries.X 0 * MvPowerSeries.X 1
• ψMap 1 = MvPowerSeries.X 0 ^ 2
• ψMap 2 = MvPowerSeries.X 1 ^ 2

theorem ψ_hasSubst : MvPowerSeries.HasSubst ψMap

noncomputable def ψHom : MvPowerSeries (Fin 3) ℂ →ₐ[ℂ] MvPowerSeries (Fin 2) ℂ

The algebra hom ℂ[[x,y,z]] → ℂ[[u,v]] induced by the substitution ψMap (x ↦ uv, y ↦ u², z ↦ v²).

Equations

• ψHom = MvPowerSeries.substAlgHom ψ_hasSubst

theorem ψ_kills_gen : ψHom (MvPowerSeries.X 0 ^ 2 - MvPowerSeries.X 1 * MvPowerSeries.X 2) = 0

theorem conjI_le_ker_ψ : conjI ≤ RingHom.ker ψHom.toRingHom

theorem anderson_gen_ne_zero : MvPowerSeries.X 0 ^ 2 - MvPowerSeries.X 1 * MvPowerSeries.X 2 ≠ 0

noncomputable def ψBar : T →+* MvPowerSeries (Fin 2) ℂ

The factored map ψbar : T → ℂ[[u,v]].

Equations

• ψBar = Ideal.Quotient.lift conjI ψHom.toRingHom ⋯

noncomputable def mkFin3 (a b c : ℕ) : Fin 3 →₀ ℕ

Construct a Fin 3 →₀ ℕ from three natural numbers.

Equations

• mkFin3 a b c = Finsupp.equivFunOnFinite.symm ![a, b, c]

theorem mkFin3_ext (n : Fin 3 →₀ ℕ) : n = mkFin3 (n 0) (n 1) (n 2)

noncomputable def mkFin2 (a b : ℕ) : Fin 2 →₀ ℕ

Construct a Fin 2 →₀ ℕ from two natural numbers.

Equations

• mkFin2 a b = Finsupp.equivFunOnFinite.symm ![a, b]

noncomputable def divQ (f : MvPowerSeries (Fin 3) ℂ) : MvPowerSeries (Fin 3) ℂ

Explicit quotient: given f, define q so that f = q * (X₀² - X₁X₂) when ψ(f)=0. q(n₀,n₁,n₂) = Σ_{k=0}^{min(n₁,n₂)} f(n₀+2+2k, n₁-k, n₂-k).

Equations

• divQ f n = ∑ k ∈ Finset.range (min (n 1) (n 2) + 1), f (mkFin3 (n 0 + 2 + 2 * k) (n 1 - k) (n 2 - k))

theorem ψMap_prod_eq (d : Fin 3 →₀ ℕ) : (d.prod fun (s : Fin 3) (n : ℕ) => ψMap s ^ n) = (MvPowerSeries.monomial (mkFin2 (d 0 + 2 * d 1) (d 0 + 2 * d 2))) 1

Key coefficient relation: the sum Σ_{k=0}^{min(m₁,m₂)} f(m₀+2k, m₁-k, m₂-k) equals a coefficient of ψHom(f) at the monomial u^{m₀+2m₁} v^{m₀+2m₂}.

theorem mkFin2_inj {a b c d : ℕ} : mkFin2 a b = mkFin2 c d ↔ a = c ∧ b = d

theorem mkFin3_inj {a b c d e f : ℕ} : mkFin3 a b c = mkFin3 d e f ↔ a = d ∧ b = e ∧ c = f

theorem ψ_fiber_char (m₀ m₁ m₂ : ℕ) (hm₀ : m₀ ≤ 1) (d : Fin 3 →₀ ℕ) : mkFin2 (d 0 + 2 * d 1) (d 0 + 2 * d 2) = mkFin2 (m₀ + 2 * m₁) (m₀ + 2 * m₂) ↔ ∃ k ≤ min m₁ m₂, d = mkFin3 (m₀ + 2 * k) (m₁ - k) (m₂ - k)

theorem ψHom_coeff_sum (f : MvPowerSeries (Fin 3) ℂ) (m₀ m₁ m₂ : ℕ) (hm₀ : m₀ ≤ 1) : ∑ k ∈ Finset.range (min m₁ m₂ + 1), f (mkFin3 (m₀ + 2 * k) (m₁ - k) (m₂ - k)) = (MvPowerSeries.coeff (mkFin2 (m₀ + 2 * m₁) (m₀ + 2 * m₂))) (ψHom f)

theorem ψBar_injective : Function.Injective ⇑ψBar

Key lemma: ψbar is injective. This is equivalent to ker ψHom = conjI.

Proof sketch: View ℂ[[x,y,z]] ≅ ℂ[[y,z]][[x]] via the ring equiv. Under this decomposition, every f can be written uniquely as q·(x²-yz) + (a + bx). If ψ(f) = 0 then ψ(a + bx) = a(u²,v²) + b(u²,v²)·uv = 0. The terms a(u²,v²) use only even-even degree monomials while b(u²,v²)·uv uses only odd-odd degree monomials, so both must be zero. Since g ↦ g(u²,v²) is injective, a = b = 0, hence f = q·(x²-yz) ∈ conjI.

instance T_isDomain : IsDomain T