The Complete Domain T -- Local Ring Properties

T = C[[x,y,z]]/(x^2 - yz) is a Noetherian complete local domain whose residue field has the cardinality of C.

instance T_isLocalRing : IsLocalRing T

instance instIsNoetherianRingMvPowerSeriesFinOfNatNatComplex_leanPool : IsNoetherianRing (MvPowerSeries (Fin 1) ℂ)

theorem Finsupp.cons_add' {n a b : ℕ} {s t : Fin n →₀ ℕ} : cons (a + b) (s + t) = cons a s + cons b t

theorem Finsupp.tail_add' {n : ℕ} (s t : Fin (n + 1) →₀ ℕ) : (s + t).tail = s.tail + t.tail

theorem Finsupp.add_cons_zero {n : ℕ} (s t : Fin (n + 1) →₀ ℕ) : (s + t) 0 = s 0 + t 0

theorem Finsupp.mem_antidiagonal_cons_iff {n k : ℕ} {s : Fin n →₀ ℕ} {a b : Fin (n + 1) →₀ ℕ} : (a, b) ∈ Finset.antidiagonal (cons k s) ↔ (a 0, b 0) ∈ Finset.antidiagonal k ∧ (a.tail, b.tail) ∈ Finset.antidiagonal s

noncomputable def mvPowerSeriesFin0RingEquiv (R : Type u_1) [CommSemiring R] : MvPowerSeries (Fin 0) R ≃+* R

The ring equivalence MvPowerSeries (Fin 0) R ≃+* R given by taking the constant coefficient (its inverse is the constant-series embedding).

Equations

• mvPowerSeriesFin0RingEquiv R = { toFun := ⇑MvPowerSeries.constantCoeff, invFun := ⇑MvPowerSeries.C, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

theorem fin1_finsupp_eq {u : Fin 1 →₀ ℕ} : u = Finsupp.single 0 (u 0)

noncomputable def mvPowerSeriesFinSuccRingEquiv {n : ℕ} {R : Type u_1} [CommSemiring R] : MvPowerSeries (Fin (n + 1)) R ≃+* MvPowerSeries (Fin 1) (MvPowerSeries (Fin n) R)

MvPowerSeries (Fin (n+1)) R ≃+* MvPowerSeries (Fin 1) (MvPowerSeries (Fin n) R)

Equations

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

noncomputable def mvPowerSeriesFinSuccRingEquiv' {n : ℕ} {R : Type u_1} [CommSemiring R] : MvPowerSeries (Fin (n + 1)) R ≃+* PowerSeries (MvPowerSeries (Fin n) R)

The ring equivalence MvPowerSeries (Fin (n+1)) R ≃+* PowerSeries (MvPowerSeries (Fin n) R), obtained from mvPowerSeriesFinSuccRingEquiv by identifying Fin 1-variable power series with ordinary power series.

Equations

• mvPowerSeriesFinSuccRingEquiv' = mvPowerSeriesFinSuccRingEquiv.trans (MvPowerSeries.renameEquiv (MvPowerSeries (Fin n) R) (Equiv.equivPUnit (Fin 1))).toRingEquiv

theorem mvPowerSeries_fin_isNoetherianRing {n : ℕ} {R : Type u_1} [CommRing R] [IsNoetherianRing R] : IsNoetherianRing (MvPowerSeries (Fin n) R)

theorem mvPowerSeries_fin3_isNoetherianRing : IsNoetherianRing (MvPowerSeries (Fin 3) ℂ)

instance T_isNoetherianRing : IsNoetherianRing T

@[reducible, inline]

noncomputable abbrev MPS : Ideal (MvPowerSeries (Fin 3) ℂ)

Local abbreviation for the maximal ideal of ℂ[[x,y,z]] = MvPowerSeries (Fin 3) ℂ.

Equations

• MPS = IsLocalRing.maximalIdeal (MvPowerSeries (Fin 3) ℂ)

@[reducible, inline]

abbrev tdeg (d : Fin 3 →₀ ℕ) : ℕ

Total degree of a monomial exponent vector d : Fin 3 →₀ ℕ.

Equations

• tdeg d = d.sum fun (x : Fin 3) (k : ℕ) => k

theorem tdeg_add (a b : Fin 3 →₀ ℕ) : tdeg (a + b) = tdeg a + tdeg b

theorem constantCoeff_eq_zero_of_mem_MPS {m : MvPowerSeries (Fin 3) ℂ} (hm : m ∈ MPS) : MvPowerSeries.constantCoeff m = 0

theorem coeff_eq_zero_of_mem_MPS_pow {f : MvPowerSeries (Fin 3) ℂ} {n : ℕ} (hf : f ∈ MPS ^ n) (d : Fin 3 →₀ ℕ) : tdeg d < n → (MvPowerSeries.coeff d) f = 0

theorem mem_MPS_pow_of_coeff_vanish (f : MvPowerSeries (Fin 3) ℂ) (n : ℕ) (hf : ∀ (d : Fin 3 →₀ ℕ), tdeg d < n → (MvPowerSeries.coeff d) f = 0) : f ∈ MPS ^ n

theorem mvPS_isPrecomplete : IsPrecomplete MPS (MvPowerSeries (Fin 3) ℂ)

theorem T_isPrecomplete : IsPrecomplete (IsLocalRing.maximalIdeal T) T

instance T_isAdicComplete : IsAdicComplete (IsLocalRing.maximalIdeal T) T

T is complete with respect to its maximal ideal.

theorem mvPS_mem_span_X_of_constantCoeff_zero {k : Type u_1} [CommRing k] (f : MvPowerSeries (Fin 3) k) (hf : MvPowerSeries.constantCoeff f = 0) : f ∈ Ideal.span {MvPowerSeries.X 0, MvPowerSeries.X 1, MvPowerSeries.X 2}

theorem mvPS_maximalIdeal_eq_span_X : IsLocalRing.maximalIdeal (MvPowerSeries (Fin 3) ℂ) = Ideal.span {MvPowerSeries.X 0, MvPowerSeries.X 1, MvPowerSeries.X 2}

theorem mvPS_ringKrullDim_le : ringKrullDim (MvPowerSeries (Fin 3) ℂ) ≤ 3

theorem gen_mem_nonZeroDivisors : MvPowerSeries.X 0 ^ 2 - MvPowerSeries.X 1 * MvPowerSeries.X 2 ∈ nonZeroDivisors (MvPowerSeries (Fin 3) ℂ)

theorem gen_mem_maximalIdeal : MvPowerSeries.X 0 ^ 2 - MvPowerSeries.X 1 * MvPowerSeries.X 2 ∈ IsLocalRing.maximalIdeal (MvPowerSeries (Fin 3) ℂ)

theorem cToT_injective : Function.Injective ⇑((Ideal.Quotient.mk conjI).comp MvPowerSeries.C)

theorem mvPS_card_eq : Cardinal.mk (MvPowerSeries (Fin 3) ℂ) = Cardinal.mk ℂ

theorem T_card_eq : Cardinal.mk T = Cardinal.mk ℂ

|T| = |ℂ| (a power series ring over ℂ in finitely many vars has cardinality |ℂ|).

theorem unit_of_mk_unit_T (g : MvPowerSeries (Fin 3) ℂ) (h : IsUnit ((Ideal.Quotient.mk conjI) g)) : IsUnit (MvPowerSeries.constantCoeff g)

theorem mk_sub_C_mem_maxIdeal_T (f : MvPowerSeries (Fin 3) ℂ) : (Ideal.Quotient.mk conjI) (f - MvPowerSeries.C (MvPowerSeries.constantCoeff f)) ∈ IsLocalRing.maximalIdeal T

noncomputable def cToResT : ℂ →+* IsLocalRing.ResidueField T

The composite ℂ →[C] MvPowerSeries (Fin 3) ℂ →[mk] T →[residue] T/M from ℂ to the residue field of T.

Equations

• cToResT = (IsLocalRing.residue T).comp ((Ideal.Quotient.mk conjI).comp MvPowerSeries.C)

theorem cToResT_surjective : Function.Surjective ⇑cToResT

theorem cToResT_injective : Function.Injective ⇑cToResT

theorem T_residueField_card : Cardinal.mk (IsLocalRing.ResidueField T) = Cardinal.mk ℂ

|T/M| = |ℂ| (the residue field is ℂ).