Structure groupoids

This file contains the definitions and properties of structure groupoids, i.e., sets of open partial homeomorphisms stable under composition and inverse. These are used to define charted spaces (and hence manifolds). See the file Mathlib.Geometry.Manifold.ChartedSpace for more details.

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.

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)

Notation

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

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

Composing two open partial homeomorphisms, by restricting to the maximal domain where their composition is well defined. Within the Manifold namespace, there is the notation e ≫ₕ f for this.

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

Composing two partial equivs, by restricting to the maximal domain where their composition is well defined. Within the Manifold namespace, there is the notation e ≫ f for this.

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 an open 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 an open 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 an open 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_2) [TopologicalSpace H] : Type u_2

A structure groupoid is a set of open 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 (OpenPartialHomeomorph H H)

  Members of the structure groupoid are open partial homeomorphisms.

• trans' (e e' : OpenPartialHomeomorph H H) : e ∈ self.members → e' ∈ self.members → e.trans e' ∈ self.members

  Structure groupoids are stable under composition.

• symm' (e : OpenPartialHomeomorph H H) : e ∈ self.members → e.symm ∈ self.members

  Structure groupoids are stable under inverse.

• id_mem' : OpenPartialHomeomorph.refl H ∈ self.members

  The identity morphism lies in the structure groupoid.

• locality' (e : OpenPartialHomeomorph H H) : (∀ x ∈ e.source, ∃ (s : Set H), IsOpen s ∧ x ∈ s ∧ e.restr s ∈ self.members) → e ∈ self.members

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

• mem_of_eqOnSource' (e e' : OpenPartialHomeomorph H H) : e ∈ self.members → e' ≈ e → e' ∈ self.members

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

instance instMembershipOpenPartialHomeomorphStructureGroupoid {H : Type u_1} [TopologicalSpace H] : Membership (OpenPartialHomeomorph H H) (StructureGroupoid H)

Equations

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

instance instSetLikeStructureGroupoidOpenPartialHomeomorph (H : Type u_2) [TopologicalSpace H] : SetLike (StructureGroupoid H) (OpenPartialHomeomorph H H)

Equations

• instSetLikeStructureGroupoidOpenPartialHomeomorph H = { coe := fun (s : StructureGroupoid H) => s.members, coe_injective' := ⋯ }

instance instMinStructureGroupoid {H : Type u_1} [TopologicalSpace H] : Min (StructureGroupoid H)

Equations

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

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

Equations

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

theorem StructureGroupoid.trans {H : Type u_1} [TopologicalSpace H] (G : StructureGroupoid H) {e e' : OpenPartialHomeomorph H H} (he : e ∈ G) (he' : e' ∈ G) : e.trans e' ∈ G

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

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

theorem StructureGroupoid.locality {H : Type u_1} [TopologicalSpace H] (G : StructureGroupoid H) {e : OpenPartialHomeomorph H H} (h : ∀ x ∈ e.source, ∃ (s : Set H), IsOpen s ∧ x ∈ s ∧ e.restr s ∈ G) : e ∈ G

theorem StructureGroupoid.mem_of_eqOnSource {H : Type u_1} [TopologicalSpace H] (G : StructureGroupoid H) {e e' : OpenPartialHomeomorph H H} (he : e ∈ G) (h : e' ≈ e) : e' ∈ G

theorem StructureGroupoid.mem_iff_of_eqOnSource {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} {e e' : OpenPartialHomeomorph H H} (h : e ≈ e') : e ∈ G ↔ e' ∈ G

instance StructureGroupoid.partialOrder {H : Type u_1} [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 ⋯

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

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

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

Equations

• idGroupoid H = { members := {OpenPartialHomeomorph.refl H} ∪ {e : OpenPartialHomeomorph H H | e.source = ∅}, trans' := ⋯, symm' := ⋯, id_mem' := ⋯, locality' := ⋯, mem_of_eqOnSource' := ⋯ }

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

Every structure groupoid contains the identity groupoid.

Equations

• instStructureGroupoidOrderBot = { bot := idGroupoid H, bot_le := ⋯ }

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

Equations

• instInhabitedStructureGroupoid = { default := idGroupoid H }

structure Pregroupoid (H : Type u_2) [TopologicalSpace H] : Type u_2

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

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

• comp {f g : 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)

  The pregroupoid property is stable under composition

• id_mem : self.property id Set.univ

  Pregroupoids contain the identity map (on 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

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

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

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

def Pregroupoid.groupoid {H : Type u_1} [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_1} [TopologicalSpace H] {PG : Pregroupoid H} {e : OpenPartialHomeomorph H H} : e ∈ PG.groupoid ↔ PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target

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

theorem mem_pregroupoid_of_eqOnSource {H : Type u_1} [TopologicalSpace H] (PG : Pregroupoid H) {e e' : OpenPartialHomeomorph H H} (he' : e ≈ e') (he : PG.property (↑e) e.source) : PG.property (↑e') e'.source

@[reducible, inline]

abbrev continuousPregroupoid (H : Type u_2) [TopologicalSpace H] : Pregroupoid H

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

Equations

• continuousPregroupoid H = { property := fun (x : H → H) (x_1 : Set H) => True, comp := ⋯, id_mem := trivial, locality := ⋯, congr := ⋯ }

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

Equations

• instInhabitedPregroupoid H = { default := continuousPregroupoid H }

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

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

Equations

• continuousGroupoid H = (continuousPregroupoid H).groupoid

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

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

Equations

• instStructureGroupoidOrderTop = { top := continuousGroupoid H, le_top := ⋯ }

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

Equations

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

class ClosedUnderRestriction {H : Type u_1} [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 : OpenPartialHomeomorph H H} : e ∈ G → ∀ (s : Set H), IsOpen s → e.restr s ∈ G

theorem closedUnderRestriction' {H : Type u_1} [TopologicalSpace H] {G : StructureGroupoid H} [ClosedUnderRestriction G] {e : OpenPartialHomeomorph H H} (he : e ∈ G) {s : Set H} (hs : IsOpen s) : e.restr s ∈ G

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

The trivial restriction-closed groupoid, containing only open 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_1} [TopologicalSpace H] {s : Set H} (hs : IsOpen s) : OpenPartialHomeomorph.ofSet s hs ∈ idRestrGroupoid

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

The trivial restriction-closed groupoid is indeed ClosedUnderRestriction.

theorem closedUnderRestriction_iff_id_le {H : Type u_1} [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_1} [TopologicalSpace H] : ClosedUnderRestriction (continuousGroupoid H)

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