mathlib3 documentation

geometry.manifold.charted_space

Charted spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 local 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 charted_space_model_space (H : Type*) [topological_space H] : charted_space 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 charted_space_core making it possible to construct a topology out of a set of local 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 local homeomorphisms with ≫ₕ, and the composition of local 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 closed_under_restriction for groupoids which have the restriction property.

The only nontrivial requirement is locality: if a local 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 local 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 local 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 has_mem instance, writing e ∈ G instead of e ∈ G.members.

source
structure structure_groupoid (H : Type u) [topological_space H] :
Type u

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

Instances for structure_groupoid
source
@[protected, instance]
def structure_groupoid.has_mem {H : Type u} [topological_space H] :
has_mem (local_homeomorph H H) (structure_groupoid H)
Equations
source
theorem structure_groupoid.trans {H : Type u} [topological_space H] (G : structure_groupoid H) {e e' : local_homeomorph H H} (he : e ∈ G) (he' : e' ∈ G) :
e.trans e' ∈ G
source
theorem structure_groupoid.symm {H : Type u} [topological_space H] (G : structure_groupoid H) {e : local_homeomorph H H} (he : e ∈ G) :
e.symm ∈ G
source
theorem structure_groupoid.id_mem {H : Type u} [topological_space H] (G : structure_groupoid H) :
local_homeomorph.refl H ∈ G
source
theorem structure_groupoid.locality {H : Type u} [topological_space H] (G : structure_groupoid H) {e : local_homeomorph H H} (h : ∀ (x : H), x ∈ e.to_local_equiv.source → (∃ (s : set H), is_open s ∧ x ∈ s ∧ e.restr s ∈ G)) :
e ∈ G
source
theorem structure_groupoid.eq_on_source {H : Type u} [topological_space H] (G : structure_groupoid H) {e e' : local_homeomorph H H} (he : e ∈ G) (h : e' ≈ e) :
e' ∈ G
source
@[protected, instance]
def structure_groupoid.partial_order {H : Type u} [topological_space H] :
partial_order (structure_groupoid H)

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

Equations
source
theorem structure_groupoid.le_iff {H : Type u} [topological_space H] {G₁ G₂ : structure_groupoid H} :
G₁ ≤ G₂ ↔ ∀ (e : local_homeomorph H H), e ∈ G₁ → e ∈ G₂
source
def id_groupoid (H : Type u) [topological_space H] :
structure_groupoid H

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

Equations
source
@[protected, instance]
def structure_groupoid.order_bot {H : Type u} [topological_space H] :
order_bot (structure_groupoid H)

Every structure groupoid contains the identity groupoid

Equations
source
@[protected, instance]
def structure_groupoid.inhabited (H : Type u) [topological_space H] :
inhabited (structure_groupoid H)
Equations
source
structure pregroupoid (H : Type u_5) [topological_space H] :
Type u_5

To construct a groupoid, one may consider classes of local homeos 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.

Instances for pregroupoid
source
def pregroupoid.groupoid {H : Type u} [topological_space H] (PG : pregroupoid H) :
structure_groupoid H

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

Equations
source
theorem mem_groupoid_of_pregroupoid {H : Type u} [topological_space H] {PG : pregroupoid H} {e : local_homeomorph H H} :
e ∈ PG.groupoid ↔ PG.property ⇑e e.to_local_equiv.source ∧ PG.property ⇑(e.symm) e.to_local_equiv.target
source
theorem groupoid_of_pregroupoid_le {H : Type u} [topological_space H] (PG₁ PG₂ : pregroupoid H) (h : ∀ (f : H → H) (s : set H), PG₁.property f s → PG₂.property f s) :
PG₁.groupoid ≤ PG₂.groupoid
source
theorem mem_pregroupoid_of_eq_on_source {H : Type u} [topological_space H] (PG : pregroupoid H) {e e' : local_homeomorph H H} (he' : e ≈ e') (he : PG.property ⇑e e.to_local_equiv.source) :
PG.property ⇑e' e'.to_local_equiv.source
source
@[reducible]
def continuous_pregroupoid (H : Type u_1) [topological_space H] :
pregroupoid H

The pregroupoid of all local maps on a topological space H

Equations
source
@[protected, instance]
def pregroupoid.inhabited (H : Type u_1) [topological_space H] :
inhabited (pregroupoid H)
Equations
source
def continuous_groupoid (H : Type u_1) [topological_space H] :
structure_groupoid H

The groupoid of all local homeomorphisms on a topological space H

Equations
Instances for continuous_groupoid
source
@[protected, instance]
def structure_groupoid.order_top {H : Type u} [topological_space H] :
order_top (structure_groupoid H)

Every structure groupoid is contained in the groupoid of all local homeomorphisms

Equations
source
@[class]
structure closed_under_restriction {H : Type u} [topological_space H] (G : structure_groupoid H) :
Prop

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

Instances of this typeclass
source
theorem closed_under_restriction' {H : Type u} [topological_space H] {G : structure_groupoid H} [closed_under_restriction G] {e : local_homeomorph H H} (he : e ∈ G) {s : set H} (hs : is_open s) :
e.restr s ∈ G
source
def id_restr_groupoid {H : Type u} [topological_space H] :
structure_groupoid H

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

Equations
Instances for id_restr_groupoid
source
theorem id_restr_groupoid_mem {H : Type u} [topological_space H] {s : set H} (hs : is_open s) :
local_homeomorph.of_set s hs ∈ id_restr_groupoid
source
@[protected, instance]
def closed_under_restriction_id_restr_groupoid {H : Type u} [topological_space H] :
closed_under_restriction id_restr_groupoid

The trivial restriction-closed groupoid is indeed closed_under_restriction.

source
theorem closed_under_restriction_iff_id_le {H : Type u} [topological_space H] (G : structure_groupoid H) :
closed_under_restriction G ↔ id_restr_groupoid ≤ G

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

source
@[protected, instance]
def continuous_groupoid.closed_under_restriction {H : Type u} [topological_space H] :
closed_under_restriction (continuous_groupoid H)

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

Charted spaces #

source
theorem charted_space.ext {H : Type u_5} {_inst_1 : topological_space H} {M : Type u_6} {_inst_2 : topological_space M} (x y : charted_space H M) (h : charted_space.atlas H M = charted_space.atlas H M) (h_1 : charted_space.chart_at H = charted_space.chart_at H) :
x = y
source
theorem charted_space.ext_iff {H : Type u_5} {_inst_1 : topological_space H} {M : Type u_6} {_inst_2 : topological_space M} (x y : charted_space H M) :
x = y ↔ charted_space.atlas H M = charted_space.atlas H M ∧ charted_space.chart_at H = charted_space.chart_at H
source
@[ext, class]
structure charted_space (H : Type u_5) [topological_space H] (M : Type u_6) [topological_space 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 chosing for each x a member chart_at H 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 of this typeclass
Instances of other typeclasses for charted_space
  • charted_space.has_sizeof_inst
source
@[protected, instance]
def charted_space_self (H : Type u_1) [topological_space H] :
charted_space H H

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

Equations
source
@[simp]
theorem charted_space_self_atlas {H : Type u_1} [topological_space H] {e : local_homeomorph H H} :
e ∈ charted_space.atlas H H ↔ e = local_homeomorph.refl H

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

source
theorem chart_at_self_eq {H : Type u_1} [topological_space H] {x : H} :
charted_space.chart_at H x = local_homeomorph.refl H

In the model space, chart_at is always the identity

source
theorem mem_chart_target (H : Type u) {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] (x : M) :
⇑(charted_space.chart_at H x) x ∈ (charted_space.chart_at H x).to_local_equiv.target
source
theorem chart_source_mem_nhds (H : Type u) {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] (x : M) :
(charted_space.chart_at H x).to_local_equiv.source ∈ nhds x
source
theorem chart_target_mem_nhds (H : Type u) {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] (x : M) :
(charted_space.chart_at H x).to_local_equiv.target ∈ nhds (⇑(charted_space.chart_at H x) x)
source
def achart (H : Type u) {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] (x : M) :
↥(charted_space.atlas H M)

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

Equations
source
theorem achart_def (H : Type u) {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] (x : M) :
achart H x = ⟨charted_space.chart_at H x, _⟩
source
@[simp]
theorem coe_achart (H : Type u) {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] (x : M) :
↑(achart H x) = charted_space.chart_at H x
source
@[simp]
theorem achart_val (H : Type u) {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] (x : M) :
(achart H x).val = charted_space.chart_at H x
source
theorem mem_achart_source (H : Type u) {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] (x : M) :
x ∈ (achart H x).val.to_local_equiv.source
source
theorem charted_space.second_countable_of_countable_cover (H : Type u) {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] [topological_space.second_countable_topology H] {s : set M} (hs : (⋃ (x : M) (hx : x ∈ s), (charted_space.chart_at H x).to_local_equiv.source) = set.univ) (hsc : s.countable) :
topological_space.second_countable_topology M
source
theorem charted_space.second_countable_of_sigma_compact (H : Type u) (M : Type u_2) [topological_space H] [topological_space M] [charted_space H M] [topological_space.second_countable_topology H] [sigma_compact_space M] :
topological_space.second_countable_topology M
source
theorem charted_space.locally_compact (H : Type u) (M : Type u_2) [topological_space H] [topological_space M] [charted_space H M] [locally_compact_space H] :
locally_compact_space M

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

source
theorem charted_space.locally_connected_space (H : Type u) (M : Type u_2) [topological_space H] [topological_space M] [charted_space H M] [locally_connected_space H] :
locally_connected_space M

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

source
def charted_space.comp (H : Type u_1) [topological_space H] (H' : Type u_2) [topological_space H'] (M : Type u_3) [topological_space M] [charted_space H H'] [charted_space H' M] :
charted_space 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
source
def library_note.Manifold type tags  :
unit

For technical reasons we introduce two type tags:

  • model_prod H H' is the same as H × H';
  • model_pi 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 local charts from M to H covering the space. Every space is registered as a charted space over itself, using the only chart id, in manifold_model_space. 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 manifold_model_space, and the one coming from the product of the two manifold_model_space 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.

source
def model_prod (H : Type u_1) (H' : Type u_2) :
Type (max u_1 u_2)

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

Equations
Instances for model_prod
source
def model_pi {ι : Type u_1} (H : ι → Type u_2) :
Type (max u_1 u_2)

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

Equations
Instances for model_pi
source
@[protected, instance]
def model_prod_inhabited {H : Type u} {H' : Type u_1} [inhabited H] [inhabited H'] :
inhabited (model_prod H H')
Equations
source
@[protected, instance]
def model_prod.topological_space (H : Type u_1) [topological_space H] (H' : Type u_2) [topological_space H'] :
topological_space (model_prod H H')
Equations
source
@[simp]
theorem model_prod_range_prod_id {H : Type u_1} {H' : Type u_2} {α : Type u_3} (f : H → α) :
set.range (λ (p : model_prod H H'), (f p.fst, p.snd)) = set.range f ×ˢ set.univ
source
@[protected, instance]
def model_pi_inhabited {ι : Type u_5} {Hi : ι → Type u_6} [Π (i : ι), inhabited (Hi i)] :
inhabited (model_pi Hi)
Equations
source
@[protected, instance]
def model_pi.topological_space {ι : Type u_5} {Hi : ι → Type u_6} [Π (i : ι), topological_space (Hi i)] :
topological_space (model_pi Hi)
Equations
source
@[protected, instance]
def prod_charted_space (H : Type u_1) [topological_space H] (M : Type u_2) [topological_space M] [charted_space H M] (H' : Type u_3) [topological_space H'] (M' : Type u_4) [topological_space M'] [charted_space H' M'] :
charted_space (model_prod 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
source
@[simp]
theorem prod_charted_space_chart_at {H : Type u} {H' : Type u_1} {M : Type u_2} {M' : Type u_3} [topological_space H] [topological_space M] [charted_space H M] [topological_space H'] [topological_space M'] [charted_space H' M'] {x : M × M'} :
charted_space.chart_at (model_prod H H') x = (charted_space.chart_at H x.fst).prod (charted_space.chart_at H' x.snd)
source
theorem charted_space_self_prod {H : Type u} {H' : Type u_1} [topological_space H] [topological_space H'] :
prod_charted_space H H H' H' = charted_space_self (H × H')
source
@[protected, instance]
def pi_charted_space {ι : Type u_1} [fintype ι] (H : ι → Type u_2) [Π (i : ι), topological_space (H i)] (M : ι → Type u_3) [Π (i : ι), topological_space (M i)] [Π (i : ι), charted_space (H i) (M i)] :
charted_space (model_pi 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
source
@[simp]
theorem pi_charted_space_chart_at {ι : Type u_1} [fintype ι] (H : ι → Type u_2) [Π (i : ι), topological_space (H i)] (M : ι → Type u_3) [Π (i : ι), topological_space (M i)] [Π (i : ι), charted_space (H i) (M i)] (f : Π (i : ι), M i) :
charted_space.chart_at (model_pi H) f = local_homeomorph.pi (λ (i : ι), charted_space.chart_at (H i) (f i))

Constructing a topology from an atlas #

source
@[nolint]
structure charted_space_core (H : Type u_5) [topological_space 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 local equivs, and continuity properties for their composition. This is formalised in charted_space_core.

Instances for charted_space_core
  • charted_space_core.has_sizeof_inst
source
@[protected]
def charted_space_core.to_topological_space {H : Type u} {M : Type u_2} [topological_space H] (c : charted_space_core H M) :
topological_space M

Topology generated by a set of charts on a Type.

Equations
source
theorem charted_space_core.open_source' {H : Type u} {M : Type u_2} [topological_space H] (c : charted_space_core H M) {e : local_equiv M H} (he : e ∈ c.atlas) :
is_open e.source
source
theorem charted_space_core.open_target {H : Type u} {M : Type u_2} [topological_space H] (c : charted_space_core H M) {e : local_equiv M H} (he : e ∈ c.atlas) :
is_open e.target
source
@[protected]
def charted_space_core.local_homeomorph {H : Type u} {M : Type u_2} [topological_space H] (c : charted_space_core H M) (e : local_equiv M H) (he : e ∈ c.atlas) :
local_homeomorph M H

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

Equations
source
def charted_space_core.to_charted_space {H : Type u} {M : Type u_2} [topological_space H] (c : charted_space_core H M) :
charted_space 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

Charted space with a given structure groupoid #

source
@[class]
structure has_groupoid {H : Type u_5} [topological_space H] (M : Type u_6) [topological_space M] [charted_space H M] (G : structure_groupoid H) :
Prop

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

Instances of this typeclass
source
theorem structure_groupoid.compatible {H : Type u_1} [topological_space H] (G : structure_groupoid H) {M : Type u_2} [topological_space M] [charted_space H M] [has_groupoid M G] {e e' : local_homeomorph M H} (he : e ∈ charted_space.atlas H M) (he' : e' ∈ charted_space.atlas H M) :
e.symm.trans e' ∈ G

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

source
theorem has_groupoid_of_le {H : Type u} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {G₁ G₂ : structure_groupoid H} (h : has_groupoid M G₁) (hle : G₁ ≤ G₂) :
has_groupoid M G₂
source
theorem has_groupoid_of_pregroupoid {H : Type u} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] (PG : pregroupoid H) (h : ∀ {e e' : local_homeomorph M H}, e ∈ charted_space.atlas H M → e' ∈ charted_space.atlas H M → PG.property ⇑(e.symm.trans e') (e.symm.trans e').to_local_equiv.source) :
has_groupoid M PG.groupoid
source
@[protected, instance]
def has_groupoid_model_space (H : Type u_1) [topological_space H] (G : structure_groupoid H) :
has_groupoid H G

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

source
@[protected, instance]
def has_groupoid_continuous_groupoid {H : Type u} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] :
has_groupoid M (continuous_groupoid H)

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

source
def structure_groupoid.maximal_atlas {H : Type u} (M : Type u_2) [topological_space H] [topological_space M] [charted_space H M] (G : structure_groupoid H) :
set (local_homeomorph M H)

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

Equations
source
theorem structure_groupoid.subset_maximal_atlas {H : Type u} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] (G : structure_groupoid H) [has_groupoid M G] :
charted_space.atlas H M ⊆ structure_groupoid.maximal_atlas M G

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

source
theorem structure_groupoid.chart_mem_maximal_atlas {H : Type u} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] (G : structure_groupoid H) [has_groupoid M G] (x : M) :
charted_space.chart_at H x ∈ structure_groupoid.maximal_atlas M G
source
theorem mem_maximal_atlas_iff {H : Type u} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {G : structure_groupoid H} {e : local_homeomorph M H} :
e ∈ structure_groupoid.maximal_atlas M G ↔ ∀ (e' : local_homeomorph M H), e' ∈ charted_space.atlas H M → e.symm.trans e' ∈ G ∧ e'.symm.trans e ∈ G
source
theorem structure_groupoid.compatible_of_mem_maximal_atlas {H : Type u} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {G : structure_groupoid H} {e e' : local_homeomorph M H} (he : e ∈ structure_groupoid.maximal_atlas M G) (he' : e' ∈ structure_groupoid.maximal_atlas M G) :
e.symm.trans e' ∈ G

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

source
theorem structure_groupoid.id_mem_maximal_atlas {H : Type u} [topological_space H] (G : structure_groupoid H) :
local_homeomorph.refl H ∈ structure_groupoid.maximal_atlas H G

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

source
theorem structure_groupoid.mem_maximal_atlas_of_mem_groupoid {H : Type u} [topological_space H] (G : structure_groupoid H) {f : local_homeomorph H H} (hf : f ∈ G) :
f ∈ structure_groupoid.maximal_atlas H G

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

source
def local_homeomorph.singleton_charted_space {H : Type u} [topological_space H] {α : Type u_5} [topological_space α] (e : local_homeomorph α H) (h : e.to_local_equiv.source = set.univ) :
charted_space H α

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

Equations
source
@[simp]
theorem local_homeomorph.singleton_charted_space_chart_at_eq {H : Type u} [topological_space H] {α : Type u_5} [topological_space α] (e : local_homeomorph α H) (h : e.to_local_equiv.source = set.univ) {x : α} :
charted_space.chart_at H x = e
source
theorem local_homeomorph.singleton_charted_space_chart_at_source {H : Type u} [topological_space H] {α : Type u_5} [topological_space α] (e : local_homeomorph α H) (h : e.to_local_equiv.source = set.univ) {x : α} :
(charted_space.chart_at H x).to_local_equiv.source = set.univ
source
theorem local_homeomorph.singleton_charted_space_mem_atlas_eq {H : Type u} [topological_space H] {α : Type u_5} [topological_space α] (e : local_homeomorph α H) (h : e.to_local_equiv.source = set.univ) (e' : local_homeomorph α H) (h' : e' ∈ charted_space.atlas H α) :
e' = e
source
theorem local_homeomorph.singleton_has_groupoid {H : Type u} [topological_space H] {α : Type u_5} [topological_space α] (e : local_homeomorph α H) (h : e.to_local_equiv.source = set.univ) (G : structure_groupoid H) [closed_under_restriction G] :
has_groupoid α G

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

source
noncomputable def open_embedding.singleton_charted_space {H : Type u} [topological_space H] {α : Type u_5} [topological_space α] [nonempty α] {f : α → H} (h : open_embedding f) :
charted_space H α

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

Equations
source
theorem open_embedding.singleton_charted_space_chart_at_eq {H : Type u} [topological_space H] {α : Type u_5} [topological_space α] [nonempty α] {f : α → H} (h : open_embedding f) {x : α} :
⇑(charted_space.chart_at H x) = f
source
theorem open_embedding.singleton_has_groupoid {H : Type u} [topological_space H] {α : Type u_5} [topological_space α] [nonempty α] {f : α → H} (h : open_embedding f) (G : structure_groupoid H) [closed_under_restriction G] :
has_groupoid α G
source
@[protected, instance]
noncomputable def topological_space.opens.charted_space {H : Type u} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] (s : topological_space.opens M) :
charted_space H ↥s

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

Equations
source
@[protected, instance]
def topological_space.opens.has_groupoid {H : Type u} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] (G : structure_groupoid H) [has_groupoid M G] (s : topological_space.opens M) [closed_under_restriction G] :
has_groupoid ↥s G

If a groupoid G is closed_under_restriction, then an open subset of a space which is has_groupoid G is naturally has_groupoid G.

source
theorem topological_space.opens.chart_at_inclusion_symm_eventually_eq {H : Type u} {M : Type u_2} [topological_space H] [topological_space M] [charted_space H M] {U V : topological_space.opens M} (hUV : U ≤ V) {x : ↥U} :
⇑((charted_space.chart_at H (set.inclusion hUV x)).symm) =ᶠ[nhds (⇑(charted_space.chart_at H (set.inclusion hUV x)) (set.inclusion hUV x))] set.inclusion hUV ∘ ⇑((charted_space.chart_at H x).symm)

Structomorphisms #

source
@[nolint]
structure structomorph {H : Type u} [topological_space H] (G : structure_groupoid H) (M : Type u_5) (M' : Type u_6) [topological_space M] [topological_space M'] [charted_space H M] [charted_space H M'] :
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 structomorph
  • structomorph.has_sizeof_inst
source
def structomorph.refl {H : Type u} [topological_space H] {G : structure_groupoid H} (M : Type u_1) [topological_space M] [charted_space H M] [has_groupoid M G] :
structomorph G M M

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

Equations
source
def structomorph.symm {H : Type u} {M : Type u_2} {M' : Type u_3} [topological_space H] [topological_space M] [charted_space H M] [topological_space M'] {G : structure_groupoid H} [charted_space H M'] (e : structomorph G M M') :
structomorph G M' M

The inverse of a structomorphism is a structomorphism

Equations
source
def structomorph.trans {H : Type u} {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [topological_space H] [topological_space M] [charted_space H M] [topological_space M'] [topological_space M''] {G : structure_groupoid H} [charted_space H M'] [charted_space H M''] (e : structomorph G M M') (e' : structomorph G M' M'') :
structomorph G M M''

The composition of structomorphisms is a structomorphism

Equations