Dimension of an analytic space at a point: local models and charts

dimAt X x = ringKrullDim 𝒪_{X,x} (Hironaka/AnalyticSpace/Dimension.lean; [Fre17, II 5.2]) is read on the local model at x (the local-model clause of AnalyticSpace and the stalk transports ringKrullDim_stalk_restrictOpen, ringKrullDim_stalk_of_kIso of Hironaka/AnalyticSpace/RegularStalk.lean), where the stalk is 𝒪_n/(f)_z (ringKrullDim_stalk_localModel_eq, through stalkEquivQuotientF of Hironaka/AnalyticSpace/Jacobian.lean and the Taylor isomorphism taylorAffine); hence the dimension is a natural number (exists_dimAt_eq_natCast, from dim (𝒪_n/I) ≤ n and the nontriviality of a local ring), and at a point with a manifold chart X|V ≅ (G', 𝒜_{G'}), G' ⊆ K^d, it is d (dimAt_eq_of_kIso_analyticSpaceOfOpen; with isRegular_stalk_iff_exists_manifold_nhd this is Freitag's remark that for complex manifolds the Krull dimension is the usual dimension, at a simple point). Upper semicontinuity is in Hironaka/AnalyticSpace/Semicontinuity.lean, which imports this module.

theorem AnalyticSpace.exists_natCast_eq_of_nonneg_of_le_natCast {x : WithBot ℕ∞} (h0 : 0 ≤ x) {n : ℕ} (hn : x ≤ ↑n) : ∃ (d : ℕ), x = ↑d

An element of WithBot ℕ∞ between 0 and a natural number is a natural number.

theorem AnalyticSpace.ringKrullDim_stalk_localModel_eq {K : Type} [RCLike K] {n : ℕ} (G : TopologicalSpace.Opens (Kn K n)) {k : ℕ} (f : Fin k → AnalyticFun K n G) (z : ↑↑(localModel K n G f).toPresheafedSpace) : ringKrullDim ↑((localModel K n G f).presheaf.stalk z) = ringKrullDim (↥(Analytic.Conv K n) ⧸ Ideal.map (taylorAffine K n ↑↑z) (Ideal.span (Set.range fun (j : Fin k) => (CategoryTheory.ConcreteCategory.hom ((affine K n).presheaf.germ G ↑↑z ⋯)) (f j))))

The bridge between the two levels: the stalk of the local model V(f) ⊆ G ⊆ Kⁿ at z is 𝒜_{Kⁿ,z}/(f)_z (stalkEquivQuotientF), read as 𝒪_n/(f)_z through the Taylor isomorphism taylorAffine at z.

theorem AnalyticSpace.dimAt_eq_of_kIso_analyticSpaceOfOpen {K : Type} [RCLike K] {X : AnalyticSpace K} {V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} {x : ↑↑X.toPresheafedSpace} (hx : x ∈ V) {d : ℕ} {G' : TopologicalSpace.Opens (Kn K d)} (e : (X.restrictOpen V).KIso (analyticSpaceOfOpen K d G')) : X.dimAt x = ↑d

At a point with a manifold chart X|V ≅ (G', 𝒜_{G'}), G' ⊆ K^d, the dimension is d (the stalk transports of Hironaka/AnalyticSpace/RegularStalk.lean; for complex manifolds the Krull dimension is the usual dimension, [Fre17, II 5.2]).

theorem AnalyticSpace.exists_dimAt_eq_natCast {K : Type} [RCLike K] (X : AnalyticSpace K) (x : ↑↑X.toPresheafedSpace) : ∃ (d : ℕ), X.dimAt x = ↑d

The dimension of an analytic K-space at a point is a natural number — through the local model at the point the stalk is 𝒪_n/(f)_z, of dimension between 0 (a local ring is nontrivial) and n.