Documentation

Mathlib.Geometry.Manifold.ChartedSpace

Charted spaces #

A smooth manifold is a topological space M locally modelled on a euclidean space (or a euclidean half-space for manifolds with boundaries, or an infinite dimensional vector space for more general notions of manifolds), i.e., the manifold is covered by open subsets on which there are local homeomorphisms (the charts) going to a model space H, and the changes of charts should be smooth maps.

In this file, we introduce a general framework describing these notions, where the model space is an arbitrary topological space. We avoid the word manifold, which should be reserved for the situation where the model space is a (subset of a) vector space, and use the terminology charted space instead.

If the changes of charts satisfy some additional property (for instance if they are smooth), then M inherits additional structure (it makes sense to talk about smooth manifolds). There are therefore two different ingredients in a charted space:

We separate these two parts in the definition: the charted space structure is just the set of charts, and then the different smoothness requirements (smooth manifold, orientable manifold, contact manifold, and so on) are additional properties of these charts. These properties are formalized through the notion of structure groupoid, i.e., a set of partial homeomorphisms stable under composition and inverse, to which the change of coordinates should belong.

Main definitions #

As a basic example, we give the instance instance chartedSpaceSelf (H : Type*) [TopologicalSpace H] : ChartedSpace H H saying that a topological space is a charted space over itself, with the identity as unique chart. This charted space structure is compatible with any groupoid.

Additional useful definitions:

Implementation notes #

The atlas in a charted space is not a maximal atlas in general: the notion of maximality depends on the groupoid one considers, and changing groupoids changes the maximal atlas. With the current formalization, it makes sense first to choose the atlas, and then to ask whether this precise atlas defines a smooth manifold, an orientable manifold, and so on. A consequence is that structomorphisms between M and M' do not induce a bijection between the atlases of M and M': the definition is only that, read in charts, the structomorphism locally belongs to the groupoid under consideration. (This is equivalent to inducing a bijection between elements of the maximal atlas). A consequence is that the invariance under structomorphisms of properties defined in terms of the atlas is not obvious in general, and could require some work in theory (amounting to the fact that these properties only depend on the maximal atlas, for instance). In practice, this does not create any real difficulty.

We use the letter H for the model space thinking of the case of manifolds with boundary, where the model space is a half space.

Manifolds are sometimes defined as topological spaces with an atlas of local diffeomorphisms, and sometimes as spaces with an atlas from which a topology is deduced. We use the former approach: otherwise, there would be an instance from manifolds to topological spaces, which means that any instance search for topological spaces would try to find manifold structures involving a yet unknown model space, leading to problems. However, we also introduce the latter approach, through a structure ChartedSpaceCore making it possible to construct a topology out of a set of partial equivs with compatibility conditions (but we do not register it as an instance).

In the definition of a charted space, the model space is written as an explicit parameter as there can be several model spaces for a given topological space. For instance, a complex manifold (modelled over ℂ^n) will also be seen sometimes as a real manifold modelled over ℝ^(2n).

Notations #

In the locale Manifold, we denote the composition of partial homeomorphisms with ≫ₕ, and the composition of partial equivs with .

Structure groupoids #

One could add to the definition of a structure groupoid the fact that the restriction of an element of the groupoid to any open set still belongs to the groupoid. (This is in Kobayashi-Nomizu.) I am not sure I want this, for instance on H × E where E is a vector space, and the groupoid is made of functions respecting the fibers and linear in the fibers (so that a charted space over this groupoid is naturally a vector bundle) I prefer that the members of the groupoid are always defined on sets of the form s × E. There is a typeclass ClosedUnderRestriction for groupoids which have the restriction property.

The only nontrivial requirement is locality: if a partial homeomorphism belongs to the groupoid around each point in its domain of definition, then it belongs to the groupoid. Without this requirement, the composition of structomorphisms does not have to be a structomorphism. Note that this implies that a partial homeomorphism with empty source belongs to any structure groupoid, as it trivially satisfies this condition.

There is also a technical point, related to the fact that a partial homeomorphism is by definition a global map which is a homeomorphism when restricted to its source subset (and its values outside of the source are not relevant). Therefore, we also require that being a member of the groupoid only depends on the values on the source.

We use primes in the structure names as we will reformulate them below (without primes) using a Membership instance, writing e ∈ G instead of e ∈ G.members.

structure StructureGroupoid (H : Type u) [TopologicalSpace H] :

A structure groupoid is a set of partial homeomorphisms of a topological space stable under composition and inverse. They appear in the definition of the smoothness class of a manifold.

  • members : Set (PartialHomeomorph H H)

    Members of the structure groupoid are partial homeomorphisms.

  • trans' : ∀ (e e' : PartialHomeomorph H H), e self.memberse' self.memberse.trans e' self.members

    Structure groupoids are stable under composition.

  • symm' : eself.members, e.symm self.members

    Structure groupoids are stable under inverse.

  • id_mem' : PartialHomeomorph.refl H self.members

    The identity morphism lies in the structure groupoid.

  • locality' : ∀ (e : PartialHomeomorph H H), (∀ xe.source, ∃ (s : Set H), IsOpen s x s e.restr s self.members)e self.members

    Let e be a partial homeomorphism. If for every x ∈ e.source, the restriction of e to some open set around x lies in the groupoid, then e lies in the groupoid.

  • mem_of_eqOnSource' : ∀ (e e' : PartialHomeomorph H H), e self.memberse' ee' self.members

    Membership in a structure groupoid respects the equivalence of partial homeomorphisms.

Instances For
    theorem StructureGroupoid.trans' {H : Type u} [TopologicalSpace H] (self : StructureGroupoid H) (e : PartialHomeomorph H H) (e' : PartialHomeomorph H H) :
    e self.memberse' self.memberse.trans e' self.members

    Structure groupoids are stable under composition.

    theorem StructureGroupoid.symm' {H : Type u} [TopologicalSpace H] (self : StructureGroupoid H) (e : PartialHomeomorph H H) :
    e self.memberse.symm self.members

    Structure groupoids are stable under inverse.

    The identity morphism lies in the structure groupoid.

    theorem StructureGroupoid.locality' {H : Type u} [TopologicalSpace H] (self : StructureGroupoid H) (e : PartialHomeomorph H H) :
    (∀ xe.source, ∃ (s : Set H), IsOpen s x s e.restr s self.members)e self.members

    Let e be a partial homeomorphism. If for every x ∈ e.source, the restriction of e to some open set around x lies in the groupoid, then e lies in the groupoid.

    theorem StructureGroupoid.mem_of_eqOnSource' {H : Type u} [TopologicalSpace H] (self : StructureGroupoid H) (e : PartialHomeomorph H H) (e' : PartialHomeomorph H H) :
    e self.memberse' ee' self.members

    Membership in a structure groupoid respects the equivalence of partial homeomorphisms.

    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    theorem StructureGroupoid.trans {H : Type u} [TopologicalSpace H] (G : StructureGroupoid H) {e : PartialHomeomorph H H} {e' : PartialHomeomorph H H} (he : e G) (he' : e' G) :
    e.trans e' G
    theorem StructureGroupoid.symm {H : Type u} [TopologicalSpace H] (G : StructureGroupoid H) {e : PartialHomeomorph H H} (he : e G) :
    e.symm G
    theorem StructureGroupoid.locality {H : Type u} [TopologicalSpace H] (G : StructureGroupoid H) {e : PartialHomeomorph H H} (h : xe.source, ∃ (s : Set H), IsOpen s x s e.restr s G) :
    e G
    theorem StructureGroupoid.mem_of_eqOnSource {H : Type u} [TopologicalSpace H] (G : StructureGroupoid H) {e : PartialHomeomorph H H} {e' : PartialHomeomorph H H} (he : e G) (h : e' e) :
    e' G

    Partial order on the set of groupoids, given by inclusion of the members of the groupoid.

    Equations
    theorem StructureGroupoid.le_iff {H : Type u} [TopologicalSpace H] {G₁ : StructureGroupoid H} {G₂ : StructureGroupoid H} :
    G₁ G₂ eG₁, e G₂

    The trivial groupoid, containing only the identity (and maps with empty source, as this is necessary from the definition).

    Equations
    Instances For

      Every structure groupoid contains the identity groupoid.

      Equations
      Equations
      • instInhabitedStructureGroupoid = { default := idGroupoid H }
      structure Pregroupoid (H : Type u_5) [TopologicalSpace H] :
      Type u_5

      To construct a groupoid, one may consider classes of partial homeomorphisms such that both the function and its inverse have some property. If this property is stable under composition, one gets a groupoid. Pregroupoid bundles the properties needed for this construction, with the groupoid of smooth functions with smooth inverses as an application.

      • property : (HH)Set HProp

        Property describing membership in this groupoid: the pregroupoid "contains" all functions H → H having the pregroupoid property on some s : Set H

      • comp : ∀ {f g : HH} {u v : Set H}, self.property f uself.property g vIsOpen uIsOpen vIsOpen (u f ⁻¹' v)self.property (g f) (u f ⁻¹' v)

        The pregroupoid property is stable under composition

      • id_mem : self.property id Set.univ

        Pregroupoids contain the identity map (on univ)

      • locality : ∀ {f : HH} {u : Set H}, IsOpen u(∀ xu, ∃ (v : Set H), IsOpen v x v self.property f (u v))self.property f u

        The pregroupoid property is "local", in the sense that f has the pregroupoid property on u iff its restriction to each open subset of u has it

      • congr : ∀ {f g : HH} {u : Set H}, IsOpen u(∀ xu, g x = f x)self.property f uself.property g u

        If f = g on u and property f u, then property g u

      Instances For
        theorem Pregroupoid.comp {H : Type u_5} [TopologicalSpace H] (self : Pregroupoid H) {f : HH} {g : HH} {u : Set H} {v : Set H} :
        self.property f uself.property g vIsOpen uIsOpen vIsOpen (u f ⁻¹' v)self.property (g f) (u f ⁻¹' v)

        The pregroupoid property is stable under composition

        theorem Pregroupoid.id_mem {H : Type u_5} [TopologicalSpace H] (self : Pregroupoid H) :
        self.property id Set.univ

        Pregroupoids contain the identity map (on univ)

        theorem Pregroupoid.locality {H : Type u_5} [TopologicalSpace H] (self : Pregroupoid H) {f : HH} {u : Set H} :
        IsOpen u(∀ xu, ∃ (v : Set H), IsOpen v x v self.property f (u v))self.property f u

        The pregroupoid property is "local", in the sense that f has the pregroupoid property on u iff its restriction to each open subset of u has it

        theorem Pregroupoid.congr {H : Type u_5} [TopologicalSpace H] (self : Pregroupoid H) {f : HH} {g : HH} {u : Set H} :
        IsOpen u(∀ xu, g x = f x)self.property f uself.property g u

        If f = g on u and property f u, then property g u

        Construct a groupoid of partial homeos for which the map and its inverse have some property, from a pregroupoid asserting that this property is stable under composition.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem mem_groupoid_of_pregroupoid {H : Type u} [TopologicalSpace H] {PG : Pregroupoid H} {e : PartialHomeomorph H H} :
          e PG.groupoid PG.property (↑e) e.source PG.property (↑e.symm) e.target
          theorem groupoid_of_pregroupoid_le {H : Type u} [TopologicalSpace H] (PG₁ : Pregroupoid H) (PG₂ : Pregroupoid H) (h : ∀ (f : HH) (s : Set H), PG₁.property f sPG₂.property f s) :
          PG₁.groupoid PG₂.groupoid
          theorem mem_pregroupoid_of_eqOnSource {H : Type u} [TopologicalSpace H] (PG : Pregroupoid H) {e : PartialHomeomorph H H} {e' : PartialHomeomorph H H} (he' : e e') (he : PG.property (↑e) e.source) :
          PG.property (↑e') e'.source
          @[reducible, inline]

          The pregroupoid of all partial maps on a topological space H.

          Equations
          Instances For

            The groupoid of all partial homeomorphisms on a topological space H.

            Equations
            Instances For

              Every structure groupoid is contained in the groupoid of all partial homeomorphisms.

              Equations
              Equations

              A groupoid is closed under restriction if it contains all restrictions of its element local homeomorphisms to open subsets of the source.

              Instances
                theorem ClosedUnderRestriction.closedUnderRestriction {H : Type u} [TopologicalSpace H] {G : StructureGroupoid H} [self : ClosedUnderRestriction G] {e : PartialHomeomorph H H} :
                e G∀ (s : Set H), IsOpen se.restr s G
                theorem closedUnderRestriction' {H : Type u} [TopologicalSpace H] {G : StructureGroupoid H} [ClosedUnderRestriction G] {e : PartialHomeomorph H H} (he : e G) {s : Set H} (hs : IsOpen s) :
                e.restr s G

                The trivial restriction-closed groupoid, containing only partial homeomorphisms equivalent to the restriction of the identity to the various open subsets.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem idRestrGroupoid_mem {H : Type u} [TopologicalSpace H] {s : Set H} (hs : IsOpen s) :
                  PartialHomeomorph.ofSet s hs idRestrGroupoid

                  The trivial restriction-closed groupoid is indeed ClosedUnderRestriction.

                  Equations
                  • =

                  A groupoid is closed under restriction if and only if it contains the trivial restriction-closed groupoid.

                  The groupoid of all partial homeomorphisms on a topological space H is closed under restriction.

                  Equations
                  • =

                  Charted spaces #

                  theorem ChartedSpace.ext_iff {H : Type u_5} :
                  ∀ {inst : TopologicalSpace H} {M : Type u_6} {inst_1 : TopologicalSpace M} {x y : ChartedSpace H M}, x = y ChartedSpace.atlas = ChartedSpace.atlas ChartedSpace.chartAt = ChartedSpace.chartAt
                  theorem ChartedSpace.ext {H : Type u_5} :
                  ∀ {inst : TopologicalSpace H} {M : Type u_6} {inst_1 : TopologicalSpace M} {x y : ChartedSpace H M}, ChartedSpace.atlas = ChartedSpace.atlasChartedSpace.chartAt = ChartedSpace.chartAtx = y
                  class ChartedSpace (H : Type u_5) [TopologicalSpace H] (M : Type u_6) [TopologicalSpace M] :
                  Type (max u_5 u_6)

                  A charted space is a topological space endowed with an atlas, i.e., a set of local homeomorphisms taking value in a model space H, called charts, such that the domains of the charts cover the whole space. We express the covering property by choosing for each x a member chartAt x of the atlas containing x in its source: in the smooth case, this is convenient to construct the tangent bundle in an efficient way. The model space is written as an explicit parameter as there can be several model spaces for a given topological space. For instance, a complex manifold (modelled over ℂ^n) will also be seen sometimes as a real manifold over ℝ^(2n).

                  Instances
                    theorem ChartedSpace.mem_chart_source {H : Type u_5} [TopologicalSpace H] {M : Type u_6} [TopologicalSpace M] [self : ChartedSpace H M] (x : M) :
                    theorem ChartedSpace.chart_mem_atlas {H : Type u_5} [TopologicalSpace H] {M : Type u_6} [TopologicalSpace M] [self : ChartedSpace H M] (x : M) :
                    ChartedSpace.chartAt x ChartedSpace.atlas
                    @[reducible, inline]
                    abbrev atlas (H : Type u_5) [TopologicalSpace H] (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] :

                    The atlas of charts in a ChartedSpace.

                    Equations
                    • atlas H M = ChartedSpace.atlas
                    Instances For
                      @[reducible, inline]
                      abbrev chartAt (H : Type u_5) [TopologicalSpace H] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] (x : M) :

                      The preferred chart at a point x in a charted space M.

                      Equations
                      Instances For
                        @[simp]
                        theorem mem_chart_source (H : Type u_5) {M : Type u_6} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) :
                        x (chartAt H x).source
                        @[simp]
                        theorem chart_mem_atlas (H : Type u_5) {M : Type u_6} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) :
                        chartAt H x atlas H M

                        An empty type is a charted space over any topological space.

                        Equations
                        • ChartedSpace.empty H M = { atlas := , chartAt := fun (x : M) => .elim, mem_chart_source := , chart_mem_atlas := }
                        Instances For

                          Any space is a ChartedSpace modelled over itself, by just using the identity chart.

                          Equations
                          @[simp]

                          In the trivial ChartedSpace structure of a space modelled over itself through the identity, the atlas members are just the identity.

                          In the model space, chartAt is always the identity.

                          theorem mem_chart_target (H : Type u) {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) :
                          (chartAt H x) x (chartAt H x).target
                          theorem chart_source_mem_nhds (H : Type u) {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) :
                          (chartAt H x).source nhds x
                          theorem chart_target_mem_nhds (H : Type u) {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) :
                          (chartAt H x).target nhds ((chartAt H x) x)
                          @[simp]
                          theorem iUnion_source_chartAt (H : Type u) (M : Type u_2) [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] :
                          ⋃ (x : M), (chartAt H x).source = Set.univ
                          theorem ChartedSpace.isOpen_iff (H : Type u) {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (s : Set M) :
                          IsOpen s ∀ (x : M), IsOpen ((chartAt H x) '' ((chartAt H x).source s))
                          def achart (H : Type u) {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) :
                          (atlas H M)

                          achart H x is the chart at x, considered as an element of the atlas. Especially useful for working with BasicSmoothVectorBundleCore.

                          Equations
                          Instances For
                            theorem achart_def (H : Type u) {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) :
                            achart H x = chartAt H x,
                            @[simp]
                            theorem coe_achart (H : Type u) {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) :
                            (achart H x) = chartAt H x
                            @[simp]
                            theorem achart_val (H : Type u) {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) :
                            (achart H x) = chartAt H x
                            theorem mem_achart_source (H : Type u) {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) :
                            x (↑(achart H x)).source
                            theorem ChartedSpace.secondCountable_of_countable_cover (H : Type u) {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [SecondCountableTopology H] {s : Set M} (hs : xs, (chartAt H x).source = Set.univ) (hsc : s.Countable) :

                            If a topological space admits an atlas with locally compact charts, then the space itself is locally compact.

                            If a topological space admits an atlas with locally connected charts, then the space itself is locally connected.

                            def ChartedSpace.comp (H : Type u_5) [TopologicalSpace H] (H' : Type u_6) [TopologicalSpace H'] (M : Type u_7) [TopologicalSpace M] [ChartedSpace H H'] [ChartedSpace H' M] :

                            If M is modelled on H' and H' is itself modelled on H, then we can consider M as being modelled on H.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              theorem chartAt_comp (H : Type u_5) [TopologicalSpace H] (H' : Type u_6) [TopologicalSpace H'] {M : Type u_7} [TopologicalSpace M] [ChartedSpace H H'] [ChartedSpace H' M] (x : M) :
                              chartAt H x = (chartAt H' x).trans (chartAt H ((chartAt H' x) x))
                              def ModelProd (H : Type u_5) (H' : Type u_6) :
                              Type (max u_5 u_6)

                              Same thing as H × H'. We introduce it for technical reasons, see note [Manifold type tags].

                              Equations
                              Instances For
                                def ModelPi {ι : Type u_5} (H : ιType u_6) :
                                Type (max u_5 u_6)

                                Same thing as ∀ i, H i. We introduce it for technical reasons, see note [Manifold type tags].

                                Equations
                                Instances For
                                  instance modelProdInhabited {H : Type u} {H' : Type u_1} [Inhabited H] [Inhabited H'] :
                                  Equations
                                  • modelProdInhabited = instInhabitedProd
                                  Equations
                                  @[simp]
                                  theorem modelProd_range_prod_id {H : Type u_5} {H' : Type u_6} {α : Type u_7} (f : Hα) :
                                  (Set.range fun (p : ModelProd H H') => (f p.1, p.2)) = Set.range f ×ˢ Set.univ
                                  instance modelPiInhabited {ι : Type u_5} {Hi : ιType u_6} [(i : ι) → Inhabited (Hi i)] :
                                  Equations
                                  • modelPiInhabited = { default := fun (x : ι) => default }
                                  instance instTopologicalSpaceModelPi {ι : Type u_5} {Hi : ιType u_6} [(i : ι) → TopologicalSpace (Hi i)] :
                                  Equations
                                  • instTopologicalSpaceModelPi = Pi.topologicalSpace
                                  instance prodChartedSpace (H : Type u_5) [TopologicalSpace H] (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] (H' : Type u_7) [TopologicalSpace H'] (M' : Type u_8) [TopologicalSpace M'] [ChartedSpace H' M'] :
                                  ChartedSpace (ModelProd H H') (M × M')

                                  The product of two charted spaces is naturally a charted space, with the canonical construction of the atlas of product maps.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  theorem ModelProd.ext_iff {H : Type u} {H' : Type u_1} {x : ModelProd H H'} {y : ModelProd H H'} :
                                  x = y x.1 = y.1 x.2 = y.2
                                  theorem ModelProd.ext {H : Type u} {H' : Type u_1} {x : ModelProd H H'} {y : ModelProd H H'} (h₁ : x.1 = y.1) (h₂ : x.2 = y.2) :
                                  x = y
                                  @[simp]
                                  theorem prodChartedSpace_chartAt {H : Type u} {H' : Type u_1} {M : Type u_2} {M' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace H'] [TopologicalSpace M'] [ChartedSpace H' M'] {x : M × M'} :
                                  chartAt (ModelProd H H') x = (chartAt H x.1).prod (chartAt H' x.2)
                                  instance piChartedSpace {ι : Type u_5} [Finite ι] (H : ιType u_6) [(i : ι) → TopologicalSpace (H i)] (M : ιType u_7) [(i : ι) → TopologicalSpace (M i)] [(i : ι) → ChartedSpace (H i) (M i)] :
                                  ChartedSpace (ModelPi H) ((i : ι) → M i)

                                  The product of a finite family of charted spaces is naturally a charted space, with the canonical construction of the atlas of finite product maps.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  @[simp]
                                  theorem piChartedSpace_chartAt {ι : Type u_5} [Finite ι] (H : ιType u_6) [(i : ι) → TopologicalSpace (H i)] (M : ιType u_7) [(i : ι) → TopologicalSpace (M i)] [(i : ι) → ChartedSpace (H i) (M i)] (f : (i : ι) → M i) :
                                  chartAt (ModelPi H) f = PartialHomeomorph.pi fun (i : ι) => chartAt (H i) (f i)

                                  Constructing a topology from an atlas #

                                  structure ChartedSpaceCore (H : Type u_5) [TopologicalSpace H] (M : Type u_6) :
                                  Type (max u_5 u_6)

                                  Sometimes, one may want to construct a charted space structure on a space which does not yet have a topological structure, where the topology would come from the charts. For this, one needs charts that are only partial equivalences, and continuity properties for their composition. This is formalised in ChartedSpaceCore.

                                  • atlas : Set (PartialEquiv M H)

                                    An atlas of charts, which are only PartialEquivs

                                  • chartAt : MPartialEquiv M H

                                    The preferred chart at each point

                                  • mem_chart_source : ∀ (x : M), x (self.chartAt x).source
                                  • chart_mem_atlas : ∀ (x : M), self.chartAt x self.atlas
                                  • open_source : ∀ (e e' : PartialEquiv M H), e self.atlase' self.atlasIsOpen (e.symm.trans e').source
                                  • continuousOn_toFun : ∀ (e e' : PartialEquiv M H), e self.atlase' self.atlasContinuousOn (↑(e.symm.trans e')) (e.symm.trans e').source
                                  Instances For
                                    theorem ChartedSpaceCore.mem_chart_source {H : Type u_5} [TopologicalSpace H] {M : Type u_6} (self : ChartedSpaceCore H M) (x : M) :
                                    x (self.chartAt x).source
                                    theorem ChartedSpaceCore.chart_mem_atlas {H : Type u_5} [TopologicalSpace H] {M : Type u_6} (self : ChartedSpaceCore H M) (x : M) :
                                    self.chartAt x self.atlas
                                    theorem ChartedSpaceCore.open_source {H : Type u_5} [TopologicalSpace H] {M : Type u_6} (self : ChartedSpaceCore H M) (e : PartialEquiv M H) (e' : PartialEquiv M H) :
                                    e self.atlase' self.atlasIsOpen (e.symm.trans e').source
                                    theorem ChartedSpaceCore.continuousOn_toFun {H : Type u_5} [TopologicalSpace H] {M : Type u_6} (self : ChartedSpaceCore H M) (e : PartialEquiv M H) (e' : PartialEquiv M H) :
                                    e self.atlase' self.atlasContinuousOn (↑(e.symm.trans e')) (e.symm.trans e').source

                                    Topology generated by a set of charts on a Type.

                                    Equations
                                    Instances For
                                      theorem ChartedSpaceCore.open_source' {H : Type u} {M : Type u_2} [TopologicalSpace H] (c : ChartedSpaceCore H M) {e : PartialEquiv M H} (he : e c.atlas) :
                                      IsOpen e.source
                                      theorem ChartedSpaceCore.open_target {H : Type u} {M : Type u_2} [TopologicalSpace H] (c : ChartedSpaceCore H M) {e : PartialEquiv M H} (he : e c.atlas) :
                                      IsOpen e.target
                                      def ChartedSpaceCore.partialHomeomorph {H : Type u} {M : Type u_2} [TopologicalSpace H] (c : ChartedSpaceCore H M) (e : PartialEquiv M H) (he : e c.atlas) :

                                      An element of the atlas in a charted space without topology becomes a partial homeomorphism for the topology constructed from this atlas. The PartialHomeomorph version is given in this definition.

                                      Equations
                                      • c.partialHomeomorph e he = { toPartialEquiv := e, open_source := , open_target := , continuousOn_toFun := , continuousOn_invFun := }
                                      Instances For

                                        Given a charted space without topology, endow it with a genuine charted space structure with respect to the topology constructed from the atlas.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For

                                          Charted space with a given structure groupoid #

                                          class HasGroupoid {H : Type u_5} [TopologicalSpace H] (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] (G : StructureGroupoid H) :

                                          A charted space has an atlas in a groupoid G if the change of coordinates belong to the groupoid.

                                          Instances
                                            theorem HasGroupoid.compatible {H : Type u_5} [TopologicalSpace H] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} [self : HasGroupoid M G] {e : PartialHomeomorph M H} {e' : PartialHomeomorph M H} :
                                            e atlas H Me' atlas H Me.symm.trans e' G
                                            theorem StructureGroupoid.compatible {H : Type u_5} [TopologicalSpace H] (G : StructureGroupoid H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [HasGroupoid M G] {e : PartialHomeomorph M H} {e' : PartialHomeomorph M H} (he : e atlas H M) (he' : e' atlas H M) :
                                            e.symm.trans e' G

                                            Reformulate in the StructureGroupoid namespace the compatibility condition of charts in a charted space admitting a structure groupoid, to make it more easily accessible with dot notation.

                                            theorem hasGroupoid_of_le {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G₁ : StructureGroupoid H} {G₂ : StructureGroupoid H} (h : HasGroupoid M G₁) (hle : G₁ G₂) :
                                            theorem hasGroupoid_inf_iff {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G₁ : StructureGroupoid H} {G₂ : StructureGroupoid H} :
                                            HasGroupoid M (G₁ G₂) HasGroupoid M G₁ HasGroupoid M G₂
                                            theorem hasGroupoid_of_pregroupoid {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (PG : Pregroupoid H) (h : ∀ {e e' : PartialHomeomorph M H}, e atlas H Me' atlas H MPG.property (↑(e.symm.trans e')) (e.symm.trans e').source) :
                                            HasGroupoid M PG.groupoid

                                            The trivial charted space structure on the model space is compatible with any groupoid.

                                            Equations
                                            • =

                                            Any charted space structure is compatible with the groupoid of all partial homeomorphisms.

                                            Equations
                                            • =
                                            theorem StructureGroupoid.trans_restricted {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {e : PartialHomeomorph M H} {e' : PartialHomeomorph M H} {G : StructureGroupoid H} (he : e atlas H M) (he' : e' atlas H M) [HasGroupoid M G] [ClosedUnderRestriction G] {s : TopologicalSpace.Opens M} (hs : Nonempty s) :
                                            (e.subtypeRestr hs).symm.trans (e'.subtypeRestr hs) G

                                            If G is closed under restriction, the transition function between the restriction of two charts e and e' lies in G.

                                            Given a charted space admitting a structure groupoid, the maximal atlas associated to this structure groupoid is the set of all charts that are compatible with the atlas, i.e., such that changing coordinates with an atlas member gives an element of the groupoid.

                                            Equations
                                            Instances For

                                              The elements of the atlas belong to the maximal atlas for any structure groupoid.

                                              theorem mem_maximalAtlas_iff {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {e : PartialHomeomorph M H} :
                                              e StructureGroupoid.maximalAtlas M G e'atlas H M, e.symm.trans e' G e'.symm.trans e G

                                              Changing coordinates between two elements of the maximal atlas gives rise to an element of the structure groupoid.

                                              The maximal atlas of a structure groupoid is stable under equivalence.

                                              In the model space, the identity is in any maximal atlas.

                                              In the model space, any element of the groupoid is in the maximal atlas.

                                              def PartialHomeomorph.singletonChartedSpace {H : Type u} [TopologicalSpace H] {α : Type u_5} [TopologicalSpace α] (e : PartialHomeomorph α H) (h : e.source = Set.univ) :

                                              If a single partial homeomorphism e from a space α into H has source covering the whole space α, then that partial homeomorphism induces an H-charted space structure on α. (This condition is equivalent to e being an open embedding of α into H; see OpenEmbedding.singletonChartedSpace.)

                                              Equations
                                              • e.singletonChartedSpace h = { atlas := {e}, chartAt := fun (x : α) => e, mem_chart_source := , chart_mem_atlas := }
                                              Instances For
                                                @[simp]
                                                theorem PartialHomeomorph.singletonChartedSpace_chartAt_eq {H : Type u} [TopologicalSpace H] {α : Type u_5} [TopologicalSpace α] (e : PartialHomeomorph α H) (h : e.source = Set.univ) {x : α} :
                                                chartAt H x = e
                                                theorem PartialHomeomorph.singletonChartedSpace_chartAt_source {H : Type u} [TopologicalSpace H] {α : Type u_5} [TopologicalSpace α] (e : PartialHomeomorph α H) (h : e.source = Set.univ) {x : α} :
                                                (chartAt H x).source = Set.univ
                                                theorem PartialHomeomorph.singletonChartedSpace_mem_atlas_eq {H : Type u} [TopologicalSpace H] {α : Type u_5} [TopologicalSpace α] (e : PartialHomeomorph α H) (h : e.source = Set.univ) (e' : PartialHomeomorph α H) (h' : e' ChartedSpace.atlas) :
                                                e' = e
                                                theorem PartialHomeomorph.singleton_hasGroupoid {H : Type u} [TopologicalSpace H] {α : Type u_5} [TopologicalSpace α] (e : PartialHomeomorph α H) (h : e.source = Set.univ) (G : StructureGroupoid H) [ClosedUnderRestriction G] :

                                                Given a partial homeomorphism e from a space α into H, if its source covers the whole space α, then the induced charted space structure on α is HasGroupoid G for any structure groupoid G which is closed under restrictions.

                                                def OpenEmbedding.singletonChartedSpace {H : Type u} [TopologicalSpace H] {α : Type u_5} [TopologicalSpace α] [Nonempty α] {f : αH} (h : OpenEmbedding f) :

                                                An open embedding of α into H induces an H-charted space structure on α. See PartialHomeomorph.singletonChartedSpace.

                                                Equations
                                                Instances For
                                                  theorem OpenEmbedding.singletonChartedSpace_chartAt_eq {H : Type u} [TopologicalSpace H] {α : Type u_5} [TopologicalSpace α] [Nonempty α] {f : αH} (h : OpenEmbedding f) {x : α} :
                                                  (chartAt H x) = f

                                                  An open subset of a charted space is naturally a charted space.

                                                  Equations
                                                  • s.instChartedSpace = { atlas := ⋃ (x : s), {(chartAt H x).subtypeRestr }, chartAt := fun (x : s) => (chartAt H x).subtypeRestr , mem_chart_source := , chart_mem_atlas := }
                                                  theorem TopologicalSpace.Opens.chart_eq {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {s : TopologicalSpace.Opens M} (hs : Nonempty s) {e : PartialHomeomorph (↥s) H} (he : e atlas H s) :
                                                  ∃ (x : s), e = (chartAt H x).subtypeRestr hs

                                                  If s is a non-empty open subset of M, every chart of s is the restriction of some chart on M.

                                                  theorem TopologicalSpace.Opens.chart_eq' {H : Type u} [TopologicalSpace H] {t : TopologicalSpace.Opens H} (ht : Nonempty t) {e' : PartialHomeomorph (↥t) H} (he' : e' atlas H t) :
                                                  ∃ (x : t), e' = (chartAt H x).subtypeRestr ht

                                                  If t is a non-empty open subset of H, every chart of t is the restriction of some chart on H.

                                                  If a groupoid G is ClosedUnderRestriction, then an open subset of a space which is HasGroupoid G is naturally HasGroupoid G.

                                                  Equations
                                                  • =
                                                  theorem TopologicalSpace.Opens.chartAt_subtype_val_symm_eventuallyEq {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (U : TopologicalSpace.Opens M) {x : U} :
                                                  (chartAt H x).symm =ᶠ[nhds ((chartAt H x) x)] Subtype.val (chartAt H x).symm

                                                  Restricting a chart of M to an open subset s yields a chart in the maximal atlas of s.

                                                  NB. We cannot deduce membership in atlas H s in general: by definition, this atlas contains precisely the restriction of each preferred chart at x ∈ s --- whereas atlas H M can contain more charts than these.

                                                  Structomorphisms #

                                                  structure Structomorph {H : Type u} [TopologicalSpace H] (G : StructureGroupoid H) (M : Type u_5) (M' : Type u_6) [TopologicalSpace M] [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H M'] extends Homeomorph :
                                                  Type (max u_5 u_6)

                                                  A G-diffeomorphism between two charted spaces is a homeomorphism which, when read in the charts, belongs to G. We avoid the word diffeomorph as it is too related to the smooth category, and use structomorph instead.

                                                  Instances For
                                                    theorem Structomorph.mem_groupoid {H : Type u} [TopologicalSpace H] {G : StructureGroupoid H} {M : Type u_5} {M' : Type u_6} [TopologicalSpace M] [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H M'] (self : Structomorph G M M') (c : PartialHomeomorph M H) (c' : PartialHomeomorph M' H) :
                                                    c atlas H Mc' atlas H M'c.symm.trans (self.toPartialHomeomorph.trans c') G

                                                    The identity is a diffeomorphism of any charted space, for any groupoid.

                                                    Equations
                                                    Instances For
                                                      def Structomorph.symm {H : Type u} {M : Type u_2} {M' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] {G : StructureGroupoid H} [ChartedSpace H M'] (e : Structomorph G M M') :

                                                      The inverse of a structomorphism is a structomorphism.

                                                      Equations
                                                      • e.symm = { toHomeomorph := e.symm, mem_groupoid := }
                                                      Instances For
                                                        def Structomorph.trans {H : Type u} {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace M'] [TopologicalSpace M''] {G : StructureGroupoid H} [ChartedSpace H M'] [ChartedSpace H M''] (e : Structomorph G M M') (e' : Structomorph G M' M'') :
                                                        Structomorph G M M''

                                                        The composition of structomorphisms is a structomorphism.

                                                        Equations
                                                        • e.trans e' = { toHomeomorph := e.trans e'.toHomeomorph, mem_groupoid := }
                                                        Instances For
                                                          theorem StructureGroupoid.restriction_mem_maximalAtlas_subtype {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {e : PartialHomeomorph M H} (he : e atlas H M) (hs : Nonempty e.source) [HasGroupoid M G] [ClosedUnderRestriction G] :
                                                          let s := { carrier := e.source, is_open' := }; let t := { carrier := e.target, is_open' := }; c'atlas H t, e.toHomeomorphSourceTarget.toPartialHomeomorph.trans c' StructureGroupoid.maximalAtlas (↥s) G

                                                          Restricting a chart to its source s ⊆ M yields a chart in the maximal atlas of s.

                                                          def PartialHomeomorph.toStructomorph {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {e : PartialHomeomorph M H} (he : e atlas H M) [HasGroupoid M G] [ClosedUnderRestriction G] :
                                                          let s := { carrier := e.source, is_open' := }; let t := { carrier := e.target, is_open' := }; Structomorph G s t

                                                          Each chart of a charted space is a structomorphism between its source and target.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For