Documentation

Hironaka.AnalyticSpace.Manifold.StratumIso

The stratum of a non-singular analytic space is the space of its manifold #

With X_d the stratum of dimension d of a non-singular analytic K-space X, an analytic manifold by Hironaka.AnalyticSpace.Manifold.Stratum, the comparison morphism Sp(X_d) ⟢ X | X_d (stratumHom) is the identity on points and sends a section s of π’ͺ_X to the function y ↦ ev_y(s_y) of its values at the simple points (regEval, Hironaka.AnalyticSpace.RegEval), which is analytic because through a chart e : (G', π’œ_{G'}) β‰… X | V it is the chart pullback e^* s composed with the chart (regEval_germ, contMDiff_stratumFun). Its stalk maps are local (evaluation is preserved, eval_stalkMap_stratumHomAux) and it respects the constants. It is an isomorphism (isIso_stratumHom, stratumKIso : Sp(X_d) β‰… X | X_d) because on every chart domain V_x it agrees, by the extensionality of morphisms between spaces of manifolds on their underlying maps (hom_ext_baseFun), with the composite of the known isomorphisms Sp(X_d) | V_x β‰… Sp(V_x) β‰… Sp(G'_x) β‰… X | V_x (stratumCompare_eq), so that its stalk maps are isomorphisms and the stalk criterion applies.

The three closing theorems state the result in set-theoretic form: isOpen_setOf_ringKrullDim_eq, iUnion_setOf_ringKrullDim_eq_univ, and exists_manifold_of_isNonsingular, which says that every stratum of a non-singular analytic space is K-isomorphic to the space of an analytic manifold modelled on K^d. This is Hironaka's description of the non-singular analytic spaces as those locally isomorphic to some (G, π’œ_G) [Hir64, Ch. 0, Β§1, p. 121] and Bierstone–Milman's "every smooth space is a manifold" [BM97, (3.8)(2)]; it is how the manifold-level theorems of the analytic strand are applied to the non-singular analytic spaces of the analytic-space main theorem.

source
@[reducible, inline]
abbrev AnalyticSpace.stratumImage {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) (W : TopologicalSpace.Opens β†₯(X.dimOpens hX d)) :
TopologicalSpace.Opens ↑↑X.toPresheafedSpace

The image in X of an open of the stratum.

Equations
Instances For
    source
    theorem AnalyticSpace.mem_stratumImage {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) {W : TopologicalSpace.Opens β†₯(X.dimOpens hX d)} (y : β†₯W) :
    ↑↑y ∈ X.stratumImage hX d W
    source
    noncomputable def AnalyticSpace.stratumEval {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) (W : TopologicalSpace.Opens β†₯(X.dimOpens hX d)) (y : β†₯W) :
    ↑(X.presheaf.obj (Opposite.op (X.stratumImage hX d W))) β†’+* K

    The evaluation at a point y of the stratum of the sections over (the image of) an open W βˆ‹ y of the stratum: s ↦ ev_y(s_y), a ring homomorphism.

    Equations
    Instances For
      source
      noncomputable def AnalyticSpace.stratumFun {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) (W : TopologicalSpace.Opens β†₯(X.dimOpens hX d)) (s : ↑(X.presheaf.obj (Opposite.op (X.stratumImage hX d W)))) (y : β†₯W) :
      K

      The function of a section s of π’ͺ_X over (the image of) an open W of the stratum: y ↦ ev_y(s_y).

      Equations
      Instances For
        source
        theorem AnalyticSpace.stratumFun_chartPt {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (W : TopologicalSpace.Opens β†₯(X.dimOpens hX d)) (s : ↑(X.presheaf.obj (Opposite.op (X.stratumImage hX d W)))) (x : β†₯(X.dimOpens hX d)) (q : ↑↑(analyticSpaceOfOpen K d (X.chartG hX d x)).toPresheafedSpace) (hq : chartPt x q ∈ W) :
        X.stratumFun hX d W s ⟨chartPt x q, hq⟩ = Manifold.extendSection K (Kn K d) (X.sectionViaChart (X.chartE hX d x) (X.stratumImage hX d W) s) ↑q

        The chart formula: at the point e_x(q) of the stratum the function of s is the value at q of the chart pullback of s.

        source
        theorem AnalyticSpace.chartPt_symm {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x w : β†₯(X.dimOpens hX d)) (hw : ↑w ∈ X.chartV hX d x) :
        chartPt x ((X.chartHomeo hX d x).symm βŸ¨β†‘w, hw⟩) = w

        The chart at x writes a point w of V_x as e_x(q), q = e_x⁻¹(w).

        source
        theorem AnalyticSpace.up_stratumCoord {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x w : β†₯(X.dimOpens hX d)) (hw : ↑w ∈ X.chartV hX d x) :
        { down := stratumCoord x w hw } = ↑((X.chartHomeo hX d x).symm βŸ¨β†‘w, hw⟩)
        source
        theorem AnalyticSpace.contMDiff_stratumFun {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (W : TopologicalSpace.Opens β†₯(X.dimOpens hX d)) (s : ↑(X.presheaf.obj (Opposite.op (X.stratumImage hX d W)))) :
        ContMDiff (modelWithCornersSelf K (Fin d β†’ K)) (modelWithCornersSelf K K) ⊀ (X.stratumFun hX d W s)

        The function of a section is analytic: near x it is the chart pullback of s, an analytic function on an open subset of K^d, composed with the chart.

        source
        @[reducible, inline]
        noncomputable abbrev AnalyticSpace.stratumSpace {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) :
        KLocallyRingedSpace K

        The stratum's space of the bundled manifold stratumManifold.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev AnalyticSpace.stratumRestrict {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) :
          KLocallyRingedSpace K

          The open subspace X | X_d.

          Equations
          Instances For
            source
            noncomputable def AnalyticSpace.stratumSheafHom {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) :
            (X.stratumRestrict hX d).presheaf ⟢ (TopCat.Presheaf.pushforward CommRingCat (CategoryTheory.CategoryStruct.id ↧β†₯(X.dimOpens hX d))).obj (Manifold.structureSheaf K (Fin d β†’ K) β†₯(X.dimOpens hX d)).presheaf

            The sheaf map of the comparison morphism: a section of π’ͺ_X goes to the function of its values.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def AnalyticSpace.stratumHomAux {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) :
              (X.stratumSpace hX d).toPresheafedSpace ⟢ (X.stratumRestrict hX d).toPresheafedSpace

              (Implementation.) The morphism of presheafed spaces Sp(X_d) ⟢ X | X_d: the identity on points, evaluation on sections.

              Equations
              Instances For
                source
                noncomputable def AnalyticSpace.stratumRegEval {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) (y : β†₯(X.dimOpens hX d)) :
                ↑((X.stratumRestrict hX d).presheaf.stalk y) β†’+* K

                The evaluation at a point y of the stratum on the stalk of the open subspace X | X_d.

                Equations
                Instances For
                  source
                  theorem AnalyticSpace.isLocalHom_stratumRegEval {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) (y : β†₯(X.dimOpens hX d)) :
                  IsLocalHom (X.stratumRegEval hX d y)
                  source
                  theorem AnalyticSpace.stratumRegEval_germ {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) (W : TopologicalSpace.Opens β†₯(X.dimOpens hX d)) (y : β†₯(X.dimOpens hX d)) (hy : y ∈ W) (s : ↑((X.stratumRestrict hX d).presheaf.obj (Opposite.op W))) :
                  (X.stratumRegEval hX d y) ((CategoryTheory.ConcreteCategory.hom ((X.stratumRestrict hX d).presheaf.germ W y hy)) s) = (X.stratumEval hX d W ⟨y, hy⟩) s
                  source
                  theorem AnalyticSpace.eval_stalkMap_stratumHomAux {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) (y : β†₯(X.dimOpens hX d)) (Οƒ : ↑((X.stratumRestrict hX d).presheaf.stalk y)) :
                  (Manifold.eval K (Fin d β†’ K) (β†₯(X.dimOpens hX d)) y) ((CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (X.stratumHomAux hX d) y)) Οƒ) = (X.stratumRegEval hX d y) Οƒ

                  Evaluation is preserved by the comparison morphism.

                  source
                  theorem AnalyticSpace.isLocalHom_stalkMap_stratumHomAux {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) (y : β†₯(X.dimOpens hX d)) :
                  IsLocalHom (CommRingCat.Hom.hom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (X.stratumHomAux hX d) y))
                  source
                  noncomputable def AnalyticSpace.stratumHomL {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) :
                  (X.stratumSpace hX d).toLocallyRingedSpace ⟢ (X.stratumRestrict hX d).toLocallyRingedSpace

                  (Implementation.) The morphism of locally ringed spaces Sp(X_d) ⟢ X | X_d.

                  Equations
                  Instances For
                    source
                    theorem AnalyticSpace.stratumHomL_Ξ“_algebraMap {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) (c : K) :
                    (CommRingCat.Hom.hom (AlgebraicGeometry.LocallyRingedSpace.Ξ“.map (X.stratumHomL hX d).op)) ((X.stratumRestrict hX d).algebraMap c) = (Manifold.constHom K (Fin d β†’ K) β†₯(X.dimOpens hX d)) c
                    source
                    noncomputable def AnalyticSpace.stratumHom {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) :
                    X.stratumSpace hX d ⟢ X.stratumRestrict hX d

                    The comparison K-morphism Sp(X_d) ⟢ X | X_d.

                    Equations
                    Instances For
                      source
                      theorem AnalyticSpace.stratumHom_base_apply {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) (y : β†₯(X.dimOpens hX d)) :
                      (CategoryTheory.ConcreteCategory.hom (↑(X.stratumHom hX d)).base) y = y

                      The comparison morphism is an isomorphism: comparison with Sp(chart) on each chart #

                      source
                      def AnalyticSpace.chartOpensD {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) :
                      TopologicalSpace.Opens β†₯(X.dimOpens hX d)

                      The chart domain V_x ∩ X_d as an open of the stratum.

                      Equations
                      Instances For
                        source
                        theorem AnalyticSpace.mem_chartOpensD {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) {w : β†₯(X.dimOpens hX d)} :
                        w ∈ chartOpensD x ↔ ↑w ∈ X.chartV hX d x
                        source
                        theorem AnalyticSpace.range_ofRestrict_comp_stratumHom {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) :
                        Set.range ⇑(CategoryTheory.ConcreteCategory.hom (↑(CategoryTheory.CategoryStruct.comp ((X.stratumSpace hX d).ofRestrict (chartOpensD x)) (X.stratumHom hX d))).base) βŠ† Set.range ⇑(CategoryTheory.ConcreteCategory.hom (↑((X.stratumRestrict hX d).ofRestrict (chartOpensD x))).base)
                        source
                        noncomputable def AnalyticSpace.stratumHomRestrict {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) :
                        (X.stratumSpace hX d).restrictOpen (chartOpensD x) ⟢ (X.stratumRestrict hX d).restrictOpen (chartOpensD x)

                        The restriction of the comparison morphism to a chart domain.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          theorem AnalyticSpace.stratumHomRestrict_comp {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) :
                          CategoryTheory.CategoryStruct.comp (stratumHomRestrict x) ((X.stratumRestrict hX d).ofRestrict (chartOpensD x)) = CategoryTheory.CategoryStruct.comp ((X.stratumSpace hX d).ofRestrict (chartOpensD x)) (X.stratumHom hX d)
                          source
                          theorem AnalyticSpace.stratumHomRestrict_base {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) (p : ↑↑((X.stratumSpace hX d).restrictOpen (chartOpensD x)).toPresheafedSpace) :
                          ↑((CategoryTheory.ConcreteCategory.hom (↑(stratumHomRestrict x)).base) p) = ↑p
                          source
                          theorem AnalyticSpace.imageOpens_chartOpensD {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) :
                          KLocallyRingedSpace.imageOpens (X.dimOpens hX d) (chartOpensD x) = X.chartV hX d x
                          source
                          theorem AnalyticSpace.eqToIso_restrictOpen_hom_base {K : Type} [RCLike K] {Y : KLocallyRingedSpace K} {U U' : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace} (h : U = U') (p : ↑↑(Y.restrictOpen U).toPresheafedSpace) :
                          ↑((CategoryTheory.ConcreteCategory.hom (↑(CategoryTheory.eqToIso β‹―).hom).base) p) = ↑p
                          source
                          noncomputable def AnalyticSpace.chartRestrictIso {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) :
                          (X.stratumRestrict hX d).restrictOpen (chartOpensD x) β‰… analyticSpaceOfOpen K d (X.chartG hX d x)

                          The chart domain of X | X_d, read as (G'_x, π’œ_{G'_x}) through the chart.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            theorem AnalyticSpace.chartRestrictIso_hom_base {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) (r : ↑↑((X.stratumRestrict hX d).restrictOpen (chartOpensD x)).toPresheafedSpace) :
                            ↑((CategoryTheory.ConcreteCategory.hom (↑(X.chartE hX d x).hom).base) ((CategoryTheory.ConcreteCategory.hom (↑(chartRestrictIso x).hom).base) r)) = ↑↑r
                            source
                            noncomputable def AnalyticSpace.chartMap {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) :
                            β†₯(chartOpensD x) β†’ β†₯(X.chartG hX d x)

                            The chart V_x ∩ X_d β†’ G'_x as a map of the open submanifolds.

                            Equations
                            Instances For
                              source
                              noncomputable def AnalyticSpace.chartMapInv {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) :
                              β†₯(X.chartG hX d x) β†’ β†₯(chartOpensD x)

                              The inverse chart G'_x β†’ V_x ∩ X_d.

                              Equations
                              Instances For
                                source
                                theorem AnalyticSpace.chartMap_chartInv {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) (q : β†₯(X.chartG hX d x)) :
                                chartMap x (chartMapInv x q) = q
                                source
                                theorem AnalyticSpace.chartInv_chartMap {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) (w : β†₯(chartOpensD x)) :
                                chartMapInv x (chartMap x w) = w
                                source
                                theorem AnalyticSpace.contMDiff_ulift_up {K : Type} [RCLike K] {d : β„•} :
                                ContMDiff (modelWithCornersSelf K (Fin d β†’ K)) (modelWithCornersSelf K (Kn K d)) ⊀ fun (z : Fin d β†’ K) => { down := z }
                                source
                                theorem AnalyticSpace.contMDiff_ulift_down {K : Type} [RCLike K] {d : β„•} :
                                ContMDiff (modelWithCornersSelf K (Kn K d)) (modelWithCornersSelf K (Fin d β†’ K)) ⊀ fun (w : Kn K d) => w.down
                                source
                                theorem AnalyticSpace.contMDiff_chartMap {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) :
                                ContMDiff (modelWithCornersSelf K (Fin d β†’ K)) (modelWithCornersSelf K (Kn K d)) ⊀ (chartMap x)
                                source
                                theorem AnalyticSpace.contMDiff_chartInv {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) :
                                ContMDiff (modelWithCornersSelf K (Kn K d)) (modelWithCornersSelf K (Fin d β†’ K)) ⊀ (chartMapInv x)
                                source
                                noncomputable def AnalyticSpace.chartKIsoM {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) :
                                (KLocallyRingedSpace.ofManifold K (Fin d β†’ K) β†₯(chartOpensD x)).KIso (KLocallyRingedSpace.ofManifold K (Kn K d) β†₯(X.chartG hX d x))

                                Sp of the chart, a K-isomorphism Sp(V_x ∩ X_d) β‰… Sp(G'_x).

                                Equations
                                Instances For
                                  source
                                  noncomputable def AnalyticSpace.stratumCompare {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) :
                                  KLocallyRingedSpace.ofManifold K (Fin d β†’ K) β†₯(chartOpensD x) ⟢ KLocallyRingedSpace.ofManifold K (Kn K d) β†₯(X.chartG hX d x)

                                  The comparison morphism on the chart domain, read between Sp(V_x ∩ X_d) and Sp(G'_x).

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    theorem AnalyticSpace.stratumCompare_eq {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) :
                                    stratumCompare x = (chartKIsoM x).hom

                                    On a chart domain the comparison morphism is Sp of the chart: the two K-morphisms Sp(V_x ∩ X_d) ⟢ Sp(G'_x) agree on points, hence are equal (hom_ext_baseFun).

                                    source
                                    theorem AnalyticSpace.isIso_stratumHomRestrict {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : β„•} (x : β†₯(X.dimOpens hX d)) :
                                    CategoryTheory.IsIso (stratumHomRestrict x)
                                    source
                                    theorem AnalyticSpace.isIso_stalkMap_stratumHom {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) (y : β†₯(X.dimOpens hX d)) :
                                    CategoryTheory.IsIso (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (↑(X.stratumHom hX d)) y)

                                    The stalk maps of the comparison morphism are isomorphisms: on the chart domain through y the morphism is Sp of the chart.

                                    source
                                    theorem AnalyticSpace.isIso_stratumHom {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) :
                                    CategoryTheory.IsIso (X.stratumHom hX d)

                                    The comparison morphism is a K-isomorphism (the stalk criterion; the base map is the identity).

                                    source
                                    noncomputable def AnalyticSpace.stratumKIso {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) :
                                    (X.stratumSpace hX d).KIso (X.stratumRestrict hX d)

                                    Sp(X_d) β‰… X | X_d.

                                    Equations
                                    Instances For

                                      The strata in set-theoretic form #

                                      source
                                      theorem AnalyticSpace.isOpen_setOf_ringKrullDim_eq {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) :
                                      IsOpen {x : ↑↑X.toPresheafedSpace | ringKrullDim ↑(X.presheaf.stalk x) = ↑d}

                                      The dimension is locally constant on a non-singular space: isOpen_dimSet (Hironaka.AnalyticSpace.Manifold.Stratum) with dimSet unfolded, the set-theoretic form used in the statement exists_manifold_of_isNonsingular.

                                      source
                                      theorem AnalyticSpace.iUnion_setOf_ringKrullDim_eq_univ {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) :
                                      ⋃ (d : β„•), {x : ↑↑X.toPresheafedSpace | ringKrullDim ↑(X.presheaf.stalk x) = ↑d} = Set.univ

                                      The strata cover a non-singular space: iUnion_dimSet_eq_univ (Hironaka.AnalyticSpace.Manifold.Stratum) with dimSet unfolded, the set-theoretic form of the statement.

                                      source
                                      theorem AnalyticSpace.exists_manifold_of_isNonsingular {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : β„•) :
                                      βˆƒ (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace), ↑U = {x : ↑↑X.toPresheafedSpace | ringKrullDim ↑(X.presheaf.stalk x) = ↑d} ∧ βˆƒ (M : AnalyticManifold K (Fin d β†’ K)), Nonempty ((toSpace (ContinuousLinearEquiv.refl K (Fin d β†’ K)) M).KIso (X.restrictOpen U))

                                      Every stratum of a non-singular analytic K-space is the space of an analytic manifold modelled on K^d [Hir64, Ch. 0, Β§1, p. 121], [BM97, (3.8)(2)]: Sp is essentially surjective onto the non-singular spaces, dimension by dimension. The stratum is quantified as an open set U whose carrier is the set of points of dimension d, so that the statement does not presuppose the openness lemma.