Dimension at a point and irreducible components of an analytic space

• AnalyticSpace.dimAt X x, the dimension of X at x — the dimension that Hironaka's Main Theorem I'(n) [Hir64, Ch. 0, §7, p. 155] uses for the space W without defining it there: the Krull dimension of the stalk 𝒪_{X,x}, as in [Fre17, II 5.2] ("the dimension of X at some point a ∈ X is the Krull dimension of 𝒪_{X,a}"), an element of WithBot ℕ∞ (⊥ only for the trivial ring, which no stalk of an analytic space is). The dimension ClosedSubspace.dim W of a closed subspace (Hironaka/AnalyticSpace/ClosedSubspace.lean) is the supremum of these over its points.
• taylorAffine K n q: the stalk 𝒜_{Kⁿ,q} read as convergent power series centred at q, through the Taylor isomorphism in the identity chart of Kⁿ; the bridge between statements about convergent power series and the stalks of the local models.
• AnalyticSpace.analyticComponents X: the closures of the connected components of the simple locus X.regularLocus, the irreducible components of a reduced complex space in the sense of the global decomposition of [GR84, Ch. 9].

noncomputable def AnalyticSpace.dimAt {K : Type} [RCLike K] (X : AnalyticSpace K) (x : ↑↑X.toPresheafedSpace) : WithBot ℕ∞

The dimension of X at x [Hir64, Main Theorem I'(n), p. 155], [Fre17, II 5.2]: the Krull dimension of the local ring 𝒪_{X,x}.

Equations

• X.dimAt x = ringKrullDim ↑(X.presheaf.stalk x)

def AnalyticSpace.analyticComponents {K : Type} [RCLike K] (X : AnalyticSpace K) : Set (Set ↑↑X.toPresheafedSpace)

The irreducible components of the analytic space X in the analytic sense [GR84, Ch. 9]: the closures of the connected components of the simple locus X.regularLocus. This is NOT Mathlib's topological irreducibleComponents X (the maximal irreducible closed subsets, which in the Hausdorff topology of an analytic space are the singletons), hence the name.

Equations

• X.analyticComponents = {C : Set ↑↑X.toPresheafedSpace | ∃ x ∈ X.regularLocus, C = closure (connectedComponentIn X.regularLocus x)}

noncomputable def AnalyticSpace.taylorAffine (K : Type) [RCLike K] (n : ℕ) (q : Kn K n) : ↑((affine K n).presheaf.stalk q) ≃+* ↥(Analytic.Conv K n)

The Taylor isomorphism 𝒜_{Kⁿ,q} ≃+* K{x} in the identity chart of Kⁿ (taylorEquivConv): the stalk as convergent power series centred at q.

Equations

• AnalyticSpace.taylorAffine K n q = Manifold.taylorEquivConv (AnalyticSpace.Kn K n) ContinuousLinearEquiv.ulift (chartAt (AnalyticSpace.Kn K n) q) ⋯ ⋯