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:

• the set of charts, which is data
• the fact that changes of charts belong to some group (in fact groupoid), which is additional Prop.

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

• StructureGroupoid H : a subset of partial homeomorphisms of H stable under composition, inverse and restriction (ex: partial diffeomorphisms).
• continuousGroupoid H : the groupoid of all partial homeomorphisms of H.
• ChartedSpace H M : charted space structure on M modelled on H, given by an atlas of partial homeomorphisms from M to H whose sources cover M. This is a type class.
• HasGroupoid M G : when G is a structure groupoid on H and M is a charted space modelled on H, require that all coordinate changes belong to G. This is a type class.
• atlas H M : when M is a charted space modelled on H, the atlas of this charted space structure, i.e., the set of charts.
• G.maximalAtlas M : when M is a charted space modelled on H and admitting G as a structure groupoid, one can consider all the partial homeomorphisms from M to H such that changing coordinate from any chart to them belongs to G. This is a larger atlas, called the maximal atlas (for the groupoid G).
• Structomorph G M M' : the type of diffeomorphisms between the charted spaces M and M' for the groupoid G. We avoid the word diffeomorphism, keeping it for the smooth category.

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:

• Pregroupoid H : a subset of partial maps of H stable under composition and restriction, but not inverse (ex: smooth maps)
• Pregroupoid.groupoid : construct a groupoid from a pregroupoid, by requiring that a map and its inverse both belong to the pregroupoid (ex: construct diffeos from smooth maps)
• chartAt H x is a preferred chart at x : M when M has a charted space structure modelled on H.
• G.compatible he he' states that, for any two charts e and e' in the atlas, the composition of e.symm and e' belongs to the groupoid G when M admits G as a structure groupoid.
• G.compatible_of_mem_maximalAtlas he he' states that, for any two charts e and e' in the maximal atlas associated to the groupoid G, the composition of e.symm and e' belongs to the G if M admits G as a structure groupoid.
• ChartedSpaceCore.toChartedSpace: consider a space without a topology, but endowed with a set of charts (which are partial equivs) for which the change of coordinates are partial homeos. Then one can construct a topology on the space for which the charts become partial homeos, defining a genuine charted space structure.

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 ≫.

def Manifold.«term_≫ₕ_» : Lean.TrailingParserDescr

Equations

• Manifold.«term_≫ₕ_» = Lean.ParserDescr.trailingNode `Manifold.term_≫ₕ_ 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≫ₕ ") (Lean.ParserDescr.cat `term 100))

def Manifold.«term_≫_» : Lean.TrailingParserDescr

Equations

• Manifold.«term_≫_» = Lean.ParserDescr.trailingNode `Manifold.term_≫_ 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≫ ") (Lean.ParserDescr.cat `term 100))

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] : Type u

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)
• trans' : ∀ (e e' : PartialHomeomorph H H), e ∈ self.members → e' ∈ self.members → PartialHomeomorph.trans e e' ∈ self.members
• symm' : ∀ e ∈ self.members, PartialHomeomorph.symm e ∈ self.members
• id_mem' : PartialHomeomorph.refl H ∈ self.members
• locality' : ∀ (e : PartialHomeomorph H H), (∀ x ∈ e.source, ∃ (s : Set H), IsOpen s ∧ x ∈ s ∧ PartialHomeomorph.restr e s ∈ self.members) → e ∈ self.members
• mem_of_eqOnSource' : ∀ (e e' : PartialHomeomorph H H), e ∈ self.members → e' ≈ e → e' ∈ self.members

instance instMembershipPartialHomeomorphStructureGroupoid {H : Type u} [TopologicalSpace H] : Membership (PartialHomeomorph H H) (StructureGroupoid H)

Equations

• instMembershipPartialHomeomorphStructureGroupoid = { mem := fun (e : PartialHomeomorph H H) (G : StructureGroupoid H) => e ∈ G.members }

instance instSetLikeStructureGroupoidPartialHomeomorph (H : Type u) [TopologicalSpace H] : SetLike (StructureGroupoid H) (PartialHomeomorph H H)

Equations

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

instance instInfStructureGroupoid {H : Type u} [TopologicalSpace H] : Inf (StructureGroupoid H)

Equations

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

instance instInfSetStructureGroupoid {H : Type u} [TopologicalSpace H] : InfSet (StructureGroupoid H)

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) : PartialHomeomorph.trans e e' ∈ G

theorem StructureGroupoid.symm {H : Type u} [TopologicalSpace H] (G : StructureGroupoid H) {e : PartialHomeomorph H H} (he : e ∈ G) : PartialHomeomorph.symm e ∈ G

theorem StructureGroupoid.id_mem {H : Type u} [TopologicalSpace H] (G : StructureGroupoid H) : PartialHomeomorph.refl H ∈ G

theorem StructureGroupoid.locality {H : Type u} [TopologicalSpace H] (G : StructureGroupoid H) {e : PartialHomeomorph H H} (h : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen s ∧ x ∈ s ∧ PartialHomeomorph.restr e 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

instance StructureGroupoid.partialOrder {H : Type u} [TopologicalSpace H] : PartialOrder (StructureGroupoid H)

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

Equations

• StructureGroupoid.partialOrder = PartialOrder.lift StructureGroupoid.members (_ : ∀ (a b : StructureGroupoid H), a.members = b.members → a = b)

theorem StructureGroupoid.le_iff {H : Type u} [TopologicalSpace H] {G₁ : StructureGroupoid H} {G₂ : StructureGroupoid H} : G₁ ≤ G₂ ↔ ∀ e ∈ G₁, e ∈ G₂

def idGroupoid (H : Type u) [TopologicalSpace H] : StructureGroupoid H

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

Equations

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

instance instStructureGroupoidOrderBot {H : Type u} [TopologicalSpace H] : OrderBot (StructureGroupoid H)

Every structure groupoid contains the identity groupoid.

Equations

• instStructureGroupoidOrderBot = OrderBot.mk (_ : ∀ (u : StructureGroupoid H) ⦃f : PartialHomeomorph H H⦄, f ∈ ⊥.members → f ∈ u.members)

instance instInhabitedStructureGroupoid {H : Type u} [TopologicalSpace H] : Inhabited (StructureGroupoid H)

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 : (H → H) → Set H → Prop
• comp : ∀ {f g : H → H} {u v : Set H}, self.property f u → self.property g v → IsOpen u → IsOpen v → IsOpen (u ∩ f ⁻¹' v) → self.property (g ∘ f) (u ∩ f ⁻¹' v)
• id_mem : self.property id Set.univ
• locality : ∀ {f : H → H} {u : Set H}, IsOpen u → (∀ x ∈ u, ∃ (v : Set H), IsOpen v ∧ x ∈ v ∧ self.property f (u ∩ v)) → self.property f u
• congr : ∀ {f g : H → H} {u : Set H}, IsOpen u → (∀ x ∈ u, g x = f x) → self.property f u → self.property g u

def Pregroupoid.groupoid {H : Type u} [TopologicalSpace H] (PG : Pregroupoid H) : StructureGroupoid H

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.

theorem mem_groupoid_of_pregroupoid {H : Type u} [TopologicalSpace H] {PG : Pregroupoid H} {e : PartialHomeomorph H H} : e ∈ Pregroupoid.groupoid PG ↔ PG.property (↑e) e.source ∧ PG.property (↑(PartialHomeomorph.symm e)) e.target

theorem groupoid_of_pregroupoid_le {H : Type u} [TopologicalSpace H] (PG₁ : Pregroupoid H) (PG₂ : Pregroupoid H) (h : ∀ (f : H → H) (s : Set H), PG₁.property f s → PG₂.property f s) : Pregroupoid.groupoid PG₁ ≤ Pregroupoid.groupoid PG₂

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]

def continuousPregroupoid (H : Type u_5) [TopologicalSpace H] : Pregroupoid H

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

Equations

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

instance instInhabitedPregroupoid (H : Type u_5) [TopologicalSpace H] : Inhabited (Pregroupoid H)

Equations

• instInhabitedPregroupoid H = { default := continuousPregroupoid H }

def continuousGroupoid (H : Type u_5) [TopologicalSpace H] : StructureGroupoid H

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

Equations

• continuousGroupoid H = Pregroupoid.groupoid (continuousPregroupoid H)

instance instStructureGroupoidOrderTop {H : Type u} [TopologicalSpace H] : OrderTop (StructureGroupoid H)

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

Equations

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

instance instCompleteLatticeStructureGroupoid {H : Type u} [TopologicalSpace H] : CompleteLattice (StructureGroupoid H)

Equations

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

class ClosedUnderRestriction {H : Type u} [TopologicalSpace H] (G : StructureGroupoid H) : Prop

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

• closedUnderRestriction : ∀ {e : PartialHomeomorph H H}, e ∈ G → ∀ (s : Set H), IsOpen s → PartialHomeomorph.restr e 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) : PartialHomeomorph.restr e s ∈ G

def idRestrGroupoid {H : Type u} [TopologicalSpace H] : StructureGroupoid H

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.

theorem idRestrGroupoid_mem {H : Type u} [TopologicalSpace H] {s : Set H} (hs : IsOpen s) : PartialHomeomorph.ofSet s hs ∈ idRestrGroupoid

instance closedUnderRestriction_idRestrGroupoid {H : Type u} [TopologicalSpace H] : ClosedUnderRestriction idRestrGroupoid

The trivial restriction-closed groupoid is indeed ClosedUnderRestriction.

Equations

• (_ : ClosedUnderRestriction idRestrGroupoid) = (_ : ClosedUnderRestriction idRestrGroupoid)

theorem closedUnderRestriction_iff_id_le {H : Type u} [TopologicalSpace H] (G : StructureGroupoid H) : ClosedUnderRestriction G ↔ idRestrGroupoid ≤ G

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

instance instClosedUnderRestrictionContinuousGroupoid {H : Type u} [TopologicalSpace H] : ClosedUnderRestriction (continuousGroupoid H)

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

Equations

• (_ : ClosedUnderRestriction (continuousGroupoid H)) = (_ : ClosedUnderRestriction (continuousGroupoid H))

Charted spaces

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.atlas → ChartedSpace.chartAt = ChartedSpace.chartAt → x = y

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

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).

• atlas : Set (PartialHomeomorph M H)

  The atlas of charts in the ChartedSpace.

• chartAt : M → PartialHomeomorph M H

  The preferred chart at each point in the charted space.

• mem_chart_source : ∀ (x : M), x ∈ (ChartedSpace.chartAt x).source
• chart_mem_atlas : ∀ (x : M), ChartedSpace.chartAt x ∈ ChartedSpace.atlas

@[inline, reducible]

abbrev atlas (H : Type u_5) [TopologicalSpace H] (M : Type u_6) [TopologicalSpace M] [ChartedSpace H M] : Set (PartialHomeomorph M H)

The atlas of charts in a ChartedSpace.

Equations

• atlas H M = ChartedSpace.atlas

@[inline, reducible]

abbrev chartAt (H : Type u_5) [TopologicalSpace H] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] (x : M) : PartialHomeomorph M H

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

Equations

• chartAt H x = ChartedSpace.chartAt x

@[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).toPartialEquiv.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

instance chartedSpaceSelf (H : Type u_5) [TopologicalSpace H] : ChartedSpace H H

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

Equations

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

@[simp]

theorem chartedSpaceSelf_atlas {H : Type u_5} [TopologicalSpace H] {e : PartialHomeomorph H H} : e ∈ atlas H H ↔ e = PartialHomeomorph.refl H

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

theorem chartAt_self_eq {H : Type u_5} [TopologicalSpace H] {x : H} : chartAt H x = PartialHomeomorph.refl H

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).toPartialEquiv.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).toPartialEquiv.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).toPartialEquiv.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).toPartialEquiv.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).toPartialEquiv.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

• achart H x = { val := chartAt H x, property := (_ : chartAt H x ∈ atlas H M) }

theorem achart_def (H : Type u) {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) : achart H x = { val := chartAt H x, property := (_ : chartAt H x ∈ atlas H M) }

@[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 : ⋃ x ∈ s, (chartAt H x).toPartialEquiv.source = Set.univ) (hsc : Set.Countable s) : SecondCountableTopology M

theorem ChartedSpace.secondCountable_of_sigma_compact (H : Type u) (M : Type u_2) [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [SecondCountableTopology H] [SigmaCompactSpace M] : SecondCountableTopology M

theorem ChartedSpace.locallyCompactSpace (H : Type u) (M : Type u_2) [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [LocallyCompactSpace H] : LocallyCompactSpace M

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

theorem ChartedSpace.locallyConnectedSpace (H : Type u) (M : Type u_2) [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [LocallyConnectedSpace H] : LocallyConnectedSpace M

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] : 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.

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 = PartialHomeomorph.trans (chartAt H' x) (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

• ModelProd H H' = (H × H')

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

• ModelPi H = ((i : ι) → H i)

instance modelProdInhabited {H : Type u} {H' : Type u_1} [Inhabited H] [Inhabited H'] : Inhabited (ModelProd H H')

Equations

• modelProdInhabited = instInhabitedProd

instance instTopologicalSpaceModelProd (H : Type u_5) [TopologicalSpace H] (H' : Type u_6) [TopologicalSpace H'] : TopologicalSpace (ModelProd H H')

Equations

• instTopologicalSpaceModelProd H H' = instTopologicalSpaceProd

@[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)] : Inhabited (ModelPi Hi)

Equations

• modelPiInhabited = { default := fun (x : ι) => default }

instance instTopologicalSpaceModelPi {ι : Type u_5} {Hi : ι → Type u_6} [(i : ι) → TopologicalSpace (Hi i)] : TopologicalSpace (ModelPi Hi)

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 {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 = PartialHomeomorph.prod (chartAt H x.1) (chartAt H' x.2)

theorem chartedSpaceSelf_prod {H : Type u} {H' : Type u_1} [TopologicalSpace H] [TopologicalSpace H'] : prodChartedSpace H H H' H' = chartedSpaceSelf (H × H')

instance piChartedSpace {ι : Type u_5} [Fintype ι] (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} [Fintype ι] (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 equivs, and continuity properties for their composition. This is formalised in ChartedSpaceCore.

• atlas : Set (PartialEquiv M H)
• chartAt : M → PartialEquiv M H
• 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.atlas → e' ∈ self.atlas → IsOpen (PartialEquiv.trans (PartialEquiv.symm e) e').source
• continuousOn_toFun : ∀ (e e' : PartialEquiv M H), e ∈ self.atlas → e' ∈ self.atlas → ContinuousOn (↑(PartialEquiv.trans (PartialEquiv.symm e) e')) (PartialEquiv.trans (PartialEquiv.symm e) e').source

def ChartedSpaceCore.toTopologicalSpace {H : Type u} {M : Type u_2} [TopologicalSpace H] (c : ChartedSpaceCore H M) : TopologicalSpace M

Topology generated by a set of charts on a Type.

Equations

• ChartedSpaceCore.toTopologicalSpace c = TopologicalSpace.generateFrom (⋃ e ∈ c.atlas, ⋃ (s : Set H), ⋃ (_ : IsOpen s), {↑e ⁻¹' s ∩ e.source})

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) : PartialHomeomorph M H

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

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

def ChartedSpaceCore.toChartedSpace {H : Type u} {M : Type u_2} [TopologicalSpace H] (c : ChartedSpaceCore H M) : ChartedSpace H M

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.

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) : Prop

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

• compatible : ∀ {e e' : PartialHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → PartialHomeomorph.trans (PartialHomeomorph.symm e) 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) : PartialHomeomorph.trans (PartialHomeomorph.symm e) 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₂) : HasGroupoid M 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 M → e' ∈ atlas H M → PG.property (↑(PartialHomeomorph.trans (PartialHomeomorph.symm e) e')) (PartialHomeomorph.trans (PartialHomeomorph.symm e) e').toPartialEquiv.source) : HasGroupoid M (Pregroupoid.groupoid PG)

instance hasGroupoid_model_space (H : Type u_5) [TopologicalSpace H] (G : StructureGroupoid H) : HasGroupoid H G

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

Equations

• (_ : HasGroupoid H G) = (_ : HasGroupoid H G)

instance hasGroupoid_continuousGroupoid {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] : HasGroupoid M (continuousGroupoid H)

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

Equations

• (_ : HasGroupoid M (continuousGroupoid H)) = (_ : HasGroupoid M (continuousGroupoid H))

def StructureGroupoid.maximalAtlas {H : Type u} (M : Type u_2) [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (G : StructureGroupoid H) : Set (PartialHomeomorph M H)

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

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

theorem StructureGroupoid.subset_maximalAtlas {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (G : StructureGroupoid H) [HasGroupoid M G] : atlas H M ⊆ StructureGroupoid.maximalAtlas M G

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

theorem StructureGroupoid.chart_mem_maximalAtlas {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (G : StructureGroupoid H) [HasGroupoid M G] (x : M) : chartAt H x ∈ StructureGroupoid.maximalAtlas M G

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, PartialHomeomorph.trans (PartialHomeomorph.symm e) e' ∈ G ∧ PartialHomeomorph.trans (PartialHomeomorph.symm e') e ∈ G

theorem StructureGroupoid.compatible_of_mem_maximalAtlas {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {e : PartialHomeomorph M H} {e' : PartialHomeomorph M H} (he : e ∈ StructureGroupoid.maximalAtlas M G) (he' : e' ∈ StructureGroupoid.maximalAtlas M G) : PartialHomeomorph.trans (PartialHomeomorph.symm e) e' ∈ G

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

theorem StructureGroupoid.id_mem_maximalAtlas {H : Type u} [TopologicalSpace H] (G : StructureGroupoid H) : PartialHomeomorph.refl H ∈ StructureGroupoid.maximalAtlas H G

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

theorem StructureGroupoid.mem_maximalAtlas_of_mem_groupoid {H : Type u} [TopologicalSpace H] (G : StructureGroupoid H) {f : PartialHomeomorph H H} (hf : f ∈ G) : f ∈ StructureGroupoid.maximalAtlas H G

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) : ChartedSpace H α

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

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

@[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).toPartialEquiv.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] : HasGroupoid α 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) : ChartedSpace H α

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

Equations

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

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

theorem OpenEmbedding.singleton_hasGroupoid {H : Type u} [TopologicalSpace H] {α : Type u_5} [TopologicalSpace α] [Nonempty α] {f : α → H} (h : OpenEmbedding f) (G : StructureGroupoid H) [ClosedUnderRestriction G] : HasGroupoid α G

instance TopologicalSpace.Opens.instChartedSpace {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (s : TopologicalSpace.Opens M) : ChartedSpace H ↥s

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

Equations

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

instance TopologicalSpace.Opens.instHasGroupoid {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (G : StructureGroupoid H) [HasGroupoid M G] (s : TopologicalSpace.Opens M) [ClosedUnderRestriction G] : HasGroupoid (↥s) G

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

Equations

• (_ : HasGroupoid (↥s) G) = (_ : HasGroupoid (↥s) G)

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} : ↑(PartialHomeomorph.symm (chartAt H ↑x)) =ᶠ[nhds (↑(chartAt H ↑x) ↑x)] Subtype.val ∘ ↑(PartialHomeomorph.symm (chartAt H x))

theorem TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {U : TopologicalSpace.Opens M} {V : TopologicalSpace.Opens M} (hUV : U ≤ V) {x : ↥U} : ↑(PartialHomeomorph.symm (chartAt H (Set.inclusion hUV x))) =ᶠ[nhds (↑(chartAt H (Set.inclusion hUV x)) (Set.inclusion hUV x))] Set.inclusion hUV ∘ ↑(PartialHomeomorph.symm (chartAt H x))

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.

• toFun : M → M'
• invFun : M' → M
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• continuous_toFun : Continuous self.toFun
• continuous_invFun : Continuous self.invFun
• mem_groupoid : ∀ (c : PartialHomeomorph M H) (c' : PartialHomeomorph M' H), c ∈ atlas H M → c' ∈ atlas H M' → PartialHomeomorph.trans (PartialHomeomorph.symm c) (PartialHomeomorph.trans (Homeomorph.toPartialHomeomorph self.toHomeomorph) c') ∈ G

def Structomorph.refl {H : Type u} [TopologicalSpace H] {G : StructureGroupoid H} (M : Type u_5) [TopologicalSpace M] [ChartedSpace H M] [HasGroupoid M G] : Structomorph G M M

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

Equations

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

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') : Structomorph G M' M

The inverse of a structomorphism is a structomorphism.

Equations

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

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

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