A non-singular analytic space as the coproduct of its strata

For a non-singular analytic K-space X, the strata X_d = {x | dim 𝒪_{X,x} = d} (dimOpens) are open, pairwise disjoint and cover X, and each is K-isomorphic to the space of the manifold stratumManifold X hX d modelled on K^d (stratumKIso, Hironaka.AnalyticSpace.Manifold.StratumIso). The morphisms stratumIncl d : Sp(X_d) ⟶ X (the isomorphism followed by the open immersion X | X_d ⟶ X) are therefore open immersions with pairwise disjoint images covering X, so their descent ∐ d, Sp(X_d) ⟶ X is an isomorphism (isIso_sigmaDesc_of_isOpenImmersion); stratumSigmaIso : X ≅ ∐ d, Sp(X_d) is its inverse, and a point has local dimension d exactly when its image lies in the d-th summand (ringKrullDim_eq_iff_exists).

This is the disjoint-union form of Hironaka's description of a non-singular analytic space as locally the space of an open subset of some K^d [Hir64, Ch. 0, §1, p. 121]: a non-singular analytic space is the space of a manifold whose components may have different dimensions. It is used to apply results proved for the spaces of manifolds of one dimension to arbitrary non-singular analytic spaces (Hironaka.AnalyticSpace.SigmaCoproductLemmas).

@[reducible, inline]

noncomputable abbrev AnalyticSpace.stratumSpaceOf {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : ℕ) : AnalyticSpace K

Sp of the d-th stratum, with the identity coordinates on K^d.

Equations

• X.stratumSpaceOf hX d = AnalyticSpace.toSpace (ContinuousLinearEquiv.refl K (Fin d → K)) (X.stratumManifold hX d)

noncomputable def AnalyticSpace.stratumIncl {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : ℕ) : X.stratumSpaceOf hX d ⟶ X

The morphism Sp(X_d) ⟶ X: the isomorphism Sp(X_d) ≅ X | X_d followed by the open immersion X | X_d ⟶ X.

Equations

• X.stratumIncl hX d = CategoryTheory.CategoryStruct.comp (X.stratumKIso hX d).hom (X.ofRestrict (X.dimOpens hX d))

instance AnalyticSpace.isOpenImmersion_stratumIncl {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : ℕ) : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion ↑(X.stratumIncl hX d)

Sp(X_d) ⟶ X is an open immersion (an isomorphism followed by an open immersion).

theorem AnalyticSpace.toFun_stratumIncl_mem {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : ℕ) (m : ↑↑(X.stratumSpaceOf hX d).toPresheafedSpace) : ↑(X.stratumIncl hX d) m ∈ X.dimSet d

The image of Sp(X_d) ⟶ X lies in the stratum X_d.

theorem AnalyticSpace.exists_toFun_stratumIncl_eq {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) {d : ℕ} {x : ↑↑X.toPresheafedSpace} (hx : x ∈ X.dimSet d) : ∃ (m : ↑↑(X.stratumSpaceOf hX d).toPresheafedSpace), ↑(X.stratumIncl hX d) m = x

Every point of the stratum X_d is in the image of Sp(X_d) ⟶ X.

noncomputable def AnalyticSpace.stratumDesc {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) : (sigma fun (d : ℕ) => X.stratumSpaceOf hX d) ⟶ X

The descent ∐ d, Sp(X_d) ⟶ X of the inclusions of the strata.

Equations

• X.stratumDesc hX = AnalyticSpace.sigmaDesc (X.stratumIncl hX)

theorem AnalyticSpace.isIso_stratumDesc {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) : CategoryTheory.IsIso (X.stratumDesc hX)

The descent of the strata is an isomorphism: the Sp(X_d) ⟶ X are open immersions with pairwise disjoint images (a point has one local dimension) covering X (iUnion_dimSet_eq_univ).

noncomputable def AnalyticSpace.stratumSigmaIso {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) : X ≅ sigma fun (d : ℕ) => X.stratumSpaceOf hX d

A non-singular analytic K-space is the coproduct of its pure-dimensional strata, X ≅ ∐ d, Sp(X_d) [Hir64, Ch. 0, §1, p. 121].

Equations

• X.stratumSigmaIso hX = (CategoryTheory.asIso (X.stratumDesc hX)).symm

theorem AnalyticSpace.toFun_stratumSigmaIso_hom_eq_iff {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : ℕ) (x : ↑↑X.toPresheafedSpace) (m : ↑↑(X.stratumSpaceOf hX d).toPresheafedSpace) : ↑(X.stratumSigmaIso hX).hom x = ↑(sigmaι (fun (d : ℕ) => X.stratumSpaceOf hX d) d) m ↔ x = ↑(X.stratumIncl hX d) m

Under X ≅ ∐ d, Sp(X_d), a point of X goes to the point m of the d-th summand exactly when it is the image of m under Sp(X_d) ⟶ X.

theorem AnalyticSpace.ringKrullDim_eq_iff_exists {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : ℕ) (x : ↑↑X.toPresheafedSpace) : ringKrullDim ↑(X.presheaf.stalk x) = ↑d ↔ ∃ (m : (X.stratumManifold hX d).carrier), ↑(X.stratumSigmaIso hX).hom x = ↑(sigmaι (fun (d : ℕ) => X.stratumSpaceOf hX d) d) m

Under X ≅ ∐ d, Sp(X_d), the points of local dimension d are exactly the points of the d-th summand.