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 open partial homeomorphisms stable under composition and inverse, to which the change of coordinates should belong.

Main definitions

• StructureGroupoid H : a subset of open partial homeomorphisms of H stable under composition, inverse and restriction (ex: partial diffeomorphisms).
• continuousGroupoid H : the groupoid of all open partial homeomorphisms of H.
• ChartedSpace H M : charted space structure on M modelled on H, given by an atlas of open 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 open 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 changes 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).

Notation

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

Charted spaces

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 values 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 (OpenPartialHomeomorph M H)

  The atlas of charts in the ChartedSpace.

• chartAt : M → OpenPartialHomeomorph 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

theorem ChartedSpace.ext {H : Type u_5} {inst✝ : TopologicalSpace H} {M : Type u_6} {inst✝¹ : TopologicalSpace M} {x y : ChartedSpace H M} (atlas : ChartedSpace.atlas = ChartedSpace.atlas) (chartAt : ChartedSpace.chartAt = ChartedSpace.chartAt) : x = y

theorem ChartedSpace.ext_iff {H : Type u_5} {inst✝ : TopologicalSpace H} {M : Type u_6} {inst✝¹ : TopologicalSpace M} {x y : ChartedSpace H M} : x = y ↔ ChartedSpace.atlas = ChartedSpace.atlas ∧ ChartedSpace.chartAt = ChartedSpace.chartAt

@[reducible, inline]

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

The atlas of charts in a ChartedSpace.

Equations

• atlas H M = ChartedSpace.atlas

@[reducible, inline]

abbrev chartAt (H : Type u_5) [TopologicalSpace H] {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] (x : M) : OpenPartialHomeomorph 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).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

theorem nonempty_of_chartedSpace {H : Type u_5} {M : Type u_6} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) : Nonempty H

theorem isEmpty_of_chartedSpace (H : Type u_5) {M : Type u_6} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [IsEmpty H] : IsEmpty M

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

Equations

• achart H x = ⟨chartAt H x, ⋯⟩

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

theorem ChartedSpace.secondCountable_of_sigmaCompact (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.

theorem ChartedSpace.locPathConnectedSpace (H : Type u) (M : Type u_2) [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [LocPathConnectedSpace H] : LocPathConnectedSpace M

If a topological space M admits an atlas with locally path-connected charts, then M itself is locally path-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 = (chartAt H' x).trans (chartAt H (↑(chartAt H' x) x))

theorem ChartedSpace.t1Space (H : Type u) (M : Type u_2) [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [T1Space H] : T1Space M

A charted space over a T1 space is T1. Note that this is not true for T2 (for instance for the real line with a double origin).

theorem ChartedSpace.discreteTopology (H : Type u) (M : Type u_2) [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [DiscreteTopology H] : DiscreteTopology M

A charted space over a discrete space is discrete.

def ChartedSpace.empty (H : Type u_5) [TopologicalSpace H] (M : Type u_6) [TopologicalSpace M] [IsEmpty M] : ChartedSpace 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 := ⋯ }

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

• chartedSpaceSelf H = { atlas := {OpenPartialHomeomorph.refl H}, chartAt := fun (x : H) => OpenPartialHomeomorph.refl H, mem_chart_source := ⋯, chart_mem_atlas := ⋯ }

@[simp]

theorem chartedSpaceSelf_atlas {H : Type u_5} [TopologicalSpace H] {e : OpenPartialHomeomorph H H} : e ∈ atlas H H ↔ e = OpenPartialHomeomorph.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 = OpenPartialHomeomorph.refl H

In the model space, chartAt is always the identity.

def ChartedSpace.of_discreteTopology {H : Type u} {M : Type u_2} [TopologicalSpace M] [TopologicalSpace H] [DiscreteTopology M] [h : Unique H] : ChartedSpace H M

Any discrete space is a charted space over a singleton set. We keep this as a definition (not an instance) to avoid instance search trying to search for DiscreteTopology or Unique instances.

Equations

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

@[simp]

theorem chartedSpace_of_discreteTopology_chartAt {H : Type u} {M : Type u_2} [TopologicalSpace M] [TopologicalSpace H] [DiscreteTopology M] [h : Unique H] {x : M} : chartAt H x = OpenPartialHomeomorph.const ⋯ ⋯

A chart on the discrete space is the constant chart.

def LibraryNote.Manifold_type_tags : Batteries.Util.LibraryNote

For technical reasons we introduce two type tags:

• ModelProd H H' is the same as H × H';
• ModelPi H is the same as ∀ i, H i, where H : ι → Type* and ι is a finite type.

In both cases the reason is the same, so we explain it only in the case of the product. A charted space M with model H is a set of charts from M to H covering the space. Every space is registered as a charted space over itself, using the only chart id, in chartedSpaceSelf. You can also define a product of charted space M and M' (with model space H × H') by taking the products of the charts. Now, on H × H', there are two charted space structures with model space H × H' itself, the one coming from chartedSpaceSelf, and the one coming from the product of the two chartedSpaceSelf on each component. They are equal, but not defeq (because the product of id and id is not defeq to id), which is bad as we know. This expedient of renaming H × H' solves this problem.

Equations

• LibraryNote.Manifold_type_tags = default

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 = Pi.instInhabited

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 y : ModelProd H H'} (h₁ : x.1 = y.1) (h₂ : x.2 = y.2) : x = y

theorem ModelProd.ext_iff {H : Type u} {H' : Type u_1} {x y : ModelProd H H'} : x = y ↔ x.1 = y.1 ∧ x.2 = y.2

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

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} [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 = OpenPartialHomeomorph.pi fun (i : ι) => chartAt (H i) (f i)

def ChartedSpace.sum_of_nonempty {H : Type u} {M : Type u_2} {M' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [TopologicalSpace M'] [cm : ChartedSpace H M] [cm' : ChartedSpace H M'] [Nonempty H] : ChartedSpace H (M ⊕ M')

The disjoint union of two charted spaces modelled on a non-empty space H is a charted space over H.

Equations

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

instance ChartedSpace.sum {H : Type u} {M : Type u_2} {M' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [TopologicalSpace M'] [cm : ChartedSpace H M] [cm' : ChartedSpace H M'] : ChartedSpace H (M ⊕ M')

Equations

• ChartedSpace.sum = if h : Nonempty H then ChartedSpace.sum_of_nonempty else have this := ⋯; have this_1 := ⋯; ChartedSpace.empty H (M ⊕ M')

theorem ChartedSpace.sum_chartAt_inl {H : Type u} {M : Type u_2} {M' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [TopologicalSpace M'] [cm : ChartedSpace H M] [cm' : ChartedSpace H M'] (x : M) : chartAt H (Sum.inl x) = (chartAt H x).lift_openEmbedding ⋯

theorem ChartedSpace.sum_chartAt_inr {H : Type u} {M : Type u_2} {M' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [TopologicalSpace M'] [cm : ChartedSpace H M] [cm' : ChartedSpace H M'] (x' : M') : chartAt H (Sum.inr x') = (chartAt H x').lift_openEmbedding ⋯

@[simp]

theorem sum_chartAt_inl_apply {H : Type u} {M : Type u_2} {M' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [TopologicalSpace M'] [cm : ChartedSpace H M] [cm' : ChartedSpace H M'] {x y : M} : ↑(chartAt H (Sum.inl x)) (Sum.inl y) = ↑(chartAt H x) y

@[simp]

theorem sum_chartAt_inr_apply {H : Type u} {M : Type u_2} {M' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [TopologicalSpace M'] [cm : ChartedSpace H M] [cm' : ChartedSpace H M'] {x y : M'} : ↑(chartAt H (Sum.inr x)) (Sum.inr y) = ↑(chartAt H x) y

theorem ChartedSpace.mem_atlas_sum {H : Type u} {M : Type u_2} {M' : Type u_3} [TopologicalSpace H] [TopologicalSpace M] [TopologicalSpace M'] [cm : ChartedSpace H M] [cm' : ChartedSpace H M'] [h : Nonempty H] {e : OpenPartialHomeomorph (M ⊕ M') H} (he : e ∈ atlas H (M ⊕ M')) : (∃ f ∈ atlas H M, e = f.lift_openEmbedding ⋯) ∨ ∃ f' ∈ atlas H M', e = f'.lift_openEmbedding ⋯

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

• c.toTopologicalSpace = 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.openPartialHomeomorph {H : Type u} {M : Type u_2} [TopologicalSpace H] (c : ChartedSpaceCore H M) (e : PartialEquiv M H) (he : e ∈ c.atlas) : OpenPartialHomeomorph M H

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

Equations

• c.openPartialHomeomorph e he = { toPartialEquiv := e, open_source := ⋯, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }

@[deprecated ChartedSpaceCore.openPartialHomeomorph (since := "2025-08-29")]

def ChartedSpaceCore.partialHomeomorph {H : Type u} {M : Type u_2} [TopologicalSpace H] (c : ChartedSpaceCore H M) (e : PartialEquiv M H) (he : e ∈ c.atlas) : OpenPartialHomeomorph M H

Alias of ChartedSpaceCore.openPartialHomeomorph.

---

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

Equations

• @ChartedSpaceCore.partialHomeomorph = @ChartedSpaceCore.openPartialHomeomorph

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.