Charted spaces 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' : OpenPartialHomeomorph M H} : e ∈ atlas H M → e' ∈ atlas H M → e.symm.trans e' ∈ G

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

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

theorem hasGroupoid_of_le {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G₁ 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₁ 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' : OpenPartialHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → PG.property (↑(e.symm.trans e')) (e.symm.trans e').source) : HasGroupoid M PG.groupoid

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.

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 open partial homeomorphisms.

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

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

def StructureGroupoid.maximalAtlas {H : Type u} (M : Type u_2) [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (G : StructureGroupoid H) : Set (OpenPartialHomeomorph 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.

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 ⊆ 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 ∈ 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 : OpenPartialHomeomorph M H} : e ∈ StructureGroupoid.maximalAtlas M G ↔ ∀ e' ∈ atlas H M, e.symm.trans e' ∈ G ∧ e'.symm.trans 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 e' : OpenPartialHomeomorph M H} (he : e ∈ maximalAtlas M G) (he' : e' ∈ maximalAtlas 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.

theorem StructureGroupoid.mem_maximalAtlas_of_eqOnSource {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {e e' : OpenPartialHomeomorph M H} (h : e' ≈ e) (he : e ∈ maximalAtlas M G) : e' ∈ maximalAtlas M G

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

theorem StructureGroupoid.id_mem_maximalAtlas {H : Type u} [TopologicalSpace H] (G : StructureGroupoid H) : OpenPartialHomeomorph.refl H ∈ 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 : OpenPartialHomeomorph H H} (hf : f ∈ G) : f ∈ maximalAtlas H G

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

theorem StructureGroupoid.maximalAtlas_mono {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G G' : StructureGroupoid H} (h : G ≤ G') : maximalAtlas M G ⊆ maximalAtlas M G'

theorem restr_mem_maximalAtlas {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (G : StructureGroupoid H) [ClosedUnderRestriction G] {e : OpenPartialHomeomorph M H} (he : e ∈ StructureGroupoid.maximalAtlas M G) {s : Set M} (hs : IsOpen s) : e.restr s ∈ StructureGroupoid.maximalAtlas M G

If a structure groupoid G is closed under restriction, for any chart e in the maximal atlas, the restriction e.restr s to an open set s is also in the maximal atlas.

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

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

@[simp]

theorem OpenPartialHomeomorph.singletonChartedSpace_chartAt_eq {H : Type u} [TopologicalSpace H] {α : Type u_5} [TopologicalSpace α] (e : OpenPartialHomeomorph α H) (h : e.source = Set.univ) {x : α} : chartAt H x = e

theorem OpenPartialHomeomorph.singletonChartedSpace_chartAt_source {H : Type u} [TopologicalSpace H] {α : Type u_5} [TopologicalSpace α] (e : OpenPartialHomeomorph α H) (h : e.source = Set.univ) {x : α} : (chartAt H x).source = Set.univ

theorem OpenPartialHomeomorph.singletonChartedSpace_mem_atlas_eq {H : Type u} [TopologicalSpace H] {α : Type u_5} [TopologicalSpace α] (e : OpenPartialHomeomorph α H) (h : e.source = Set.univ) (e' : OpenPartialHomeomorph α H) (h' : e' ∈ ChartedSpace.atlas) : e' = e

theorem OpenPartialHomeomorph.singleton_hasGroupoid {H : Type u} [TopologicalSpace H] {α : Type u_5} [TopologicalSpace α] (e : OpenPartialHomeomorph α H) (h : e.source = Set.univ) (G : StructureGroupoid H) [ClosedUnderRestriction G] : HasGroupoid α G

Given an open 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 Topology.IsOpenEmbedding.singletonChartedSpace {H : Type u} [TopologicalSpace H] {α : Type u_5} [TopologicalSpace α] [Nonempty α] {f : α → H} (h : IsOpenEmbedding f) : ChartedSpace H α

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

theorem Topology.IsOpenEmbedding.singletonChartedSpace_chartAt_eq {H : Type u} [TopologicalSpace H] {α : Type u_5} [TopologicalSpace α] [Nonempty α] {f : α → H} (h : IsOpenEmbedding f) {x : α} : ↑(chartAt H x) = f

theorem Topology.IsOpenEmbedding.singleton_hasGroupoid {H : Type u} [TopologicalSpace H] {α : Type u_5} [TopologicalSpace α] [Nonempty α] {f : α → H} (h : IsOpenEmbedding 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 : Opens M) : ChartedSpace H ↥s

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

theorem TopologicalSpace.Opens.chartAt_eq {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {s : Opens M} {x : ↥s} : chartAt H x = (chartAt H ↑x).subtypeRestr ⋯

theorem TopologicalSpace.Opens.chart_eq {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {s : Opens M} (hs : Nonempty ↥s) {e : OpenPartialHomeomorph (↥s) H} (he : e ∈ atlas H ↥s) : ∃ (x : ↥s), e = (chartAt H ↑x).subtypeRestr hs

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

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

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

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

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

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

theorem StructureGroupoid.subtypeRestr_mem_maximalAtlas {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {e : OpenPartialHomeomorph M H} (he : e ∈ atlas H M) {s : TopologicalSpace.Opens M} (hs : Nonempty ↥s) {G : StructureGroupoid H} [HasGroupoid M G] [ClosedUnderRestriction G] : e.subtypeRestr hs ∈ maximalAtlas (↥s) G

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

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

@[deprecated StructureGroupoid.subtypeRestr_mem_maximalAtlas (since := "2025-08-17")]

theorem StructureGroupoid.restriction_in_maximalAtlas {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {e : OpenPartialHomeomorph M H} (he : e ∈ atlas H M) {s : TopologicalSpace.Opens M} (hs : Nonempty ↥s) {G : StructureGroupoid H} [HasGroupoid M G] [ClosedUnderRestriction G] : e.subtypeRestr hs ∈ maximalAtlas (↥s) G

Alias of StructureGroupoid.subtypeRestr_mem_maximalAtlas.

---

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

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

Structomorphisms

structure Structomorph {H : Type u} [TopologicalSpace H] (G : StructureGroupoid H) (M : Type u_5) (M' : Type u_6) [TopologicalSpace M] [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H M'] extends M ≃ₜ 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.

• 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 : OpenPartialHomeomorph M H) (c' : OpenPartialHomeomorph M' H) : c ∈ atlas H M → c' ∈ atlas H M' → c.symm.trans (self.toOpenPartialHomeomorph.trans 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.

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.

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.

theorem StructureGroupoid.restriction_mem_maximalAtlas_subtype {H : Type u} {M : Type u_2} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {G : StructureGroupoid H} {e : OpenPartialHomeomorph M H} (he : e ∈ atlas H M) (hs : Nonempty ↑e.source) [HasGroupoid M G] [ClosedUnderRestriction G] : let s := { carrier := e.source, is_open' := ⋯ }; let t := { carrier := e.target, is_open' := ⋯ }; ∀ c' ∈ atlas H ↥t, e.toHomeomorphSourceTarget.toOpenPartialHomeomorph.trans c' ∈ maximalAtlas (↥s) G

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

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

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