The Complete Local Domain T = C[[x,y,z]]/(x^2-yz)

This folder constructs the complete local domain T used in the main counterexample. T is the quotient of C[[x,y,z]] by the ideal (x^2-yz). It is a two-dimensional Noetherian complete local domain with a height-one prime Q = (x,y) that is not principal.

noncomputable def Q : Ideal T

Q = (x, y)T, the height-1 prime that is not principal. Here x = image of X 0, y = image of X 1 in T.

Equations

• Q = Ideal.span {(Ideal.Quotient.mk conjI) (MvPowerSeries.X 0), (Ideal.Quotient.mk conjI) (MvPowerSeries.X 1)}

noncomputable def phiToPS : MvPowerSeries (Fin 3) ℂ →+* PowerSeries ℂ

Ring hom from MvPowerSeries (Fin 3) ℂ to PowerSeries ℂ that "projects onto X₂": φ(f)(n) = coeff (Finsupp.single 2 n) f. This sends X₀ ↦ 0, X₁ ↦ 0, X₂ ↦ X.

Equations

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

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

The ideal P = (X₀, X₁) in MvPowerSeries (Fin 3) ℂ.

Equations

• PPre = Ideal.span {MvPowerSeries.X 0, MvPowerSeries.X 1}

theorem conjI_le_PPre : conjI ≤ PPre

conjI ≤ PPre: x²-yz ∈ (X₀, X₁) since x² ∈ (X₀) and yz ∈ (X₁).

noncomputable def divX (s : Fin 3) (f : MvPowerSeries (Fin 3) ℂ) : MvPowerSeries (Fin 3) ℂ

"Division by X s": shifts the s-index down by 1.

Equations

• divX s f m = f (m + Finsupp.single s 1)

theorem coeff_sub_X_mul_divX (s : Fin 3) (f : MvPowerSeries (Fin 3) ℂ) (m : Fin 3 →₀ ℕ) : (MvPowerSeries.coeff m) (f - MvPowerSeries.X s * divX s f) = if m s = 0 then (MvPowerSeries.coeff m) f else 0

f - X s * divX s f vanishes whenever m s ≥ 1, and equals f(m) when m s = 0.

theorem ker_phiToPS_eq : RingHom.ker phiToPS = PPre

ker phiToPS = PPre.

instance PPre_isPrime : PPre.IsPrime

PPre is prime because ker phiToPS = PPre and PowerSeries ℂ is a domain.

theorem Q_eq_map_PPre : Q = Ideal.map (Ideal.Quotient.mk conjI) PPre

Q = Ideal.map (mk conjI) PPre.

theorem Q_isPrime : Q.IsPrime

theorem Q_height_one : Q.height = 1

theorem ψBar_mk (f : MvPowerSeries (Fin 3) ℂ) : ψBar ((Ideal.Quotient.mk conjI) f) = ψHom f

theorem ψBar_mk_X0 : ψBar ((Ideal.Quotient.mk conjI) (MvPowerSeries.X 0)) = MvPowerSeries.X 0 * MvPowerSeries.X 1

theorem ψBar_mk_X1 : ψBar ((Ideal.Quotient.mk conjI) (MvPowerSeries.X 1)) = MvPowerSeries.X 0 ^ 2

noncomputable def negSubstMap : Fin 2 → MvPowerSeries (Fin 2) ℂ

Substitution data Xᵢ ↦ -Xᵢ on ℂ[[u,v]], used to detect odd-parity vanishing of coefficients (recall ψMap sends X₀ ↦ X₀X₁, X₁ ↦ X₀², X₂ ↦ X₁², so the total degree of any monomial in the image is even).

Equations

• negSubstMap i = -MvPowerSeries.X i

theorem negSubst_hasSubst : MvPowerSeries.HasSubst negSubstMap

noncomputable def negSubst : MvPowerSeries (Fin 2) ℂ →ₐ[ℂ] MvPowerSeries (Fin 2) ℂ

The algebra hom on ℂ[[u,v]] induced by the substitution Xᵢ ↦ -Xᵢ.

Equations

• negSubst = MvPowerSeries.substAlgHom negSubst_hasSubst

theorem negSubst_X (i : Fin 2) : negSubst (MvPowerSeries.X i) = -MvPowerSeries.X i

theorem negSubst_ψMap (i : Fin 3) : negSubst (ψMap i) = ψMap i

theorem negSubst_comp_ψHom (f : MvPowerSeries (Fin 3) ℂ) : negSubst (ψHom f) = ψHom f

theorem negSubstMap_eq (s : Fin 2) : negSubstMap s = -1 • MvPowerSeries.X s

theorem Finsupp.sum_fin2 (m : Fin 2 →₀ ℕ) (f : Fin 2 → ℕ → ℕ) (hf : ∀ (i : Fin 2), f i 0 = 0) : m.sum f = f 0 (m 0) + f 1 (m 1)

theorem coeff_negSubst (g : MvPowerSeries (Fin 2) ℂ) (m : Fin 2 →₀ ℕ) : (MvPowerSeries.coeff m) (negSubst g) = (-1) ^ (m 0 + m 1) * (MvPowerSeries.coeff m) g

theorem ψHom_coeff_odd_parity (f : MvPowerSeries (Fin 3) ℂ) (m : Fin 2 →₀ ℕ) (hm : Odd (m 0 + m 1)) : (MvPowerSeries.coeff m) (ψHom f) = 0

theorem Q_le_maximalIdeal : Q ≤ IsLocalRing.maximalIdeal T

theorem Q_not_isPrincipal : ¬Submodule.IsPrincipal Q

theorem mk_X2_not_mem_Q : (Ideal.Quotient.mk conjI) (MvPowerSeries.X 2) ∉ Q

theorem T_ringKrullDim : ringKrullDim T = 2

T has Krull dimension 2.