Documentation

Hironaka.AnalyticSpace.Manifold.Stratum

The dimension strata of a non-singular analytic space are analytic manifolds #

On a non-singular analytic K-space X, every point x has an open neighbourhood V and a K-isomorphism (G', ๐’œ_{G'}) โ‰… X | V with G' โŠ† K^d open and d = dim ๐’ช_{X,x}, by Hironaka's characterization of the simple points [Hir64, Ch. 0, ยง1, p. 121] (isRegular_stalk_iff_exists_manifold_nhd), and every point of V then has dimension d. Hence

This is the manifold half of the statement that a smooth space is a manifold, locally pure-dimensional [BM97, (3.8)(2)]; the K-isomorphism Sp(X_d) โ‰… X | X_d completing it is Hironaka.AnalyticSpace.Manifold.StratumIso.

The dimension strata #

source
def AnalyticSpace.dimSet {K : Type} [RCLike K] (X : AnalyticSpace K) (d : โ„•) :
Set โ†‘โ†‘X.toPresheafedSpace

The points of local dimension d: X_d = {x | dim ๐’ช_{X,x} = d}.

Equations
Instances For
    source
    theorem AnalyticSpace.mem_reg_of_isNonsingular {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (x : โ†‘โ†‘X.toPresheafedSpace) :
    x โˆˆ X.regularLocus
    source
    theorem AnalyticSpace.mem_dimSet_of_chart {K : Type} [RCLike K] (X : AnalyticSpace K) {V : TopologicalSpace.Opens โ†‘โ†‘X.toPresheafedSpace} {d : โ„•} {G' : TopologicalSpace.Opens (Kn K d)} (e : (analyticSpaceOfOpen K d G').KIso (X.restrictOpen V)) (q : โ†‘โ†‘(analyticSpaceOfOpen K d G').toPresheafedSpace) :
    โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘e.hom).base) q) โˆˆ X.dimSet d

    Every point of a chart neighbourhood X | V โ‰… (G', ๐’œ_{G'}), G' โŠ† K^d, has dimension d.

    source
    theorem AnalyticSpace.subset_dimSet_of_chart {K : Type} [RCLike K] (X : AnalyticSpace K) {V : TopologicalSpace.Opens โ†‘โ†‘X.toPresheafedSpace} {d : โ„•} {G' : TopologicalSpace.Opens (Kn K d)} (e : (analyticSpaceOfOpen K d G').KIso (X.restrictOpen V)) :
    โ†‘V โŠ† X.dimSet d
    source
    theorem AnalyticSpace.exists_chart_of_mem_dimSet {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) {d : โ„•} {x : โ†‘โ†‘X.toPresheafedSpace} (hx : x โˆˆ X.dimSet d) :
    โˆƒ (V : TopologicalSpace.Opens โ†‘โ†‘X.toPresheafedSpace) (_ : x โˆˆ V) (G' : TopologicalSpace.Opens (Kn K d)), Nonempty ((analyticSpaceOfOpen K d G').KIso (X.restrictOpen V))

    At a point of dimension d of a non-singular space there is a chart (G', ๐’œ_{G'}) โ‰… X | V, G' โŠ† K^d [Hir64, Ch. 0, ยง1, p. 121].

    source
    theorem AnalyticSpace.isOpen_dimSet {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : โ„•) :
    IsOpen (X.dimSet d)

    The dimension is locally constant on a non-singular space: each stratum X_d is open.

    source
    theorem AnalyticSpace.iUnion_dimSet_eq_univ {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) :
    โ‹ƒ (d : โ„•), X.dimSet d = Set.univ

    The strata cover the space: every stalk of a non-singular space has finite dimension.

    source
    def AnalyticSpace.dimOpens {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : โ„•) :
    TopologicalSpace.Opens โ†‘โ†‘X.toPresheafedSpace

    The stratum X_d as an open of X.

    Equations
    Instances For

      The charts #

      source
      noncomputable def AnalyticSpace.chartV {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : โ„•) (x : โ†ฅ(X.dimOpens hX d)) :
      TopologicalSpace.Opens โ†‘โ†‘X.toPresheafedSpace

      The chart neighbourhood of a point of the stratum (a choice).

      Equations
      Instances For
        source
        theorem AnalyticSpace.mem_chartV {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : โ„•) (x : โ†ฅ(X.dimOpens hX d)) :
        โ†‘x โˆˆ X.chartV hX d x
        source
        noncomputable def AnalyticSpace.chartG {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : โ„•) (x : โ†ฅ(X.dimOpens hX d)) :
        TopologicalSpace.Opens (Kn K d)

        The open G' โŠ† K^d of the chart.

        Equations
        Instances For
          source
          noncomputable def AnalyticSpace.chartE {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : โ„•) (x : โ†ฅ(X.dimOpens hX d)) :
          (analyticSpaceOfOpen K d (X.chartG hX d x)).KIso (X.restrictOpen (X.chartV hX d x))

          The K-isomorphism (G', ๐’œ_{G'}) โ‰… X | V of the chart.

          Equations
          Instances For
            source
            theorem AnalyticSpace.chartV_subset {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : โ„•) (x : โ†ฅ(X.dimOpens hX d)) :
            โ†‘(X.chartV hX d x) โŠ† X.dimSet d
            source
            noncomputable def AnalyticSpace.chartHomeo {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : โ„•) (x : โ†ฅ(X.dimOpens hX d)) :
            โ†‘โ†‘(analyticSpaceOfOpen K d (X.chartG hX d x)).toPresheafedSpace โ‰ƒโ‚œ โ†‘โ†‘(X.restrictOpen (X.chartV hX d x)).toPresheafedSpace

            The homeomorphism G' โ‰ƒโ‚œ V underlying the chart isomorphism.

            Equations
            Instances For
              source
              theorem AnalyticSpace.chartHomeo_apply {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : โ„•) (x : โ†ฅ(X.dimOpens hX d)) (q : โ†‘โ†‘(analyticSpaceOfOpen K d (X.chartG hX d x)).toPresheafedSpace) :
              (X.chartHomeo hX d x) q = (CategoryTheory.ConcreteCategory.hom (โ†‘(X.chartE hX d x).hom).base) q
              source
              noncomputable def AnalyticSpace.chartPt {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x : โ†ฅ(X.dimOpens hX d)) (q : โ†‘โ†‘(analyticSpaceOfOpen K d (X.chartG hX d x)).toPresheafedSpace) :
              โ†ฅ(X.dimOpens hX d)

              The point of the stratum under a point of the chart's open G'.

              Equations
              Instances For
                source
                theorem AnalyticSpace.chartPt_val {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x : โ†ฅ(X.dimOpens hX d)) (q : โ†‘โ†‘(analyticSpaceOfOpen K d (X.chartG hX d x)).toPresheafedSpace) :
                โ†‘(chartPt x q) = โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘(X.chartE hX d x).hom).base) q)
                source
                noncomputable def AnalyticSpace.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) :
                Fin d โ†’ K

                The chart coordinates of a point of V, in K^d.

                Equations
                Instances For
                  source
                  theorem AnalyticSpace.stratumCoord_chartPt {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x : โ†ฅ(X.dimOpens hX d)) (q : โ†‘โ†‘(analyticSpaceOfOpen K d (X.chartG hX d x)).toPresheafedSpace) :
                  stratumCoord x (chartPt x q) โ‹ฏ = (โ†‘q).down
                  source
                  theorem AnalyticSpace.continuous_stratumCoord {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x : โ†ฅ(X.dimOpens hX d)) :
                  Continuous fun (w : { w : โ†ฅ(X.dimOpens hX d) // โ†‘w โˆˆ X.chartV hX d x }) => stratumCoord x โ†‘w โ‹ฏ
                  source
                  theorem AnalyticSpace.continuous_chartPt {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x : โ†ฅ(X.dimOpens hX d)) :
                  Continuous fun (z : { z : Fin d โ†’ K // { down := z } โˆˆ X.chartG hX d x }) => chartPt x โŸจ{ down := โ†‘z }, โ‹ฏโŸฉ
                  source
                  noncomputable def AnalyticSpace.stratumChart {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x : โ†ฅ(X.dimOpens hX d)) :
                  OpenPartialHomeomorph (โ†ฅ(X.dimOpens hX d)) (Fin d โ†’ K)

                  The chart of the stratum at x: on V_x โˆฉ X_d, the coordinates w โ†ฆ e_xโปยน(w) โˆˆ G'_x โŠ† K^d.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem AnalyticSpace.stratumChart_source {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x : โ†ฅ(X.dimOpens hX d)) :
                    (stratumChart x).source = {w : โ†ฅ(X.dimOpens hX d) | โ†‘w โˆˆ X.chartV hX d x}
                    source
                    theorem AnalyticSpace.stratumChart_target {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x : โ†ฅ(X.dimOpens hX d)) :
                    (stratumChart x).target = {z : Fin d โ†’ K | { down := z } โˆˆ X.chartG hX d x}
                    source
                    theorem AnalyticSpace.stratumChart_apply {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x : โ†ฅ(X.dimOpens hX d)) {w : โ†ฅ(X.dimOpens hX d)} (hw : โ†‘w โˆˆ X.chartV hX d x) :
                    โ†‘(stratumChart x) w = stratumCoord x w hw
                    source
                    theorem AnalyticSpace.stratumChart_symm_apply {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x : โ†ฅ(X.dimOpens hX d)) {z : Fin d โ†’ K} (hz : { down := z } โˆˆ X.chartG hX d x) :
                    โ†‘(stratumChart x).symm z = chartPt x โŸจ{ down := z }, hzโŸฉ
                    source
                    theorem AnalyticSpace.mem_stratumChart_source {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x : โ†ฅ(X.dimOpens hX d)) :
                    x โˆˆ (stratumChart x).source
                    source
                    @[instance_reducible]
                    noncomputable instance AnalyticSpace.instChartedSpaceDimOpens {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : โ„•) :
                    ChartedSpace (Fin d โ†’ K) โ†ฅ(X.dimOpens hX d)

                    The atlas of the stratum.

                    Equations
                    source
                    theorem AnalyticSpace.chartAt_eq {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : โ„•) (x : โ†ฅ(X.dimOpens hX d)) :
                    chartAt (Fin d โ†’ K) x = stratumChart x

                    Chart changes are analytic #

                    source
                    noncomputable def AnalyticSpace.overlapOpens {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) :
                    TopologicalSpace.Opens โ†‘โ†‘(analyticSpaceOfOpen K d (X.chartG hX d x)).toPresheafedSpace

                    The overlap V_x โˆฉ V_y, seen in G'_x.

                    Equations
                    Instances For
                      source
                      theorem AnalyticSpace.mem_overlapOpens {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) {q : โ†‘โ†‘(analyticSpaceOfOpen K d (X.chartG hX d x)).toPresheafedSpace} :
                      q โˆˆ overlapOpens x y โ†” โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘(X.chartE hX d x).hom).base) q) โˆˆ X.chartV hX d y
                      source
                      noncomputable def AnalyticSpace.overlapIncl {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) :
                      (analyticSpaceOfOpen K d (X.chartG hX d x)).restrictOpen (overlapOpens x y) โŸถ X.toKLocallyRingedSpace

                      The open immersion (G'_x, ๐’œ) | (V_x โˆฉ V_y) โŸถ X.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        instance AnalyticSpace.isOpenImmersion_overlapIncl {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) :
                        AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion โ†‘(overlapIncl x y)
                        source
                        theorem AnalyticSpace.overlapIncl_base_apply {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) (p : โ†‘โ†‘((analyticSpaceOfOpen K d (X.chartG hX d x)).restrictOpen (overlapOpens x y)).toPresheafedSpace) :
                        (CategoryTheory.ConcreteCategory.hom (โ†‘(overlapIncl x y)).base) p = โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘(X.chartE hX d x).hom).base) โ†‘p)
                        source
                        theorem AnalyticSpace.range_overlapIncl {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) :
                        Set.range (KLocallyRingedSpace.Hom.toFun (overlapIncl x y)) = โ†‘(X.chartV hX d x) โˆฉ โ†‘(X.chartV hX d y)
                        source
                        noncomputable def AnalyticSpace.transitionIso {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) :
                        (analyticSpaceOfOpen K d (X.chartG hX d x)).restrictOpen (overlapOpens x y) โ‰… (analyticSpaceOfOpen K d (X.chartG hX d y)).restrictOpen (overlapOpens y x)

                        The transition K-isomorphism between the overlaps read in the two charts.

                        Equations
                        Instances For
                          source
                          theorem AnalyticSpace.transitionIso_hom_base {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) (p : โ†‘โ†‘((analyticSpaceOfOpen K d (X.chartG hX d x)).restrictOpen (overlapOpens x y)).toPresheafedSpace) :
                          โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘(X.chartE hX d y).hom).base) โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘(transitionIso x y).hom).base) p)) = โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘(X.chartE hX d x).hom).base) โ†‘p)
                          source
                          noncomputable def AnalyticSpace.overlapTrace {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) :
                          TopologicalSpace.Opens (Kn K d)

                          The trace of the overlap on K^d: an open G'' โ‰ค G'_x.

                          Equations
                          Instances For
                            source
                            theorem AnalyticSpace.overlapTrace_le {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) :
                            overlapTrace x y โ‰ค X.chartG hX d x
                            source
                            theorem AnalyticSpace.mem_overlapOpens_iff {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) (p : โ†‘โ†‘(analyticSpaceOfOpen K d (X.chartG hX d x)).toPresheafedSpace) :
                            p โˆˆ overlapOpens x y โ†” โ†‘p โˆˆ overlapTrace x y
                            source
                            noncomputable def AnalyticSpace.overlapTraceIso {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) :
                            (analyticSpaceOfOpen K d (X.chartG hX d x)).restrictOpen (overlapOpens x y) โ‰… analyticSpaceOfOpen K d (overlapTrace x y)

                            The overlap flattened to (G'', ๐’œ_{G''}) (traceIso).

                            Equations
                            Instances For
                              source
                              theorem AnalyticSpace.overlapTraceIso_inv_base {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) (p : โ†‘โ†‘(analyticSpaceOfOpen K d (overlapTrace x y)).toPresheafedSpace) :
                              โ†‘โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘(overlapTraceIso x y).inv).base) p) = โ†‘p
                              source
                              theorem AnalyticSpace.overlapTraceIso_hom_base {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) (p : โ†‘โ†‘((analyticSpaceOfOpen K d (X.chartG hX d x)).restrictOpen (overlapOpens x y)).toPresheafedSpace) :
                              โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘(overlapTraceIso x y).hom).base) p) = โ†‘โ†‘p
                              source
                              noncomputable def AnalyticSpace.transitionManifoldIso {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) :
                              (KLocallyRingedSpace.ofManifold K (Kn K d) โ†ฅ(overlapTrace x y)).KIso (KLocallyRingedSpace.ofManifold K (Kn K d) โ†ฅ(overlapTrace y x))

                              The transition, as a K-isomorphism of the spaces of the open submanifolds G''_x, G''_y of K^d.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                theorem AnalyticSpace.ofManifold_restrictOpen_iso_hom_base {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (U : TopologicalSpace.Opens M) (p : โ†‘โ†‘((KLocallyRingedSpace.ofManifold K E M).restrictOpen U).toPresheafedSpace) :
                                โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘(KLocallyRingedSpace.ofManifold_restrictOpen_iso U).hom).base) p) = โ†‘p
                                source
                                theorem AnalyticSpace.ofManifold_restrictOpen_iso_inv_base {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (U : TopologicalSpace.Opens M) (q : โ†ฅU) :
                                โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘(KLocallyRingedSpace.ofManifold_restrictOpen_iso U).inv).base) q) = โ†‘q
                                source
                                noncomputable def AnalyticSpace.transitionFun {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) :
                                โ†ฅ(overlapTrace x y) โ†’ โ†ฅ(overlapTrace y x)

                                The underlying map of the transition.

                                Equations
                                Instances For
                                  source
                                  theorem AnalyticSpace.contMDiff_transitionFun {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) :
                                  ContMDiff (modelWithCornersSelf K (Kn K d)) (modelWithCornersSelf K (Kn K d)) โŠค (transitionFun x y)
                                  source
                                  theorem AnalyticSpace.chartE_transitionFun {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) (p : โ†ฅ(overlapTrace x y)) :
                                  โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘(X.chartE hX d y).hom).base) โŸจโ†‘(transitionFun x y p), โ‹ฏโŸฉ) = โ†‘((CategoryTheory.ConcreteCategory.hom (โ†‘(X.chartE hX d x).hom).base) โŸจโ†‘p, โ‹ฏโŸฉ)

                                  The transition preserves the point of X: e_y (ฯ„ p) = e_x p in X.

                                  source
                                  noncomputable def AnalyticSpace.transitionExt {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) :
                                  Kn K d โ†’ Kn K d

                                  The extension by an arbitrary value of the transition to K^d.

                                  Equations
                                  Instances For
                                    source
                                    theorem AnalyticSpace.transitionExt_of_mem {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) {w : Kn K d} (hw : w โˆˆ overlapTrace x y) :
                                    transitionExt x y w = โ†‘(transitionFun x y โŸจw, hwโŸฉ)
                                    source
                                    theorem AnalyticSpace.contMDiffOn_transitionExt {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) :
                                    ContMDiffOn (modelWithCornersSelf K (Kn K d)) (modelWithCornersSelf K (Kn K d)) โŠค (transitionExt x y) โ†‘(overlapTrace x y)
                                    source
                                    theorem AnalyticSpace.contDiffOn_transitionExt {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) :
                                    ContDiffOn K โŠค (transitionExt x y) โ†‘(overlapTrace x y)
                                    source
                                    theorem AnalyticSpace.stratumChart_trans_apply {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) {z : Fin d โ†’ K} (hz : z โˆˆ ((stratumChart x).symm.trans (stratumChart y)).source) :
                                    โ†‘(stratumChart y) (โ†‘(stratumChart x).symm z) = (transitionExt x y { down := z }).down

                                    The chart change of the stratum at a point of its domain is the transition.

                                    source
                                    theorem AnalyticSpace.stratumChart_trans_source_subset {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) :
                                    ((stratumChart x).symm.trans (stratumChart y)).source โŠ† (fun (z : Fin d โ†’ K) => { down := z }) โปยน' โ†‘(overlapTrace x y)
                                    source
                                    theorem AnalyticSpace.contDiffOn_stratumChart_trans {K : Type} [RCLike K] {X : AnalyticSpace K} {hX : X.IsNonsingular} {d : โ„•} (x y : โ†ฅ(X.dimOpens hX d)) :
                                    ContDiffOn K โŠค (โ†‘((stratumChart x).symm.trans (stratumChart y))) ((stratumChart x).symm.trans (stratumChart y)).source

                                    The chart changes of the stratum are analytic.

                                    source
                                    instance AnalyticSpace.instIsManifoldDimOpens {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : โ„•) :
                                    IsManifold (modelWithCornersSelf K (Fin d โ†’ K)) โŠค โ†ฅ(X.dimOpens hX d)

                                    The stratum X_d is an analytic manifold modelled on K^d.

                                    source
                                    instance AnalyticSpace.instT2SpaceDimOpens {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : โ„•) :
                                    T2Space โ†ฅ(X.dimOpens hX d)
                                    source
                                    instance AnalyticSpace.instSecondCountableDimOpens {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : โ„•) :
                                    SecondCountableTopology โ†ฅ(X.dimOpens hX d)
                                    source
                                    noncomputable def AnalyticSpace.stratumManifold {K : Type} [RCLike K] (X : AnalyticSpace K) (hX : X.IsNonsingular) (d : โ„•) :
                                    AnalyticManifold K (Fin d โ†’ K)

                                    The stratum X_d as a bundled analytic manifold over K^d.

                                    Equations
                                    Instances For