Analytic `K`-spaces #

Hironaka's definition [Hir64, Ch. 0, §1, pp. 119–121] starts from K ∈ {ℝ, ℂ} with its standard topology, the Cartesian power Kⁿ, and 𝒜_{Kⁿ}, the sheaf of germs of analytic K-functions on Kⁿ — the sheaf whose stalks are the convergent power series rings 𝒜_{Kⁿ,x} = K{z₁ - x₁, …, zₙ - xₙ}. For an open G ⊆ Kⁿ, 𝒜_G is the restriction of 𝒜_{Kⁿ} to G and (G, 𝒜_G) is a K-local-ringed space. A local analytic K-space is (S(𝓘), (𝒜_G/𝓘)|_{S(𝓘)}), where 𝓘 ⊆ 𝒜_G is the sheaf of ideals generated by finitely many regular analytic K-functions f₁, …, f_k on G and S(𝓘) is the support of 𝒜_G/𝓘. An analytic K-space is a K-local-ringed space X = (X, 𝒪_X) such that (i) every point x has an open neighbourhood U with (U, 𝒪_X|U) K-isomorphic to a local analytic K-space, (ii) X is countable at infinity (a union of countably many compact subsets), and (iii) X is Hausdorff. An/K is the full subcategory of ℜ/K on the analytic K-spaces [Hir64, Ch. 0, §1, p. 121]. Preanalytic K-spaces ((i) and (ii) only) are not needed and are not defined.

The local models #

Kn K n: Kⁿ placed in the universe u as ULift (Fin n → K). Analytic K-spaces have carriers in an arbitrary universe u while K : Type, and a local model must be a locally ringed space in the same universe as the spaces it models; the lift is a linear isometry (ContinuousLinearEquiv.ulift) and changes nothing else.
affine K n = (Kⁿ, 𝒜_{Kⁿ}): KLocallyRingedSpace.ofManifold of Kⁿ as an analytic manifold over itself, so that 𝒜_{Kⁿ} is the sheaf of analytic functions and its stalks are the local rings of analytic germs (identified with convergent power series rings by taylorAffine), with the constants as K-structure.
AnalyticFun K n G = Γ(G, 𝒜_{Kⁿ}) and analyticSpaceOfOpen K n G = (G, 𝒜_G), the restriction of affine K n to G; toGlobal G reads an analytic function on G as a global section of 𝒜_G.
modelIdeal K n G f, the ideal sheaf 𝓘 = (f₁, …, f_k) ⊆ 𝒜_G generated by the global sections f_i (IdealSheaf.ofGlobal), and localModel K n G f = (S(𝓘), (𝒜_G/𝓘)|_{S(𝓘)}), the quotient (KLocallyRingedSpace.quotient) of (G, 𝒜_G) by 𝓘.

The local-model clause #

AnalyticSpace K extends KLocallyRingedSpace K by the fields locallyModel (i), sigmaCompact (ii) and t2 (iii), following the pattern of AlgebraicGeometry.Scheme. Clause (i) is stated up to an open of the model: X|U ≅ (localModel G f)|W for an open W of the local model (S(𝓘), (𝒜_G/𝓘)|_{S(𝓘)}). An open subset of a local analytic K-space is again a local analytic K-space (W = S(𝓘) ∩ G' for an open G' ⊆ G, and (localModel G f)|W is the local model of the restricted equations on G'), so the two forms define the same class of spaces. The form with W makes the open subspace X|U of an analytic space an analytic space by a formal argument (open immersions with equal ranges are isomorphic, KLocallyRingedSpace.isoOfRangeEq), whereas the literal form would need that identification of restricted models first, which is a theorem about the quotient construction (localModel_restrictOpen_iso) and not a definition.

Main definitions #

AnalyticSpace K, whose carrier is Hausdorff (t2) and σ-compact (sigmaCompact);
the category An/K: X ⟶ Y (AnalyticSpace.Hom X Y) are the K-morphisms of the underlying K-local-ringed spaces (a full subcategory), Hom.toFun the underlying map (the coercion ⇑f); an isomorphism of analytic spaces is an isomorphism in An/K (Mathlib's IsIso);
regularLocus X, the simple points (x is simple if 𝒪_{X,x} is a regular local ring, IsRegularLocalRing), singularLocus X its complement, and IsNonsingular (no multiple points);
IsReduced X: the structure sheaf has no nilpotents, read through the stalks (every stalk is reduced, which is equivalent to every ring of sections being reduced).

These are the objects the resolution theorem for analytic spaces (AnalyticSpace.exists_functorial_resolution) quantifies over.

Analytic K-spaces #

The local models #

The local-model clause #

Main definitions #

The local models #

Analytic spaces #

Analytic `K`-spaces #