The dimension of an analytic germ on the germ ring 𝒪_n

The Krull dimension of 𝒪_n/I, 𝒪_n = Conv K n the ring of convergent power series (Hironaka/Analytic/ConvSeries/), is the d of every Noether normalization 𝒪_d ↪ 𝒪_n/I ([Fre17, I 7.2]: the number d is unique, it is the Krull dimension — by the theorem of Cohen–Seidenberg, [Fre17, VII 5.7], Hironaka/Algebra/Local/IntegralKrullDim.lean), so the Krull dimension is the unique — hence the largest — d with a coordinate projection finite and surjective on germs (ringKrullDim_quotient_eq_of_normMap, exists_normMap_injective_finite_iff; Noether normalization exists_noetherNormalization_analytic, normMap of Hironaka/Analytic/Rueckert/NoetherNormalization.lean); dim (𝒪_n/I) ≤ n = dim 𝒪_n ([Fre17, VII 5.6]; ringKrullDim_conv through the Taylor isomorphism taylorAffine and ringKrullDim_stalk_affine), with equality iff I = 0 ([Fre17, II 5.11] for X = Kⁿ; Ideal.eq_bot_of_ringKrullDim_quotient_eq of Hironaka/Algebra/Local/QuotientParameters.lean in the Noetherian local domain 𝒪_n), and I = 0 iff V(I) is a neighbourhood of 0 (the identity theorem, span_eq_bot_iff_eventually_mem_zeroSet). Every statement holds over K = ℝ and ℂ. Used by Hironaka/AnalyticSpace/DimensionLemmas.lean.

theorem AnalyticSpace.ringKrullDim_conv (K : Type) [RCLike K] (n : ℕ) : ringKrullDim ↥(Analytic.Conv K n) = ↑n

The germ ring has Krull dimension n ([Fre17, VII 5.6]: ℂ{z₁, …, z_n} has Krull dimension n): it is 𝒜_{Kⁿ,0} through the Taylor isomorphism taylorAffine, of Krull dimension n (ringKrullDim_stalk_affine).

theorem AnalyticSpace.ringKrullDim_quotient_eq_of_normMap (K : Type) [RCLike K] {n d : ℕ} (I : Ideal ↥(Analytic.Conv K n)) (_hI : I ≠ ⊤) (e : Fin d ↪ Fin n) (L : (Fin n → K) ≃L[K] Fin n → K) (hinj : Function.Injective ⇑(Analytic.normMap K I e L)) (hfin : (↑(Analytic.normMap K I e L)).Finite) : ringKrullDim (↥(Analytic.Conv K n) ⧸ I) = ↑d

Every Noether normalization 𝒪_d ↪ 𝒪_n/I (injective and finite) has d = ringKrullDim (𝒪_n/I) ([Fre17, I 7.2, VII 5.7]) — Cohen–Seidenberg for the finite injective normMap. The hypothesis _hI : I ≠ ⊤ is part of Freitag's statement (the ideal is proper) and is kept so that the theorem reads as printed and takes the same hypotheses as exists_normMap_injective_finite_iff below; the proof does not need it, because a finite injective ring map into the trivial ring 𝒪_n/⊤ does not exist, so I ≠ ⊤ follows from hinj.

theorem AnalyticSpace.exists_normMap_injective_finite_iff (K : Type) [RCLike K] {n : ℕ} (I : Ideal ↥(Analytic.Conv K n)) (hI : I ≠ ⊤) (d : ℕ) : (∃ (e : Fin d ↪ Fin n) (L : (Fin n → K) ≃L[K] Fin n → K), Function.Injective ⇑(Analytic.normMap K I e L) ∧ (↑(Analytic.normMap K I e L)).Finite) ↔ ringKrullDim (↥(Analytic.Conv K n) ⧸ I) = ↑d

d admits an injective finite normalization map iff d = ringKrullDim (𝒪_n/I) — existence by Noether normalization (exists_noetherNormalization_analytic), uniqueness by Cohen–Seidenberg.

theorem AnalyticSpace.ringKrullDim_quotient_le_natCast (K : Type) [RCLike K] {n : ℕ} (I : Ideal ↥(Analytic.Conv K n)) : ringKrullDim (↥(Analytic.Conv K n) ⧸ I) ≤ ↑n

dim (𝒪_n/I) ≤ n.

theorem AnalyticSpace.ringKrullDim_quotient_eq_natCast_iff (K : Type) [RCLike K] {n : ℕ} (I : Ideal ↥(Analytic.Conv K n)) (hI : I ≠ ⊤) : ringKrullDim (↥(Analytic.Conv K n) ⧸ I) = ↑n ↔ I = ⊥

dim (𝒪_n/I) = n iff I = 0 ([Fre17, II 5.11] for X = Kⁿ): a nonzero ideal of the Noetherian local domain 𝒪_n drops the dimension (Ideal.eq_bot_of_ringKrullDim_quotient_eq).

theorem AnalyticSpace.span_eq_bot_iff_eventually_mem_zeroSet (K : Type) [RCLike K] {n : ℕ} (S : Finset ↥(Analytic.Conv K n)) : Ideal.span ↑S = ⊥ ↔ ∀ᶠ (x : Fin n → K) in nhds 0, x ∈ Analytic.zeroSet S

(S) = 0 iff V(S) is a neighbourhood of 0 — the identity theorem Conv.ext_of_evalSeries_eventuallyEq.