Mathlib.Geometry.Manifold.ChartedSpace

Module docstring

{"# 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 ≫. ","### 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. ","### Charted spaces ","### Constructing a topology from an atlas ","### Charted space with a given structure groupoid ","### Structomorphisms "}

Manifold.term_≫ₕ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] scoped[Manifold] infixr:100 " ≫ₕ " => PartialHomeomorph.trans

Composition of partial homeomorphisms

Informal description

The notation `≫ₕ` denotes the composition of partial homeomorphisms. Given two partial homeomorphisms `e` and `e'`, the composition `e ≫ₕ e'` is the partial homeomorphism obtained by first applying `e` and then `e'`.

Manifold.term_≫_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] scoped[Manifold] infixr:100 " ≫ " => PartialEquiv.trans

Composition of partial equivalences

Informal description

The notation `≫` denotes the composition of partial equivalences between topological spaces. For two partial equivalences `e : PartialEquiv X Y` and `e' : PartialEquiv Y Z`, the composition `e ≫ e'` is a partial equivalence from `X` to `Z` obtained by composing the underlying functions and their inverses.

StructureGroupoid structure

(H : Type u) [TopologicalSpace H]

Full source

/-- 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. -/
structure StructureGroupoid (H : Type u) [TopologicalSpace H] where
  /-- Members of the structure groupoid are partial homeomorphisms. -/
  members : Set (PartialHomeomorph H H)
  /-- Structure groupoids are stable under composition. -/
  trans' : ∀ e e' : PartialHomeomorph H H, e ∈ members → e' ∈ members → e ≫ₕ e'e ≫ₕ e' ∈ members
  /-- Structure groupoids are stable under inverse. -/
  symm' : ∀ e : PartialHomeomorph H H, e ∈ members → e.symm ∈ members
  /-- The identity morphism lies in the structure groupoid. -/
  id_mem' : PartialHomeomorph.reflPartialHomeomorph.refl H ∈ members
  /-- Let `e` be a 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. -/
  locality' : ∀ e : PartialHomeomorph H H,
    (∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ members) → e ∈ members
  /-- Membership in a structure groupoid respects the equivalence of partial homeomorphisms. -/
  mem_of_eqOnSource' : ∀ e e' : PartialHomeomorph H H, e ∈ members → e' ≈ e → e' ∈ members

Structure groupoid on a topological space

Informal description

A structure groupoid on a topological space $H$ is a collection of partial homeomorphisms of $H$ that is closed under composition, inversion, and restriction to open subsets. These groupoids are used to define smoothness conditions on manifolds by requiring that coordinate changes between charts belong to the groupoid.

instMembershipPartialHomeomorphStructureGroupoid instance

: Membership (PartialHomeomorph H H) (StructureGroupoid H)

Full source

instance : Membership (PartialHomeomorph H H) (StructureGroupoid H) :=
  ⟨fun (G : StructureGroupoid H) (e : PartialHomeomorph H H) ↦ e ∈ G.members⟩

Membership Relation between Partial Homeomorphisms and Structure Groupoids

Informal description

For any topological space $H$, there is a membership relation between partial homeomorphisms of $H$ and structure groupoids on $H$. This means that given a partial homeomorphism $e$ of $H$ and a structure groupoid $G$ on $H$, we can say that $e$ belongs to $G$ (denoted $e \in G$) if $e$ is one of the partial homeomorphisms in the collection defining $G$.

instSetLikeStructureGroupoidPartialHomeomorph instance

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

Full source

instance (H : Type u) [TopologicalSpace H] :
    SetLike (StructureGroupoid H) (PartialHomeomorph H H) where
  coe s := s.members
  coe_injective' N O h := by cases N; cases O; congr

Set-like Structure for Structure Groupoids of Partial Homeomorphisms

Informal description

For any topological space $H$, the structure groupoid on $H$ can be treated as a set-like structure where its elements are partial homeomorphisms of $H$. This means that a structure groupoid can be viewed as a collection of partial homeomorphisms, with a membership relation and a coercion to the type of subsets of partial homeomorphisms.

instMinStructureGroupoid instance

: Min (StructureGroupoid H)

Full source

instance : Min (StructureGroupoid H) :=
  ⟨fun G G' => StructureGroupoid.mk
    (members := G.members ∩ G'.members)
    (trans' := fun e e' he he' =>
      ⟨G.trans' e e' he.left he'.left, G'.trans' e e' he.right he'.right⟩)
    (symm' := fun e he => ⟨G.symm' e he.left, G'.symm' e he.right⟩)
    (id_mem' := ⟨G.id_mem', G'.id_mem'⟩)
    (locality' := by
      intro e hx
      apply (mem_inter_iff e G.members G'.members).mpr
      refine And.intro (G.locality' e ?_) (G'.locality' e ?_)
      all_goals
        intro x hex
        rcases hx x hex with ⟨s, hs⟩
        use s
        refine And.intro hs.left (And.intro hs.right.left ?_)
      · exact hs.right.right.left
      · exact hs.right.right.right)
    (mem_of_eqOnSource' := fun e e' he hee' =>
      ⟨G.mem_of_eqOnSource' e e' he.left hee', G'.mem_of_eqOnSource' e e' he.right hee'⟩)⟩

Existence of Minimal Structure Groupoid on a Topological Space

Informal description

For any topological space $H$, the collection of structure groupoids on $H$ has a minimal element with respect to inclusion. This minimal structure groupoid contains only the identity partial homeomorphism and is closed under composition, inversion, and restriction.

instInfSetStructureGroupoid instance

: InfSet (StructureGroupoid H)

Full source

instance : InfSet (StructureGroupoid H) :=
  ⟨fun S => StructureGroupoid.mk
    (members := ⋂ s ∈ S, s.members)
    (trans' := by
      simp only [mem_iInter]
      intro e e' he he' i hi
      exact i.trans' e e' (he i hi) (he' i hi))
    (symm' := by
      simp only [mem_iInter]
      intro e he i hi
      exact i.symm' e (he i hi))
    (id_mem' := by
      simp only [mem_iInter]
      intro i _
      exact i.id_mem')
    (locality' := by
      simp only [mem_iInter]
      intro e he i hi
      refine i.locality' e ?_
      intro x hex
      rcases he x hex with ⟨s, hs⟩
      exact ⟨s, ⟨hs.left, ⟨hs.right.left, hs.right.right i hi⟩⟩⟩)
    (mem_of_eqOnSource' := by
      simp only [mem_iInter]
      intro e e' he he'e
      exact fun i hi => i.mem_of_eqOnSource' e e' (he i hi) he'e)⟩

Infimum of Structure Groupoids on a Topological Space

Informal description

For any topological space $H$, the collection of structure groupoids on $H$ has an infimum structure. This means that given a family of structure groupoids $\{G_i\}_{i \in I}$ on $H$, their infimum $\bigcap_i G_i$ is also a structure groupoid on $H$, consisting of all partial homeomorphisms that belong to every $G_i$.

StructureGroupoid.trans theorem

(G : StructureGroupoid H) {e e' : PartialHomeomorph H H} (he : e ∈ G) (he' : e' ∈ G) : e ≫ₕ e' ∈ G

Full source

theorem StructureGroupoid.trans (G : StructureGroupoid H) {e e' : PartialHomeomorph H H}
    (he : e ∈ G) (he' : e' ∈ G) : e ≫ₕ e'e ≫ₕ e' ∈ G :=
  G.trans' e e' he he'

Closure of Structure Groupoid under Composition

Informal description

For any structure groupoid $G$ on a topological space $H$, if two partial homeomorphisms $e$ and $e'$ of $H$ belong to $G$, then their composition $e \circ e'$ also belongs to $G$.

StructureGroupoid.symm theorem

(G : StructureGroupoid H) {e : PartialHomeomorph H H} (he : e ∈ G) : e.symm ∈ G

Full source

theorem StructureGroupoid.symm (G : StructureGroupoid H) {e : PartialHomeomorph H H} (he : e ∈ G) :
    e.symm ∈ G :=
  G.symm' e he

Inverse Preservation in Structure Groupoids

Informal description

For any structure groupoid $G$ on a topological space $H$, if a partial homeomorphism $e$ of $H$ belongs to $G$, then its inverse $e^{-1}$ also belongs to $G$.

StructureGroupoid.id_mem theorem

(G : StructureGroupoid H) : PartialHomeomorph.refl H ∈ G

Full source

theorem StructureGroupoid.id_mem (G : StructureGroupoid H) : PartialHomeomorph.reflPartialHomeomorph.refl H ∈ G :=
  G.id_mem'

Identity Partial Homeomorphism Belongs to Structure Groupoid

Informal description

For any structure groupoid $G$ on a topological space $H$, the identity partial homeomorphism $\mathrm{refl}_H$ belongs to $G$.

StructureGroupoid.locality theorem

 (G : StructureGroupoid H) {e : PartialHomeomorph H H} (h : ∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ G) :
  e ∈ G

Full source

theorem StructureGroupoid.locality (G : StructureGroupoid H) {e : PartialHomeomorph H H}
    (h : ∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ G) : e ∈ G :=
  G.locality' e h

Local Membership Criterion for Structure Groupoids

Informal description

Let $G$ be a structure groupoid on a topological space $H$ and let $e$ be a partial homeomorphism of $H$. If for every point $x$ in the source of $e$ there exists an open neighborhood $s$ of $x$ such that the restriction of $e$ to $s$ belongs to $G$, then $e$ itself belongs to $G$.

StructureGroupoid.mem_of_eqOnSource theorem

(G : StructureGroupoid H) {e e' : PartialHomeomorph H H} (he : e ∈ G) (h : e' ≈ e) : e' ∈ G

Full source

theorem StructureGroupoid.mem_of_eqOnSource (G : StructureGroupoid H) {e e' : PartialHomeomorph H H}
    (he : e ∈ G) (h : e' ≈ e) : e' ∈ G :=
  G.mem_of_eqOnSource' e e' he h

Equivalence on Source Preserves Membership in Structure Groupoid

Informal description

Let $G$ be a structure groupoid on a topological space $H$. For any two partial homeomorphisms $e$ and $e'$ of $H$, if $e$ belongs to $G$ and $e'$ is equivalent to $e$ on their common source (i.e., $e' \approx e$), then $e'$ also belongs to $G$.

StructureGroupoid.mem_iff_of_eqOnSource theorem

{G : StructureGroupoid H} {e e' : PartialHomeomorph H H} (h : e ≈ e') : e ∈ G ↔ e' ∈ G

Full source

theorem StructureGroupoid.mem_iff_of_eqOnSource {G : StructureGroupoid H}
    {e e' : PartialHomeomorph H H} (h : e ≈ e') : e ∈ Ge ∈ G ↔ e' ∈ G :=
  ⟨fun he ↦ G.mem_of_eqOnSource he (Setoid.symm h), fun he' ↦ G.mem_of_eqOnSource he' h⟩

Membership in Structure Groupoid is Preserved by Source Equivalence

Informal description

Let $G$ be a structure groupoid on a topological space $H$, and let $e$ and $e'$ be partial homeomorphisms of $H$ that are equivalent on their common source (i.e., $e \approx e'$). Then $e$ belongs to $G$ if and only if $e'$ belongs to $G$.

StructureGroupoid.partialOrder instance

: PartialOrder (StructureGroupoid H)

Full source

/-- Partial order on the set of groupoids, given by inclusion of the members of the groupoid. -/
instance StructureGroupoid.partialOrder : PartialOrder (StructureGroupoid H) :=
  PartialOrder.lift StructureGroupoid.members fun a b h ↦ by
    cases a
    cases b
    dsimp at h
    induction h
    rfl

Partial Order on Structure Groupoids by Inclusion

Informal description

The collection of structure groupoids on a topological space $H$ forms a partial order under inclusion, where for two structure groupoids $G_1$ and $G_2$, we say $G_1 \leq G_2$ if every partial homeomorphism in $G_1$ also belongs to $G_2$.

StructureGroupoid.le_iff theorem

{G₁ G₂ : StructureGroupoid H} : G₁ ≤ G₂ ↔ ∀ e, e ∈ G₁ → e ∈ G₂

Full source

theorem StructureGroupoid.le_iff {G₁ G₂ : StructureGroupoid H} : G₁ ≤ G₂ ↔ ∀ e, e ∈ G₁ → e ∈ G₂ :=
  Iff.rfl

Characterization of Structure Groupoid Inclusion

Informal description

For two structure groupoids $G_1$ and $G_2$ on a topological space $H$, the inclusion $G_1 \leq G_2$ holds if and only if every partial homeomorphism $e$ that belongs to $G_1$ also belongs to $G_2$.

idGroupoid definition

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

Full source

/-- The trivial groupoid, containing only the identity (and maps with empty source, as this is
necessary from the definition). -/
def idGroupoid (H : Type u) [TopologicalSpace H] : StructureGroupoid H where
  members := {PartialHomeomorph.refl H}{PartialHomeomorph.refl H} ∪ { e : PartialHomeomorph H H | e.source = ∅ }
  trans' e e' he he' := by
    rcases he with he | he
    · simpa only [mem_singleton_iff.1 he, refl_trans]
    · have : (e ≫ₕ e').source ⊆ e.source := sep_subset _ _
      rw [he] at this
      have : e ≫ₕ e'e ≫ₕ e' ∈ { e : PartialHomeomorph H H | e.source = ∅ } := eq_bot_iff.2 this
      exact (mem_union _ _ _).2 (Or.inr this)
  symm' e he := by
    rcases (mem_union _ _ _).1 he with E | E
    · simp [mem_singleton_iff.mp E]
    · right
      simpa only [e.toPartialEquiv.image_source_eq_target.symm, mfld_simps] using E
  id_mem' := mem_union_left _ rfl
  locality' e he := by
    rcases e.source.eq_empty_or_nonempty with h | h
    · right
      exact h
    · left
      rcases h with ⟨x, hx⟩
      rcases he x hx with ⟨s, open_s, xs, hs⟩
      have x's : x ∈ (e.restr s).source := by
        rw [restr_source, open_s.interior_eq]
        exact ⟨hx, xs⟩
      rcases hs with hs | hs
      · replace hs : PartialHomeomorph.restr e s = PartialHomeomorph.refl H := by
          simpa only using hs
        have : (e.restr s).source = univ := by
          rw [hs]
          simp
        have : e.toPartialEquiv.source ∩ interior s = univ := this
        have : univuniv ⊆ interior s := by
          rw [← this]
          exact inter_subset_right
        have : s = univ := by rwa [open_s.interior_eq, univ_subset_iff] at this
        simpa only [this, restr_univ] using hs
      · exfalso
        rw [mem_setOf_eq] at hs
        rwa [hs] at x's
  mem_of_eqOnSource' e e' he he'e := by
    rcases he with he | he
    · left
      have : e = e' := by
        refine eq_of_eqOnSource_univ (Setoid.symm he'e) ?_ ?_ <;>
          rw [Set.mem_singleton_iff.1 he] <;> rfl
      rwa [← this]
    · right
      have he : e.toPartialEquiv.source = ∅ := he
      rwa [Set.mem_setOf_eq, EqOnSource.source_eq he'e]

Trivial structure groupoid

Informal description

The trivial structure groupoid on a topological space $H$ consists of only the identity partial homeomorphism (where the source and target are the entire space $H$) and all partial homeomorphisms with empty source. More formally, the `idGroupoid` is defined as the structure groupoid where: - The members are the singleton set containing the identity partial homeomorphism $\{\text{PartialHomeomorph.refl } H\}$ together with all partial homeomorphisms $e$ of $H$ for which $e.\text{source} = \emptyset$. - The groupoid is closed under composition, inversion, and satisfies the locality condition (a partial homeomorphism belongs to the groupoid if it does so locally at every point in its domain).

instStructureGroupoidOrderBot instance

: OrderBot (StructureGroupoid H)

Full source

/-- Every structure groupoid contains the identity groupoid. -/
instance instStructureGroupoidOrderBot : OrderBot (StructureGroupoid H) where
  bot := idGroupoid H
  bot_le := by
    intro u f hf
    have hf : f ∈ {PartialHomeomorph.refl H} ∪ { e : PartialHomeomorph H H | e.source = ∅ } := hf
    simp only [singleton_union, mem_setOf_eq, mem_insert_iff] at hf
    rcases hf with hf | hf
    · rw [hf]
      apply u.id_mem
    · apply u.locality
      intro x hx
      rw [hf, mem_empty_iff_false] at hx
      exact hx.elim

The Trivial Structure Groupoid is the Bottom Element

Informal description

The collection of all structure groupoids on a topological space $H$ forms an order with a bottom element, where the bottom element is the trivial structure groupoid consisting only of the identity partial homeomorphism and all partial homeomorphisms with empty source.

instInhabitedStructureGroupoid instance

: Inhabited (StructureGroupoid H)

Full source

instance : Inhabited (StructureGroupoid H) := ⟨idGroupoid H⟩

Nonempty Structure Groupoids on a Topological Space

Informal description

For any topological space $H$, the collection of all structure groupoids on $H$ is nonempty. In particular, the trivial structure groupoid (consisting only of the identity partial homeomorphism and all partial homeomorphisms with empty source) provides a canonical inhabitant.

Pregroupoid structure

(H : Type*) [TopologicalSpace H]

Full source

/-- 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. -/
structure Pregroupoid (H : Type*) [TopologicalSpace H] where
  /-- Property describing membership in this groupoid: the pregroupoid "contains"
    all functions `H → H` having the pregroupoid property on some `s : Set H` -/
  property : (H → H) → Set H → Prop
  /-- The pregroupoid property is stable under composition -/
  comp : ∀ {f g u v}, property f u → property g v →
    IsOpen u → IsOpen v → IsOpen (u ∩ f ⁻¹' v) → property (g ∘ f) (u ∩ f ⁻¹' v)
  /-- Pregroupoids contain the identity map (on `univ`) -/
  id_mem : property id univ
  /-- 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 -/
  locality :
    ∀ {f u}, IsOpen u → (∀ x ∈ u, ∃ v, IsOpen v ∧ x ∈ v ∧ property f (u ∩ v)) → property f u
  /-- If `f = g` on `u` and `property f u`, then `property g u` -/
  congr : ∀ {f g : H → H} {u}, IsOpen u → (∀ x ∈ u, g x = f x) → property f u → property g u

Pregroupoid on a topological space

Informal description

A pregroupoid on a topological space $H$ is a collection of partial homeomorphisms of $H$ that is closed under composition and restriction, but not necessarily under inversion. It serves as a precursor to defining a structure groupoid, where both the function and its inverse satisfy certain properties.

Pregroupoid.groupoid definition

(PG : Pregroupoid H) : StructureGroupoid H

Full source

/-- 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. -/
def Pregroupoid.groupoid (PG : Pregroupoid H) : StructureGroupoid H where
  members := { e : PartialHomeomorph H H | PG.property e e.source ∧ PG.property e.symm e.target }
  trans' e e' he he' := by
    constructor
    · apply PG.comp he.1 he'.1 e.open_source e'.open_source
      apply e.continuousOn_toFun.isOpen_inter_preimage e.open_source e'.open_source
    · apply PG.comp he'.2 he.2 e'.open_target e.open_target
      apply e'.continuousOn_invFun.isOpen_inter_preimage e'.open_target e.open_target
  symm' _ he := ⟨he.2, he.1⟩
  id_mem' := ⟨PG.id_mem, PG.id_mem⟩
  locality' e he := by
    constructor
    · refine PG.locality e.open_source fun x xu ↦ ?_
      rcases he x xu with ⟨s, s_open, xs, hs⟩
      refine ⟨s, s_open, xs, ?_⟩
      convert hs.1 using 1
      dsimp [PartialHomeomorph.restr]
      rw [s_open.interior_eq]
    · refine PG.locality e.open_target fun x xu ↦ ?_
      rcases he (e.symm x) (e.map_target xu) with ⟨s, s_open, xs, hs⟩
      refine ⟨e.target ∩ e.symm ⁻¹' s, ?_, ⟨xu, xs⟩, ?_⟩
      · exact ContinuousOn.isOpen_inter_preimage e.continuousOn_invFun e.open_target s_open
      · rw [← inter_assoc, inter_self]
        convert hs.2 using 1
        dsimp [PartialHomeomorph.restr]
        rw [s_open.interior_eq]
  mem_of_eqOnSource' e e' he ee' := by
    constructor
    · apply PG.congr e'.open_source ee'.2
      simp only [ee'.1, he.1]
    · have A := EqOnSource.symm' ee'
      apply PG.congr e'.symm.open_source A.2
      -- Porting note: was
      -- convert he.2
      -- rw [A.1]
      -- rfl
      rw [A.1, symm_toPartialEquiv, PartialEquiv.symm_source]
      exact he.2

Structure groupoid induced by a pregroupoid

Informal description

Given a pregroupoid $PG$ on a topological space $H$, the associated structure groupoid consists of all partial homeomorphisms $e$ of $H$ such that both $e$ restricted to its source and $e^{-1}$ restricted to its target satisfy the property defined by $PG$. More formally, the structure groupoid $PG.\text{groupoid}$ is defined as the collection of partial homeomorphisms $e$ where: 1. $e$ satisfies $PG$'s property on its source set $e.\text{source}$ 2. The inverse $e^{-1}$ satisfies $PG$'s property on its target set $e.\text{target}$ This construction ensures that the resulting structure groupoid is closed under composition, inversion, and restriction to open subsets, and contains the identity homeomorphism.

mem_groupoid_of_pregroupoid theorem

 {PG : Pregroupoid H} {e : PartialHomeomorph H H} :
  e ∈ PG.groupoid ↔ PG.property e e.source ∧ PG.property e.symm e.target

Full source

theorem mem_groupoid_of_pregroupoid {PG : Pregroupoid H} {e : PartialHomeomorph H H} :
    e ∈ PG.groupoide ∈ PG.groupoid ↔ PG.property e e.source ∧ PG.property e.symm e.target :=
  Iff.rfl

Characterization of Membership in Pregroupoid-Induced Structure Groupoid

Informal description

Let $H$ be a topological space, $PG$ a pregroupoid on $H$, and $e$ a partial homeomorphism of $H$. Then $e$ belongs to the structure groupoid induced by $PG$ if and only if: 1. $e$ satisfies the property defined by $PG$ on its source set $e.\text{source}$ 2. The inverse $e^{-1}$ satisfies the property defined by $PG$ on its target set $e.\text{target}$

groupoid_of_pregroupoid_le theorem

 (PG₁ PG₂ : Pregroupoid H) (h : ∀ f s, PG₁.property f s → PG₂.property f s) : PG₁.groupoid ≤ PG₂.groupoid

Full source

theorem groupoid_of_pregroupoid_le (PG₁ PG₂ : Pregroupoid H)
    (h : ∀ f s, PG₁.property f s → PG₂.property f s) : PG₁.groupoid ≤ PG₂.groupoid := by
  refine StructureGroupoid.le_iff.2 fun e he ↦ ?_
  rw [mem_groupoid_of_pregroupoid] at he ⊢
  exact ⟨h _ _ he.1, h _ _ he.2⟩

Inclusion of Structure Groupoids Induced by Pregroupoid Property Implication

Informal description

Let $H$ be a topological space, and let $\mathrm{PG}_1$ and $\mathrm{PG}_2$ be two pregroupoids on $H$. If for every partial function $f$ and every subset $s$ of $H$, the property $\mathrm{PG}_1.\mathrm{property}(f, s)$ implies $\mathrm{PG}_2.\mathrm{property}(f, s)$, then the structure groupoid induced by $\mathrm{PG}_1$ is contained in the structure groupoid induced by $\mathrm{PG}_2$.

mem_pregroupoid_of_eqOnSource theorem

 (PG : Pregroupoid H) {e e' : PartialHomeomorph H H} (he' : e ≈ e') (he : PG.property e e.source) :
  PG.property e' e'.source

Full source

theorem mem_pregroupoid_of_eqOnSource (PG : Pregroupoid H) {e e' : PartialHomeomorph H H}
    (he' : e ≈ e') (he : PG.property e e.source) : PG.property e' e'.source := by
  rw [← he'.1]
  exact PG.congr e.open_source he'.eqOn.symm he

Pregroupoid Property Preservation under Source Equivalence

Informal description

Let $H$ be a topological space and let $\mathrm{PG}$ be a pregroupoid on $H$. For any two partial homeomorphisms $e$ and $e'$ of $H$ that are equivalent under the relation $\approx$ (i.e., they agree on their common source set), if $e$ satisfies the property $\mathrm{PG}.\mathrm{property}$ on its source set, then $e'$ also satisfies $\mathrm{PG}.\mathrm{property}$ on its source set.

continuousPregroupoid abbrev

(H : Type*) [TopologicalSpace H] : Pregroupoid H

Full source

/-- The pregroupoid of all partial maps on a topological space `H`. -/
abbrev continuousPregroupoid (H : Type*) [TopologicalSpace H] : Pregroupoid H where
  property _ _ := True
  comp _ _ _ _ _ := trivial
  id_mem := trivial
  locality _ _ := trivial
  congr _ _ _ := trivial

Continuous Pregroupoid on a Topological Space

Informal description

The continuous pregroupoid on a topological space $H$ is the collection of all partial maps on $H$ that are continuous on their domains of definition.

instInhabitedPregroupoid instance

(H : Type*) [TopologicalSpace H] : Inhabited (Pregroupoid H)

Full source

instance (H : Type*) [TopologicalSpace H] : Inhabited (Pregroupoid H) :=
  ⟨continuousPregroupoid H⟩

Nonempty Pregroupoid on a Topological Space

Informal description

For any topological space $H$, the collection of all partial homeomorphisms of $H$ forms a pregroupoid, and this collection is nonempty.

continuousGroupoid definition

(H : Type*) [TopologicalSpace H] : StructureGroupoid H

Full source

/-- The groupoid of all partial homeomorphisms on a topological space `H`. -/
def continuousGroupoid (H : Type*) [TopologicalSpace H] : StructureGroupoid H :=
  Pregroupoid.groupoid (continuousPregroupoid H)

Continuous groupoid on a topological space

Informal description

The continuous groupoid on a topological space $H$ is the structure groupoid consisting of all partial homeomorphisms of $H$. It is constructed as the groupoid induced by the continuous pregroupoid, which contains all partial maps on $H$ that are continuous on their domains of definition.

instStructureGroupoidOrderTop instance

: OrderTop (StructureGroupoid H)

Full source

/-- Every structure groupoid is contained in the groupoid of all partial homeomorphisms. -/
instance instStructureGroupoidOrderTop : OrderTop (StructureGroupoid H) where
  top := continuousGroupoid H
  le_top _ _ _ := ⟨trivial, trivial⟩

The Continuous Groupoid as the Greatest Structure Groupoid

Informal description

The collection of all structure groupoids on a topological space $H$ forms a partially ordered set with a greatest element, where the greatest element is the continuous groupoid consisting of all partial homeomorphisms of $H$.

instCompleteLatticeStructureGroupoid instance

: CompleteLattice (StructureGroupoid H)

Full source

instance : CompleteLattice (StructureGroupoid H) :=
  { SetLike.instPartialOrder,
    completeLatticeOfInf _ (by
      exact fun s =>
      ⟨fun S Ss F hF => mem_iInter₂.mp hF S Ss,
      fun T Tl F fT => mem_iInter₂.mpr (fun i his => Tl his fT)⟩) with
    le := (· ≤ ·)
    lt := (· < ·)
    bot := instStructureGroupoidOrderBot.bot
    bot_le := instStructureGroupoidOrderBot.bot_le
    top := instStructureGroupoidOrderTop.top
    le_top := instStructureGroupoidOrderTop.le_top
    inf := (· ⊓ ·)
    le_inf := fun _ _ _ h₁₂ h₁₃ _ hm ↦ ⟨h₁₂ hm, h₁₃ hm⟩
    inf_le_left := fun _ _ _ ↦ And.left
    inf_le_right := fun _ _ _ ↦ And.right }

Complete Lattice Structure on Structure Groupoids

Informal description

The collection of all structure groupoids on a topological space $H$ forms a complete lattice. In this lattice: - The partial order is given by inclusion of structure groupoids. - The infimum of a family of structure groupoids is their intersection. - The supremum of a family of structure groupoids is the smallest structure groupoid containing all of them. - The bottom element is the trivial structure groupoid containing only the identity and empty partial homeomorphisms. - The top element is the continuous groupoid containing all partial homeomorphisms of $H$.

ClosedUnderRestriction structure

(G : StructureGroupoid H)

Full source

/-- A groupoid is closed under restriction if it contains all restrictions of its element local
homeomorphisms to open subsets of the source. -/
class ClosedUnderRestriction (G : StructureGroupoid H) : Prop where
  closedUnderRestriction :
    ∀ {e : PartialHomeomorph H H}, e ∈ G → ∀ s : Set H, IsOpen s → e.restr s ∈ G

Restriction-closed structure groupoid

Informal description

A structure groupoid $G$ on a topological space $H$ is said to be *closed under restriction* if for every partial homeomorphism $e$ in $G$ and every open subset $s$ of the source of $e$, the restriction of $e$ to $s$ also belongs to $G$.

closedUnderRestriction' theorem

 {G : StructureGroupoid H} [ClosedUnderRestriction G] {e : PartialHomeomorph H H} (he : e ∈ G) {s : Set H}
  (hs : IsOpen s) : e.restr s ∈ G

Full source

theorem closedUnderRestriction' {G : StructureGroupoid H} [ClosedUnderRestriction G]
    {e : PartialHomeomorph H H} (he : e ∈ G) {s : Set H} (hs : IsOpen s) : e.restr s ∈ G :=
  ClosedUnderRestriction.closedUnderRestriction he s hs

Restriction of Partial Homeomorphism in Structure Groupoid

Informal description

Let $G$ be a structure groupoid on a topological space $H$ that is closed under restriction. For any partial homeomorphism $e \in G$ and any open subset $s \subseteq H$, the restriction of $e$ to $s$, denoted $e.restr\, s$, also belongs to $G$.

idRestrGroupoid definition

: StructureGroupoid H

Full source

/-- The trivial restriction-closed groupoid, containing only partial homeomorphisms equivalent
to the restriction of the identity to the various open subsets. -/
def idRestrGroupoid : StructureGroupoid H where
  members := { e | ∃ (s : Set H) (h : IsOpen s), e ≈ PartialHomeomorph.ofSet s h }
  trans' := by
    rintro e e' ⟨s, hs, hse⟩ ⟨s', hs', hse'⟩
    refine ⟨s ∩ s', hs.inter hs', ?_⟩
    have := PartialHomeomorph.EqOnSource.trans' hse hse'
    rwa [PartialHomeomorph.ofSet_trans_ofSet] at this
  symm' := by
    rintro e ⟨s, hs, hse⟩
    refine ⟨s, hs, ?_⟩
    rw [← ofSet_symm]
    exact PartialHomeomorph.EqOnSource.symm' hse
  id_mem' := ⟨univ, isOpen_univ, by simp only [mfld_simps, refl]⟩
  locality' := by
    intro e h
    refine ⟨e.source, e.open_source, by simp only [mfld_simps], ?_⟩
    intro x hx
    rcases h x hx with ⟨s, hs, hxs, s', hs', hes'⟩
    have hes : x ∈ (e.restr s).source := by
      rw [e.restr_source]
      refine ⟨hx, ?_⟩
      rw [hs.interior_eq]
      exact hxs
    simpa only [mfld_simps] using PartialHomeomorph.EqOnSource.eqOn hes' hes
  mem_of_eqOnSource' := by
    rintro e e' ⟨s, hs, hse⟩ hee'
    exact ⟨s, hs, Setoid.trans hee' hse⟩

Identity restriction groupoid

Informal description

The *identity restriction groupoid* on a topological space $H$ is the structure groupoid consisting of all partial homeomorphisms that are equivalent (in the sense of `EqOnSource`) to the identity partial homeomorphism restricted to some open subset of $H$. More precisely, a partial homeomorphism $e$ belongs to this groupoid if there exists an open subset $s \subseteq H$ such that $e$ is equivalent to the identity map restricted to $s$ (i.e., $e \approx \text{ofSet}\ s\ hs$ where $hs$ is a proof that $s$ is open). This groupoid is: 1. Closed under composition (transitivity) 2. Closed under inversion (symmetry) 3. Contains the identity partial homeomorphism 4. Satisfies the locality condition (if a partial homeomorphism locally belongs to the groupoid around each point in its source, then it belongs to the groupoid) 5. Stable under equivalence (if $e'$ is equivalent to some $e$ in the groupoid, then $e'$ also belongs to the groupoid)

idRestrGroupoid_mem theorem

{s : Set H} (hs : IsOpen s) : ofSet s hs ∈ @idRestrGroupoid H _

Full source

theorem idRestrGroupoid_mem {s : Set H} (hs : IsOpen s) : ofSetofSet s hs ∈ @idRestrGroupoid H _ :=
  ⟨s, hs, refl _⟩

Membership of Identity Partial Homeomorphism in Identity Restriction Groupoid

Informal description

For any open subset $s$ of a topological space $H$, the identity partial homeomorphism $\text{ofSet}\, s\, hs$ (where $hs$ is a proof that $s$ is open) belongs to the identity restriction groupoid on $H$.

closedUnderRestriction_idRestrGroupoid instance

: ClosedUnderRestriction (@idRestrGroupoid H _)

Full source

/-- The trivial restriction-closed groupoid is indeed `ClosedUnderRestriction`. -/
instance closedUnderRestriction_idRestrGroupoid : ClosedUnderRestriction (@idRestrGroupoid H _) :=
  ⟨by
    rintro e ⟨s', hs', he⟩ s hs
    use s' ∩ s, hs'.inter hs
    refine Setoid.trans (PartialHomeomorph.EqOnSource.restr he s) ?_
    exact ⟨by simp only [hs.interior_eq, mfld_simps], by simp only [mfld_simps, eqOn_refl]⟩⟩

Identity Restriction Groupoid is Closed Under Restriction

Informal description

The identity restriction groupoid on a topological space $H$ is closed under restriction. This means that for any partial homeomorphism $e$ in this groupoid and any open subset $s$ of the source of $e$, the restriction of $e$ to $s$ also belongs to the groupoid.

closedUnderRestriction_iff_id_le theorem

(G : StructureGroupoid H) : ClosedUnderRestriction G ↔ idRestrGroupoid ≤ G

Full source

/-- A groupoid is closed under restriction if and only if it contains the trivial restriction-closed
groupoid. -/
theorem closedUnderRestriction_iff_id_le (G : StructureGroupoid H) :
    ClosedUnderRestrictionClosedUnderRestriction G ↔ idRestrGroupoid ≤ G := by
  constructor
  · intro _i
    rw [StructureGroupoid.le_iff]
    rintro e ⟨s, hs, hes⟩
    refine G.mem_of_eqOnSource ?_ hes
    convert closedUnderRestriction' G.id_mem hs
    -- Porting note: was
    -- change s = _ ∩ _
    -- rw [hs.interior_eq]
    -- simp only [mfld_simps]
    ext
    · rw [PartialHomeomorph.restr_apply, PartialHomeomorph.refl_apply, id, ofSet_apply, id_eq]
    · simp [hs]
    · simp [hs.interior_eq]
  · intro h
    constructor
    intro e he s hs
    rw [← ofSet_trans (e : PartialHomeomorph H H) hs]
    refine G.trans ?_ he
    apply StructureGroupoid.le_iff.mp h
    exact idRestrGroupoid_mem hs

Characterization of Restriction-Closed Groupoids via Identity Groupoid Inclusion

Informal description

A structure groupoid $G$ on a topological space $H$ is closed under restriction if and only if the identity restriction groupoid is contained in $G$ (i.e., $idRestrGroupoid \leq G$).

instClosedUnderRestrictionContinuousGroupoid instance

: ClosedUnderRestriction (continuousGroupoid H)

Full source

/-- The groupoid of all partial homeomorphisms on a topological space `H`
is closed under restriction. -/
instance : ClosedUnderRestriction (continuousGroupoid H) :=
  (closedUnderRestriction_iff_id_le _).mpr le_top

Restriction-Closed Property of the Continuous Groupoid

Informal description

The continuous groupoid on a topological space $H$, consisting of all partial homeomorphisms of $H$, is closed under restriction. That is, for any partial homeomorphism $e$ in this groupoid and any open subset $s$ of the source of $e$, the restriction of $e$ to $s$ also belongs to the groupoid.

ChartedSpace structure

(H : Type*) [TopologicalSpace H] (M : Type*) [TopologicalSpace M]

Full source

/-- 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)`.
-/
@[ext]
class ChartedSpace (H : Type*) [TopologicalSpace H] (M : Type*) [TopologicalSpace M] where
  /-- The atlas of charts in the `ChartedSpace`. -/
  protected atlas : Set (PartialHomeomorph M H)
  /-- The preferred chart at each point in the charted space. -/
  protected chartAt : M → PartialHomeomorph M H
  protected mem_chart_source : ∀ x, x ∈ (chartAt x).source
  protected chart_mem_atlas : ∀ x, chartAt x ∈ atlas

Charted space

Informal description

A charted space structure on a topological space $M$ modeled on a topological space $H$ consists of a collection of local homeomorphisms (called charts) from open subsets of $M$ to $H$, such that the domains of the charts cover $M$. For each point $x \in M$, there is a preferred chart `chartAt x` containing $x$ in its domain.

atlas abbrev

(H : Type*) [TopologicalSpace H] (M : Type*) [TopologicalSpace M] [ChartedSpace H M] : Set (PartialHomeomorph M H)

Full source

/-- The atlas of charts in a `ChartedSpace`. -/
abbrev atlas (H : Type*) [TopologicalSpace H] (M : Type*) [TopologicalSpace M]
    [ChartedSpace H M] : Set (PartialHomeomorph M H) :=
  ChartedSpace.atlas

Atlas of a Charted Space

Informal description

Given a charted space $M$ modeled on a topological space $H$, the atlas is the set of all partial homeomorphisms (charts) from open subsets of $M$ to $H$ that cover $M$.

chartAt abbrev

(H : Type*) [TopologicalSpace H] {M : Type*} [TopologicalSpace M] [ChartedSpace H M] (x : M) : PartialHomeomorph M H

Full source

/-- The preferred chart at a point `x` in a charted space `M`. -/
abbrev chartAt (H : Type*) [TopologicalSpace H] {M : Type*} [TopologicalSpace M]
    [ChartedSpace H M] (x : M) : PartialHomeomorph M H :=
  ChartedSpace.chartAt x

Preferred Chart at a Point in a Charted Space

Informal description

Given a charted space $M$ modeled on a topological space $H$, the function $\text{chartAt}_H(x)$ returns a preferred partial homeomorphism (chart) from an open neighborhood of $x \in M$ to $H$, such that $x$ is contained in the source of this chart.

mem_chart_source theorem

 (H : Type*) {M : Type*} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) : x ∈ (chartAt H x).source

Full source

@[simp, mfld_simps]
lemma mem_chart_source (H : Type*) {M : Type*} [TopologicalSpace H] [TopologicalSpace M]
    [ChartedSpace H M] (x : M) : x ∈ (chartAt H x).source :=
  ChartedSpace.mem_chart_source x

Point Belongs to Source of Preferred Chart in Charted Space

Informal description

For any point $x$ in a charted space $M$ modeled on a topological space $H$, the point $x$ belongs to the source of its preferred chart $\text{chartAt}_H(x)$.

chart_mem_atlas theorem

 (H : Type*) {M : Type*} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) : chartAt H x ∈ atlas H M

Full source

@[simp, mfld_simps]
lemma chart_mem_atlas (H : Type*) {M : Type*} [TopologicalSpace H] [TopologicalSpace M]
    [ChartedSpace H M] (x : M) : chartAtchartAt H x ∈ atlas H M :=
  ChartedSpace.chart_mem_atlas x

Preferred Chart Belongs to Atlas in Charted Space

Informal description

For any point $x$ in a charted space $M$ modeled on a topological space $H$, the preferred chart $\text{chartAt}_H(x)$ at $x$ belongs to the atlas of $M$.

nonempty_of_chartedSpace theorem

{H : Type*} {M : Type*} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (x : M) : Nonempty H

Full source

lemma nonempty_of_chartedSpace {H : Type*} {M : Type*} [TopologicalSpace H] [TopologicalSpace M]
    [ChartedSpace H M] (x : M) : Nonempty H :=
  ⟨chartAt H x x⟩

Nonemptiness of Model Space in Charted Spaces

Informal description

For any charted space $M$ modeled on a topological space $H$, and for any point $x \in M$, the model space $H$ is nonempty.

isEmpty_of_chartedSpace theorem

(H : Type*) {M : Type*} [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] [IsEmpty H] : IsEmpty M

Full source

lemma isEmpty_of_chartedSpace (H : Type*) {M : Type*} [TopologicalSpace H] [TopologicalSpace M]
    [ChartedSpace H M] [IsEmpty H] : IsEmpty M := by
  rcases isEmpty_or_nonempty M with hM | ⟨⟨x⟩⟩
  · exact hM
  · exact (IsEmpty.false (chartAt H x x)).elim

Emptiness of Charted Space with Empty Model Space

Informal description

If $M$ is a charted space modeled on a topological space $H$ and $H$ is empty, then $M$ is also empty.

mem_chart_target theorem

(x : M) : chartAt H x x ∈ (chartAt H x).target

Full source

theorem mem_chart_target (x : M) : chartAtchartAt H x x ∈ (chartAt H x).target :=
  (chartAt H x).map_source (mem_chart_source _ _)

Image of Point under Preferred Chart Lies in Target

Informal description

For any point $x$ in a charted space $M$ modeled on a topological space $H$, the image of $x$ under its preferred chart $\text{chartAt}_H(x)$ belongs to the target set of the chart.

chart_source_mem_nhds theorem

(x : M) : (chartAt H x).source ∈ 𝓝 x

Full source

theorem chart_source_mem_nhds (x : M) : (chartAt H x).source ∈ 𝓝 x :=
  (chartAt H x).open_source.mem_nhds <| mem_chart_source H x

Preferred Chart Source is a Neighborhood of the Point

Informal description

For any point $x$ in a charted space $M$ modeled on a topological space $H$, the source of the preferred chart $\text{chartAt}_H(x)$ is a neighborhood of $x$ in $M$.

chart_target_mem_nhds theorem

(x : M) : (chartAt H x).target ∈ 𝓝 (chartAt H x x)

Full source

theorem chart_target_mem_nhds (x : M) : (chartAt H x).target ∈ 𝓝 (chartAt H x x) :=
  (chartAt H x).open_target.mem_nhds <| mem_chart_target H x

Target of Preferred Chart is a Neighborhood of its Image Point

Informal description

For any point $x$ in a charted space $M$ modeled on a topological space $H$, the target set of the preferred chart $\text{chartAt}_H(x)$ is a neighborhood of the image point $\text{chartAt}_H(x)(x)$ in $H$.

iUnion_source_chartAt theorem

: (⋃ x : M, (chartAt H x).source) = (univ : Set M)

Full source

@[simp]
theorem iUnion_source_chartAt : (⋃ x : M, (chartAt H x).source) = (univ : Set M) :=
  eq_univ_iff_forall.mpr fun x ↦ mem_iUnion.mpr ⟨x, mem_chart_source H x⟩

Union of Chart Sources Covers the Space

Informal description

The union of the sources of all preferred charts in a charted space $M$ modeled on a topological space $H$ is equal to the entire space $M$, i.e., \[ \bigcup_{x \in M} (\text{chartAt}_H(x)).\text{source} = M. \]

ChartedSpace.isOpen_iff theorem

(s : Set M) : IsOpen s ↔ ∀ x : M, IsOpen <| chartAt H x '' ((chartAt H x).source ∩ s)

Full source

theorem ChartedSpace.isOpen_iff (s : Set M) :
    IsOpenIsOpen s ↔ ∀ x : M, IsOpen <| chartAt H x '' ((chartAt H x).source ∩ s) := by
  rw [isOpen_iff_of_cover (fun i ↦ (chartAt H i).open_source) (iUnion_source_chartAt H M)]
  simp only [(chartAt H _).isOpen_image_iff_of_subset_source inter_subset_left]

Openness Criterion for Charted Spaces via Preferred Charts

Informal description

A subset $s$ of a charted space $M$ modeled on a topological space $H$ is open if and only if for every point $x \in M$, the image of the intersection of $s$ with the source of the preferred chart at $x$ under this chart is open in $H$. In other words, \[ \text{IsOpen}(s) \leftrightarrow \forall x \in M, \text{IsOpen}\left(\text{chartAt}_H(x)((\text{chartAt}_H(x).\text{source} \cap s)\right). \]

achart definition

(x : M) : atlas H M

Full source

/-- `achart H x` is the chart at `x`, considered as an element of the atlas.
Especially useful for working with `BasicContMDiffVectorBundleCore`. -/
def achart (x : M) : atlas H M :=
  ⟨chartAt H x, chart_mem_atlas H x⟩

Atlas element of preferred chart at a point

Informal description

Given a charted space $M$ modeled on a topological space $H$, the function $\text{achart}_H(x)$ returns the preferred chart at $x \in M$ as an element of the atlas of $M$. Specifically, it pairs the chart $\text{chartAt}_H(x)$ with a proof that this chart belongs to the atlas.

achart_def theorem

(x : M) : achart H x = ⟨chartAt H x, chart_mem_atlas H x⟩

Full source

theorem achart_def (x : M) : achart H x = ⟨chartAt H x, chart_mem_atlas H x⟩ :=
  rfl

Definition of Preferred Chart Element in Atlas

Informal description

For any point $x$ in a charted space $M$ modeled on a topological space $H$, the preferred chart element $\text{achart}_H(x)$ in the atlas is equal to the pair consisting of the preferred chart $\text{chartAt}_H(x)$ and a proof that this chart belongs to the atlas of $M$.

coe_achart theorem

(x : M) : (achart H x : PartialHomeomorph M H) = chartAt H x

Full source

@[simp, mfld_simps]
theorem coe_achart (x : M) : (achart H x : PartialHomeomorph M H) = chartAt H x :=
  rfl

Preferred Chart as Partial Homeomorphism: $\text{achart}_H(x) = \text{chartAt}_H(x)$

Informal description

For any point $x$ in a charted space $M$ modeled on a topological space $H$, the preferred chart $\text{achart}_H(x)$ (viewed as a partial homeomorphism) is equal to the chart $\text{chartAt}_H(x)$ at $x$.

achart_val theorem

(x : M) : (achart H x).1 = chartAt H x

Full source

@[simp, mfld_simps]
theorem achart_val (x : M) : (achart H x).1 = chartAt H x :=
  rfl

Preferred Chart Element Projection: $(\text{achart}_H(x)).1 = \text{chartAt}_H(x)$

Informal description

For any point $x$ in a charted space $M$ modeled on a topological space $H$, the first projection of the preferred chart element $\text{achart}_H(x)$ (which is a pair consisting of a chart and a proof) is equal to the preferred chart $\text{chartAt}_H(x)$ at $x$.

mem_achart_source theorem

(x : M) : x ∈ (achart H x).1.source

Full source

theorem mem_achart_source (x : M) : x ∈ (achart H x).1.source :=
  mem_chart_source H x

Point Belongs to Source of Preferred Chart in Charted Space

Informal description

For any point $x$ in a charted space $M$ modeled on a topological space $H$, the point $x$ belongs to the source of the preferred chart $\text{achart}_H(x)$.

ChartedSpace.secondCountable_of_countable_cover theorem

 [SecondCountableTopology H] {s : Set M} (hs : ⋃ (x) (_ : x ∈ s), (chartAt H x).source = univ) (hsc : s.Countable) :
  SecondCountableTopology M

Full source

theorem ChartedSpace.secondCountable_of_countable_cover [SecondCountableTopology H] {s : Set M}
    (hs : ⋃ (x) (_ : x ∈ s), (chartAt H x).source = univ) (hsc : s.Countable) :
    SecondCountableTopology M := by
  haveI : ∀ x : M, SecondCountableTopology (chartAt H x).source :=
    fun x ↦ (chartAt (H := H) x).secondCountableTopology_source
  haveI := hsc.toEncodable
  rw [biUnion_eq_iUnion] at hs
  exact secondCountableTopology_of_countable_cover (fun x : s ↦ (chartAt H (x : M)).open_source) hs

Second-Countability of Charted Spaces via Countable Cover of Chart Sources

Informal description

Let $M$ be a charted space modeled on a second-countable topological space $H$. Suppose there exists a countable set $s \subset M$ such that the union of the sources of the preferred charts $\text{chartAt}_H(x)$ for all $x \in s$ covers $M$. Then $M$ is second-countable.

ChartedSpace.secondCountable_of_sigmaCompact theorem

[SecondCountableTopology H] [SigmaCompactSpace M] : SecondCountableTopology M

Full source

theorem ChartedSpace.secondCountable_of_sigmaCompact [SecondCountableTopology H]
    [SigmaCompactSpace M] : SecondCountableTopology M := by
  obtain ⟨s, hsc, hsU⟩ : ∃ s, Set.Countable s ∧ ⋃ (x) (_ : x ∈ s), (chartAt H x).source = univ :=
    countable_cover_nhds_of_sigmaCompact fun x : M ↦ chart_source_mem_nhds H x
  exact ChartedSpace.secondCountable_of_countable_cover H hsU hsc

Second-countability of $\sigma$-compact charted spaces

Informal description

Let $M$ be a $\sigma$-compact charted space modeled on a second-countable topological space $H$. Then $M$ is second-countable.

ChartedSpace.locallyCompactSpace theorem

[LocallyCompactSpace H] : LocallyCompactSpace M

Full source

/-- If a topological space admits an atlas with locally compact charts, then the space itself
is locally compact. -/
theorem ChartedSpace.locallyCompactSpace [LocallyCompactSpace H] : LocallyCompactSpace M := by
  have : ∀ x : M, (𝓝 x).HasBasis
      (fun s ↦ s ∈ 𝓝 (chartAt H x x)s ∈ 𝓝 (chartAt H x x) ∧ IsCompact s ∧ s ⊆ (chartAt H x).target)
      fun s ↦ (chartAt H x).symm '' s := fun x ↦ by
    rw [← (chartAt H x).symm_map_nhds_eq (mem_chart_source H x)]
    exact ((compact_basis_nhds (chartAt H x x)).hasBasis_self_subset
      (chart_target_mem_nhds H x)).map _
  refine .of_hasBasis this ?_
  rintro x s ⟨_, h₂, h₃⟩
  exact h₂.image_of_continuousOn ((chartAt H x).continuousOn_symm.mono h₃)

Local Compactness of Charted Spaces Modeled on Locally Compact Spaces

Informal description

If a charted space $M$ is modeled on a locally compact topological space $H$, then $M$ itself is locally compact.

ChartedSpace.locallyConnectedSpace theorem

[LocallyConnectedSpace H] : LocallyConnectedSpace M

Full source

/-- If a topological space admits an atlas with locally connected charts, then the space itself is
locally connected. -/
theorem ChartedSpace.locallyConnectedSpace [LocallyConnectedSpace H] : LocallyConnectedSpace M := by
  let e : M → PartialHomeomorph M H := chartAt H
  refine locallyConnectedSpace_of_connected_bases (fun x s ↦ (e x).symm '' s)
      (fun x s ↦ (IsOpen s ∧ e x x ∈ s ∧ IsConnected s) ∧ s ⊆ (e x).target) ?_ ?_
  · intro x
    simpa only [e, PartialHomeomorph.symm_map_nhds_eq, mem_chart_source] using
      ((LocallyConnectedSpace.open_connected_basis (e x x)).restrict_subset
        ((e x).open_target.mem_nhds (mem_chart_target H x))).map (e x).symm
  · rintro x s ⟨⟨-, -, hsconn⟩, hssubset⟩
    exact hsconn.isPreconnected.image _ ((e x).continuousOn_symm.mono hssubset)

Local Connectedness of Charted Spaces Modeled on Locally Connected Spaces

Informal description

If a charted space $M$ is modeled on a locally connected topological space $H$, then $M$ itself is locally connected.

ChartedSpace.locPathConnectedSpace theorem

[LocPathConnectedSpace H] : LocPathConnectedSpace M

Full source

/-- If a topological space `M` admits an atlas with locally path-connected charts,
then `M` itself is locally path-connected. -/
theorem ChartedSpace.locPathConnectedSpace [LocPathConnectedSpace H] : LocPathConnectedSpace M := by
  refine ⟨fun x ↦ ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨u, hu⟩ ↦ Filter.mem_of_superset hu.1.1 hu.2⟩⟩⟩
  let e := chartAt H x
  let t := s ∩ e.source
  have ht : t ∈ 𝓝 x := Filter.inter_mem hs (chart_source_mem_nhds _ _)
  refine ⟨e.symm '' pathComponentIn (e x) (e '' t), ⟨?_, ?_⟩, (?_ : _ ⊆ t).trans inter_subset_left⟩
  · nth_rewrite 1 [← e.left_inv (mem_chart_source _ _)]
    apply e.symm.image_mem_nhds (by simp [e])
    exact pathComponentIn_mem_nhds <| e.image_mem_nhds (mem_chart_source _ _) ht
  · refine (isPathConnected_pathComponentIn <| mem_image_of_mem e (mem_of_mem_nhds ht)).image' ?_
    refine e.continuousOn_symm.mono <| subset_trans ?_ e.map_source''
    exact (pathComponentIn_mono <| image_mono inter_subset_right).trans pathComponentIn_subset
  · exact (image_mono pathComponentIn_subset).trans
      (PartialEquiv.symm_image_image_of_subset_source _ inter_subset_right).subset

Local Path-Connectedness of Charted Spaces Modeled on Locally Path-Connected Spaces

Informal description

If a charted space $M$ is modeled on a locally path-connected topological space $H$, then $M$ itself is locally path-connected.

ChartedSpace.comp definition

 (H : Type*) [TopologicalSpace H] (H' : Type*) [TopologicalSpace H'] (M : Type*) [TopologicalSpace M]
  [ChartedSpace H H'] [ChartedSpace H' M] : ChartedSpace H M

Full source

/-- If `M` is modelled on `H'` and `H'` is itself modelled on `H`, then we can consider `M` as being
modelled on `H`. -/
def ChartedSpace.comp (H : Type*) [TopologicalSpace H] (H' : Type*) [TopologicalSpace H']
    (M : Type*) [TopologicalSpace M] [ChartedSpace H H'] [ChartedSpace H' M] :
    ChartedSpace H M where
  atlas := image2 PartialHomeomorph.trans (atlas H' M) (atlas H H')
  chartAt p := (chartAt H' p).trans (chartAt H (chartAt H' p p))
  mem_chart_source p := by simp only [mfld_simps]
  chart_mem_atlas p := ⟨chartAt _ p, chart_mem_atlas _ p, chartAt _ _, chart_mem_atlas _ _, rfl⟩

Composition of charted spaces

Informal description

Given topological spaces $H$, $H'$, and $M$, if $M$ is a charted space modeled on $H'$ and $H'$ is itself a charted space modeled on $H$, then $M$ inherits a charted space structure modeled directly on $H$. The atlas for this structure consists of all possible compositions of charts from $M$ to $H'$ with charts from $H'$ to $H$. For each point $p \in M$, the preferred chart is given by composing the preferred chart of $p$ in $H'$ with the preferred chart of its image in $H$.

chartAt_comp theorem

 (H : Type*) [TopologicalSpace H] (H' : Type*) [TopologicalSpace H'] {M : Type*} [TopologicalSpace M]
  [ChartedSpace H H'] [ChartedSpace H' M] (x : M) :
  (letI := ChartedSpace.comp H H' M;
    chartAt H x) =
    chartAt H' x ≫ₕ chartAt H (chartAt H' x x)

Full source

theorem chartAt_comp (H : Type*) [TopologicalSpace H] (H' : Type*) [TopologicalSpace H']
    {M : Type*} [TopologicalSpace M] [ChartedSpace H H'] [ChartedSpace H' M] (x : M) :
    (letI := ChartedSpace.comp H H' M; chartAt H x) = chartAtchartAt H' x ≫ₕ chartAt H (chartAt H' x x) :=
  rfl

Composition Rule for Preferred Charts in Charted Spaces

Informal description

Let $H$ and $H'$ be topological spaces, and let $M$ be a topological space equipped with a charted space structure modeled on $H'$, where $H'$ itself has a charted space structure modeled on $H$. For any point $x \in M$, the preferred chart at $x$ in the composed charted space structure (modeled directly on $H$) is equal to the composition of the preferred chart at $x$ in $H'$ with the preferred chart at the image of $x$ in $H'$. In other words, under the composition of charted spaces, we have: \[ \text{chartAt}_H(x) = \text{chartAt}_{H'}(x) \circ \text{chartAt}_H(\text{chartAt}_{H'}(x)(x)) \]

ChartedSpace.t1Space theorem

[T1Space H] : T1Space M

Full source

/-- 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.t1Space [T1Space H] : T1Space M := by
  apply t1Space_iff_exists_open.2 (fun x y hxy ↦ ?_)
  by_cases hy : y ∈ (chartAt H x).source
  · refine ⟨(chartAt H x).source ∩ (chartAt H x)⁻¹' ({chartAt H x y}ᶜ), ?_, ?_, by simp⟩
    · exact PartialHomeomorph.isOpen_inter_preimage _ isOpen_compl_singleton
    · simp only [preimage_compl, mem_inter_iff, mem_chart_source, mem_compl_iff, mem_preimage,
        mem_singleton_iff, true_and]
      exact (chartAt H x).injOn.ne (ChartedSpace.mem_chart_source x) hy hxy
  · exact ⟨(chartAt H x).source, (chartAt H x).open_source, ChartedSpace.mem_chart_source x, hy⟩

T₁ Property of Charted Spaces Modeled on T₁ Spaces

Informal description

If $H$ is a T₁ space and $M$ is a charted space modeled on $H$, then $M$ is also a T₁ space.

ChartedSpace.discreteTopology theorem

[DiscreteTopology H] : DiscreteTopology M

Full source

/-- A charted space over a discrete space is discrete. -/
theorem ChartedSpace.discreteTopology [DiscreteTopology H] : DiscreteTopology M := by
  apply singletons_open_iff_discrete.1 (fun x ↦ ?_)
  have : IsOpen ((chartAt H x).source ∩ (chartAt H x) ⁻¹' {chartAt H x x}) :=
    isOpen_inter_preimage _ (isOpen_discrete _)
  convert this
  refine Subset.antisymm (by simp) ?_
  simp only [subset_singleton_iff, mem_inter_iff, mem_preimage, mem_singleton_iff, and_imp]
  intro y hy h'y
  exact (chartAt H x).injOn hy (mem_chart_source _ x) h'y

Discrete Model Space Implies Discrete Topology on Charted Space

Informal description

If a charted space $M$ is modeled on a topological space $H$ with the discrete topology, then $M$ itself has the discrete topology.

ChartedSpace.empty definition

(H : Type*) [TopologicalSpace H] (M : Type*) [TopologicalSpace M] [IsEmpty M] : ChartedSpace H M

Full source

/-- An empty type is a charted space over any topological space. -/
def ChartedSpace.empty (H : Type*) [TopologicalSpace H]
    (M : Type*) [TopologicalSpace M] [IsEmpty M] : ChartedSpace H M where
  atlas := ∅
  chartAt x := (IsEmpty.false x).elim
  mem_chart_source x := (IsEmpty.false x).elim
  chart_mem_atlas x := (IsEmpty.false x).elim

Charted space structure on an empty space

Informal description

For any topological space $H$ and any empty topological space $M$, there exists a charted space structure on $M$ modeled on $H$ with an empty atlas. The preferred chart at any point $x \in M$ is not defined (since $M$ is empty).

chartedSpaceSelf instance

(H : Type*) [TopologicalSpace H] : ChartedSpace H H

Full source

/-- Any space is a `ChartedSpace` modelled over itself, by just using the identity chart. -/
instance chartedSpaceSelf (H : Type*) [TopologicalSpace H] : ChartedSpace H H where
  atlas := {PartialHomeomorph.refl H}
  chartAt _ := PartialHomeomorph.refl H
  mem_chart_source x := mem_univ x
  chart_mem_atlas _ := mem_singleton _

Canonical Charted Space Structure on a Topological Space

Informal description

For any topological space $H$, there is a canonical charted space structure on $H$ where the model space is $H$ itself, with the identity map as the only chart. This means the atlas consists solely of the identity partial homeomorphism on $H$, and for any point $x \in H$, the preferred chart at $x$ is the identity map.

chartedSpaceSelf_atlas theorem

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

Full source

/-- In the trivial `ChartedSpace` structure of a space modelled over itself through the identity,
the atlas members are just the identity. -/
@[simp, mfld_simps]
theorem chartedSpaceSelf_atlas {H : Type*} [TopologicalSpace H] {e : PartialHomeomorph H H} :
    e ∈ atlas H He ∈ atlas H H ↔ e = PartialHomeomorph.refl H :=
  Iff.rfl

Atlas in Canonical Charted Space Structure Consists Only of Identity

Informal description

For any topological space $H$, a partial homeomorphism $e$ from $H$ to itself belongs to the atlas of the canonical charted space structure on $H$ if and only if $e$ is the identity partial homeomorphism on $H$.

chartAt_self_eq theorem

{H : Type*} [TopologicalSpace H] {x : H} : chartAt H x = PartialHomeomorph.refl H

Full source

/-- In the model space, `chartAt` is always the identity. -/
theorem chartAt_self_eq {H : Type*} [TopologicalSpace H] {x : H} :
    chartAt H x = PartialHomeomorph.refl H := rfl

Preferred Chart is Identity in Canonical Charted Space

Informal description

For any topological space $H$ and any point $x \in H$, the preferred chart at $x$ in the canonical charted space structure on $H$ is equal to the identity partial homeomorphism on $H$.

ChartedSpace.of_discreteTopology definition

[TopologicalSpace M] [TopologicalSpace H] [DiscreteTopology M] [h : Unique H] : ChartedSpace H M

Full source

/-- 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.
-/
def ChartedSpace.of_discreteTopology [TopologicalSpace M] [TopologicalSpace H]
    [DiscreteTopology M] [h : Unique H] : ChartedSpace H M where
  atlas :=
    letI f := fun x : M ↦ PartialHomeomorph.const
      (isOpen_discrete {x}) (isOpen_discrete {h.default})
    Set.image f univ
  chartAt x := PartialHomeomorph.const (isOpen_discrete {x}) (isOpen_discrete {h.default})
  mem_chart_source x := by simp
  chart_mem_atlas x := by simp

Charted space structure on a discrete space modeled on a singleton

Informal description

Given a topological space $M$ with the discrete topology and a topological space $H$ with a unique element, the charted space structure on $M$ modeled on $H$ is defined as follows: - The atlas consists of all constant partial homeomorphisms mapping each singleton $\{x\}$ (which is open in $M$) to the singleton $\{h.\text{default}\}$ (which is open in $H$), where $h.\text{default}$ is the unique element of $H$. - The preferred chart at any point $x \in M$ is the constant partial homeomorphism from $\{x\}$ to $\{h.\text{default}\}$.

chartedSpace_of_discreteTopology_chartAt theorem

 [TopologicalSpace M] [TopologicalSpace H] [DiscreteTopology M] [h : Unique H] {x : M} :
  haveI := ChartedSpace.of_discreteTopology (M := M) (H := H)
  chartAt H x = PartialHomeomorph.const (isOpen_discrete { x }) (isOpen_discrete { h.default })

Full source

/-- A chart on the discrete space is the constant chart. -/
@[simp, mfld_simps]
lemma chartedSpace_of_discreteTopology_chartAt [TopologicalSpace M] [TopologicalSpace H]
    [DiscreteTopology M] [h : Unique H] {x : M} :
    haveI := ChartedSpace.of_discreteTopology (M := M) (H := H)
    chartAt H x = PartialHomeomorph.const (isOpen_discrete {x}) (isOpen_discrete {h.default}) :=
  rfl

Preferred Chart on Discrete Space is Constant Map to Singleton

Informal description

Let $M$ be a topological space with the discrete topology and $H$ be a topological space with a unique element. Then, for any point $x \in M$, the preferred chart $\text{chartAt}_H(x)$ is equal to the constant partial homeomorphism mapping the singleton $\{x\}$ (which is open in $M$) to the singleton $\{h\}$ (which is open in $H$), where $h$ is the unique element of $H$.

ModelProd definition

(H : Type*) (H' : Type*)

Full source

/-- Same thing as `H × H'`. We introduce it for technical reasons,
see note [Manifold type tags]. -/
def ModelProd (H : Type*) (H' : Type*) :=
  H × H'

Product model space

Informal description

The type `ModelProd H H'` is defined as the product type `H × H'`, introduced for technical reasons related to manifold type tags.

ModelPi definition

{ι : Type*} (H : ι → Type*)

Full source

/-- Same thing as `∀ i, H i`. We introduce it for technical reasons,
see note [Manifold type tags]. -/
def ModelPi {ι : Type*} (H : ι → Type*) :=
  ∀ i, H i

Product model space

Informal description

Given an index type $\iota$ and a family of types $H_i$ indexed by $\iota$, the type `ModelPi` represents the product space $\prod_{i \in \iota} H_i$. This construction is introduced for technical reasons related to manifold type tags.

modelProdInhabited instance

[Inhabited H] [Inhabited H'] : Inhabited (ModelProd H H')

Full source

instance modelProdInhabited [Inhabited H] [Inhabited H'] : Inhabited (ModelProd H H') :=
  instInhabitedProd

Inhabited Product Model Space

Informal description

For any inhabited types $H$ and $H'$, the product model space $\text{ModelProd}\, H\, H'$ is also inhabited.

instTopologicalSpaceModelProd instance

(H : Type*) [TopologicalSpace H] (H' : Type*) [TopologicalSpace H'] : TopologicalSpace (ModelProd H H')

Full source

instance (H : Type*) [TopologicalSpace H] (H' : Type*) [TopologicalSpace H'] :
    TopologicalSpace (ModelProd H H') :=
  instTopologicalSpaceProd

Product Topology on Model Product Space

Informal description

For any topological spaces $H$ and $H'$, the product model space $\text{ModelProd}\, H\, H'$ (which is equivalent to $H \times H'$) is equipped with the canonical product topology.

modelProd_range_prod_id theorem

 {H : Type*} {H' : Type*} {α : Type*} (f : H → α) :
  (range fun p : ModelProd H H' ↦ (f p.1, p.2)) = range f ×ˢ (univ : Set H')

Full source

@[simp, mfld_simps]
theorem modelProd_range_prod_id {H : Type*} {H' : Type*} {α : Type*} (f : H → α) :
    (range fun p : ModelProd H H' ↦ (f p.1, p.2)) = range f ×ˢ (univ : Set H') := by
  rw [prod_range_univ_eq]
  rfl

Range of Paired Function Equals Product of Range with Universal Set

Informal description

For any function $f \colon H \to \alpha$, the range of the function $\lambda p \colon H \times H' \mapsto (f(p_1), p_2)$ is equal to the Cartesian product of the range of $f$ with the universal set on $H'$. In other words: \[ \text{range}(\lambda p \mapsto (f(p_1), p_2)) = \text{range}(f) \times H' \]

modelPiInhabited instance

[∀ i, Inhabited (Hi i)] : Inhabited (ModelPi Hi)

Full source

instance modelPiInhabited [∀ i, Inhabited (Hi i)] : Inhabited (ModelPi Hi) :=
  Pi.instInhabited

Inhabited Product of Inhabited Spaces

Informal description

For any family of inhabited types $(H_i)_{i \in \iota}$, the product space $\prod_{i \in \iota} H_i$ is also inhabited.

instTopologicalSpaceModelPi instance

[∀ i, TopologicalSpace (Hi i)] : TopologicalSpace (ModelPi Hi)

Full source

instance [∀ i, TopologicalSpace (Hi i)] : TopologicalSpace (ModelPi Hi) :=
  Pi.topologicalSpace

Product Topology on Model Spaces

Informal description

For any family of topological spaces $(H_i)_{i \in \iota}$ indexed by a type $\iota$, the product space $\prod_{i \in \iota} H_i$ is equipped with the product topology, where a subset is open if and only if it is a union of sets of the form $\prod_{i \in \iota} U_i$ with each $U_i$ open in $H_i$ and $U_i = H_i$ for all but finitely many $i$.

prodChartedSpace instance

 (H : Type*) [TopologicalSpace H] (M : Type*) [TopologicalSpace M] [ChartedSpace H M] (H' : Type*) [TopologicalSpace H']
  (M' : Type*) [TopologicalSpace M'] [ChartedSpace H' M'] : ChartedSpace (ModelProd H H') (M × M')

Full source

/-- The product of two charted spaces is naturally a charted space, with the canonical
construction of the atlas of product maps. -/
instance prodChartedSpace (H : Type*) [TopologicalSpace H] (M : Type*) [TopologicalSpace M]
    [ChartedSpace H M] (H' : Type*) [TopologicalSpace H'] (M' : Type*) [TopologicalSpace M']
    [ChartedSpace H' M'] : ChartedSpace (ModelProd H H') (M × M') where
  atlas := image2 PartialHomeomorph.prod (atlas H M) (atlas H' M')
  chartAt x := (chartAt H x.1).prod (chartAt H' x.2)
  mem_chart_source x := ⟨mem_chart_source H x.1, mem_chart_source H' x.2⟩
  chart_mem_atlas x := mem_image2_of_mem (chart_mem_atlas H x.1) (chart_mem_atlas H' x.2)

Product of Charted Spaces as a Charted Space

Informal description

For any topological spaces $H$ and $H'$, and any charted spaces $M$ modeled on $H$ and $M'$ modeled on $H'$, the product space $M \times M'$ is naturally a charted space modeled on the product model space $H \times H'$. The charts are given by the products of charts from $M$ and $M'$, where for each point $(x, y) \in M \times M'$, the chart at $(x, y)$ is the product of the preferred charts at $x$ and $y$.

ModelProd.ext theorem

{x y : ModelProd H H'} (h₁ : x.1 = y.1) (h₂ : x.2 = y.2) : x = y

Full source

@[ext]
theorem ModelProd.ext {x y : ModelProd H H'} (h₁ : x.1 = y.1) (h₂ : x.2 = y.2) : x = y :=
  Prod.ext h₁ h₂

Extensionality of Product Model Space

Informal description

Let $x$ and $y$ be elements of the product model space $\text{ModelProd}\, H\, H'$. If the first components are equal ($x.1 = y.1$) and the second components are equal ($x.2 = y.2$), then $x = y$.

prodChartedSpace_chartAt theorem

: chartAt (ModelProd H H') x = (chartAt H x.fst).prod (chartAt H' x.snd)

Full source

@[simp, mfld_simps]
theorem prodChartedSpace_chartAt :
    chartAt (ModelProd H H') x = (chartAt H x.fst).prod (chartAt H' x.snd) :=
  rfl

Preferred Chart at a Point in a Product Charted Space is the Product of Charts

Informal description

For any charted spaces $M$ and $M'$ modeled on topological spaces $H$ and $H'$ respectively, the preferred chart at a point $(x, y) \in M \times M'$ in the product charted space is equal to the product of the preferred charts at $x \in M$ and $y \in M'$. More precisely, if $\text{chartAt}_H(x)$ is the preferred chart at $x$ in $M$ and $\text{chartAt}_{H'}(y)$ is the preferred chart at $y$ in $M'$, then the preferred chart at $(x, y)$ in $M \times M'$ is given by their product $\text{chartAt}_H(x) \times \text{chartAt}_{H'}(y)$.

chartedSpaceSelf_prod theorem

: prodChartedSpace H H H' H' = chartedSpaceSelf (H × H')

Full source

theorem chartedSpaceSelf_prod : prodChartedSpace H H H' H' = chartedSpaceSelf (H × H') := by
  ext1
  · simp [prodChartedSpace, atlas, ChartedSpace.atlas]
  · ext1
    simp only [prodChartedSpace_chartAt, chartAt_self_eq, refl_prod_refl]
    rfl

Product of Canonical Charted Spaces Equals Canonical Charted Space on Product

Informal description

The product charted space structure on $H \times H'$, where both factors are equipped with their canonical charted space structures, is equal to the canonical charted space structure on the product space $H \times H'$.

piChartedSpace instance

 {ι : Type*} [Finite ι] (H : ι → Type*) [∀ i, TopologicalSpace (H i)] (M : ι → Type*) [∀ i, TopologicalSpace (M i)]
  [∀ i, ChartedSpace (H i) (M i)] : ChartedSpace (ModelPi H) (∀ i, M i)

Full source

/-- 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. -/
instance piChartedSpace {ι : Type*} [Finite ι] (H : ι → Type*) [∀ i, TopologicalSpace (H i)]
    (M : ι → Type*) [∀ i, TopologicalSpace (M i)] [∀ i, ChartedSpace (H i) (M i)] :
    ChartedSpace (ModelPi H) (∀ i, M i) where
  atlas := PartialHomeomorph.piPartialHomeomorph.pi '' Set.pi univ fun _ ↦ atlas (H _) (M _)
  chartAt f := PartialHomeomorph.pi fun i ↦ chartAt (H i) (f i)
  mem_chart_source f i _ := mem_chart_source (H i) (f i)
  chart_mem_atlas f := mem_image_of_mem _ fun i _ ↦ chart_mem_atlas (H i) (f i)

Product of Charted Spaces

Informal description

For a finite index set $\iota$ and a family of charted spaces $M_i$ modeled on topological spaces $H_i$, the product space $\prod_{i \in \iota} M_i$ is naturally a charted space modeled on the product space $\prod_{i \in \iota} H_i$. The atlas consists of the product charts formed by taking the product of the charts from each $M_i$.

piChartedSpace_chartAt theorem

 {ι : Type*} [Finite ι] (H : ι → Type*) [∀ i, TopologicalSpace (H i)] (M : ι → Type*) [∀ i, TopologicalSpace (M i)]
  [∀ i, ChartedSpace (H i) (M i)] (f : ∀ i, M i) :
  chartAt (H := ModelPi H) f = PartialHomeomorph.pi fun i ↦ chartAt (H i) (f i)

Full source

@[simp, mfld_simps]
theorem piChartedSpace_chartAt {ι : Type*} [Finite ι] (H : ι → Type*)
    [∀ i, TopologicalSpace (H i)] (M : ι → Type*) [∀ i, TopologicalSpace (M i)]
    [∀ i, ChartedSpace (H i) (M i)] (f : ∀ i, M i) :
    chartAt (H := ModelPi H) f = PartialHomeomorph.pi fun i ↦ chartAt (H i) (f i) :=
  rfl

Preferred Chart in Product Charted Space as Product of Charts

Informal description

For a finite index set $\iota$ and a family of charted spaces $M_i$ modeled on topological spaces $H_i$, the preferred chart at a point $f \in \prod_{i \in \iota} M_i$ in the product charted space is given by the product of the preferred charts at each component $f(i) \in M_i$. More precisely, if $\text{chartAt}_{H_i}(f(i))$ denotes the preferred chart at $f(i)$ in $M_i$, then the chart at $f$ in the product space is: \[ \text{chartAt}_{\prod_i H_i}(f) = \prod_{i \in \iota} \text{chartAt}_{H_i}(f(i)). \]

ChartedSpace.sum_of_nonempty definition

[Nonempty H] : ChartedSpace H (M ⊕ M')

Full source

/-- The disjoint union of two charted spaces modelled on a non-empty space `H`
is a charted space over `H`. -/
def ChartedSpace.sum_of_nonempty [Nonempty H] : ChartedSpace H (M ⊕ M') where
  atlas := ((fun e ↦ e.lift_openEmbedding IsOpenEmbedding.inl) '' cm.atlas) ∪
    ((fun e ↦ e.lift_openEmbedding IsOpenEmbedding.inr) '' cm'.atlas)
  -- At `x : M`, the chart is the chart in `M`; at `x' ∈ M'`, it is the chart in `M'`.
  chartAt := Sum.elim (fun x ↦ (cm.chartAt x).lift_openEmbedding IsOpenEmbedding.inl)
    (fun x ↦ (cm'.chartAt x).lift_openEmbedding IsOpenEmbedding.inr)
  mem_chart_source p := by
    cases p with
    | inl x =>
      rw [Sum.elim_inl, lift_openEmbedding_source,
        ← PartialHomeomorph.lift_openEmbedding_source _ IsOpenEmbedding.inl]
      use x, cm.mem_chart_source x
    | inr x =>
      rw [Sum.elim_inr, lift_openEmbedding_source,
        ← PartialHomeomorph.lift_openEmbedding_source _ IsOpenEmbedding.inr]
      use x, cm'.mem_chart_source x
  chart_mem_atlas p := by
    cases p with
    | inl x =>
      rw [Sum.elim_inl]
      left
      use ChartedSpace.chartAt x, cm.chart_mem_atlas x
    | inr x =>
      rw [Sum.elim_inr]
      right
      use ChartedSpace.chartAt x, cm'.chart_mem_atlas x

Charted space structure on the disjoint union of two charted spaces over a non-empty model space

Informal description

Given two charted spaces $M$ and $M'$ modeled on a non-empty topological space $H$, the disjoint union $M \oplus M'$ is naturally a charted space over $H$. The atlas consists of all charts obtained by lifting the charts of $M$ via the left inclusion $\mathrm{inl} \colon M \to M \oplus M'$ and the charts of $M'$ via the right inclusion $\mathrm{inr} \colon M' \to M \oplus M'$. For any point $p \in M \oplus M'$, the preferred chart at $p$ is: - If $p = \mathrm{inl}(x)$ for some $x \in M$, then $\mathrm{chartAt}_H(p)$ is the lift of $\mathrm{chartAt}_H(x)$ via $\mathrm{inl}$. - If $p = \mathrm{inr}(x')$ for some $x' \in M'$, then $\mathrm{chartAt}_H(p)$ is the lift of $\mathrm{chartAt}_H(x')$ via $\mathrm{inr}$.

ChartedSpace.sum instance

: ChartedSpace H (M ⊕ M')

Full source

instance ChartedSpace.sum : ChartedSpace H (M ⊕ M') :=
  if h : Nonempty H then ChartedSpace.sum_of_nonempty else by
  simp only [not_nonempty_iff] at h
  have : IsEmpty M := isEmpty_of_chartedSpace H
  have : IsEmpty M' := isEmpty_of_chartedSpace H
  exact empty H (M ⊕ M')

Charted Space Structure on Disjoint Union of Two Charted Spaces

Informal description

For any two charted spaces $M$ and $M'$ modeled on the same topological space $H$, the disjoint union $M \oplus M'$ is naturally a charted space over $H$. The atlas consists of all charts obtained by lifting the charts of $M$ via the left inclusion $\mathrm{inl} \colon M \to M \oplus M'$ and the charts of $M'$ via the right inclusion $\mathrm{inr} \colon M' \to M \oplus M'$. For any point $p \in M \oplus M'$, the preferred chart at $p$ is: - If $p = \mathrm{inl}(x)$ for some $x \in M$, then $\mathrm{chartAt}_H(p)$ is the lift of $\mathrm{chartAt}_H(x)$ via $\mathrm{inl}$. - If $p = \mathrm{inr}(x')$ for some $x' \in M'$, then $\mathrm{chartAt}_H(p)$ is the lift of $\mathrm{chartAt}_H(x')$ via $\mathrm{inr}$.

ChartedSpace.sum_chartAt_inl theorem

 (x : M) :
  haveI : Nonempty H := nonempty_of_chartedSpace x
  chartAt H (Sum.inl x) = (chartAt H x).lift_openEmbedding (X' := M ⊕ M') IsOpenEmbedding.inl

Full source

lemma ChartedSpace.sum_chartAt_inl (x : M) :
    haveI : Nonempty H := nonempty_of_chartedSpace x
    chartAt H (Sum.inl x)
      = (chartAt H x).lift_openEmbedding (X' := M ⊕ M') IsOpenEmbedding.inl := by
  simp only [chartAt, sum, nonempty_of_chartedSpace x, ↓reduceDIte]
  rfl

Preferred Chart at Left Inclusion Point in Disjoint Union of Charted Spaces

Informal description

For any point $x$ in a charted space $M$ modeled on a topological space $H$, the preferred chart at the point $\mathrm{inl}(x) \in M \oplus M'$ is obtained by lifting the chart $\mathrm{chartAt}_H(x)$ via the open embedding $\mathrm{inl} \colon M \to M \oplus M'$. More precisely, if $H$ is nonempty (which is guaranteed by the existence of $x$), then: \[ \mathrm{chartAt}_H(\mathrm{inl}(x)) = \mathrm{chartAt}_H(x)_{\text{lift}} \] where $\mathrm{chartAt}_H(x)_{\text{lift}}$ denotes the extension of $\mathrm{chartAt}_H(x)$ to $M \oplus M'$ via the open embedding $\mathrm{inl}$.

ChartedSpace.sum_chartAt_inr theorem

 (x' : M') :
  haveI : Nonempty H := nonempty_of_chartedSpace x'
  chartAt H (Sum.inr x') = (chartAt H x').lift_openEmbedding (X' := M ⊕ M') IsOpenEmbedding.inr

Full source

lemma ChartedSpace.sum_chartAt_inr (x' : M') :
    haveI : Nonempty H := nonempty_of_chartedSpace x'
    chartAt H (Sum.inr x')
      = (chartAt H x').lift_openEmbedding (X' := M ⊕ M') IsOpenEmbedding.inr := by
  simp only [chartAt, sum, nonempty_of_chartedSpace x', ↓reduceDIte]
  rfl

Preferred Chart at Right Inclusion Point in Disjoint Union of Charted Spaces

Informal description

For any point $x' \in M'$ in a charted space $M'$ modeled on a topological space $H$, the preferred chart at the point $\mathrm{inr}(x') \in M \oplus M'$ is obtained by lifting the chart $\mathrm{chartAt}_H(x')$ via the open embedding $\mathrm{inr} \colon M' \to M \oplus M'$. More precisely, we have: \[ \mathrm{chartAt}_H(\mathrm{inr}(x')) = \mathrm{chartAt}_H(x')_{\mathrm{lift}} \] where the right-hand side denotes the extension of $\mathrm{chartAt}_H(x')$ along $\mathrm{inr}$.

sum_chartAt_inl_apply theorem

{x y : M} : (chartAt H (.inl x : M ⊕ M')) (Sum.inl y) = (chartAt H x) y

Full source

@[simp, mfld_simps] lemma sum_chartAt_inl_apply {x y : M} :
    (chartAt H (.inl x : M ⊕ M')) (Sum.inl y) = (chartAt H x) y := by
  haveI : Nonempty H := nonempty_of_chartedSpace x
  rw [ChartedSpace.sum_chartAt_inl]
  exact PartialHomeomorph.lift_openEmbedding_apply _ _

Chart Evaluation for Left Inclusion in Disjoint Union of Charted Spaces

Informal description

For any points $x, y$ in a charted space $M$ modeled on a topological space $H$, the chart at the point $\mathrm{inl}(x) \in M \oplus M'$ evaluated at $\mathrm{inl}(y)$ equals the chart at $x$ evaluated at $y$, i.e., \[ \mathrm{chartAt}_H(\mathrm{inl}(x))(\mathrm{inl}(y)) = \mathrm{chartAt}_H(x)(y). \]

sum_chartAt_inr_apply theorem

{x y : M'} : (chartAt H (.inr x : M ⊕ M')) (Sum.inr y) = (chartAt H x) y

Full source

@[simp, mfld_simps] lemma sum_chartAt_inr_apply {x y : M'} :
    (chartAt H (.inr x : M ⊕ M')) (Sum.inr y) = (chartAt H x) y := by
  haveI : Nonempty H := nonempty_of_chartedSpace x
  rw [ChartedSpace.sum_chartAt_inr]
  exact PartialHomeomorph.lift_openEmbedding_apply _ _

Evaluation of Preferred Chart at Right Inclusion Points in Disjoint Union of Charted Spaces

Informal description

For any points $x, y \in M'$ in a charted space $M'$ modeled on a topological space $H$, the preferred chart at the point $\mathrm{inr}(x) \in M \oplus M'$ evaluated at $\mathrm{inr}(y)$ equals the preferred chart at $x$ evaluated at $y$ in $M'$. In other words, the following equality holds: \[ \mathrm{chartAt}_H(\mathrm{inr}(x))(\mathrm{inr}(y)) = \mathrm{chartAt}_H(x)(y). \]

ChartedSpace.mem_atlas_sum theorem

 [h : Nonempty H] {e : PartialHomeomorph (M ⊕ M') H} (he : e ∈ atlas H (M ⊕ M')) :
  (∃ f : PartialHomeomorph M H, f ∈ (atlas H M) ∧ e = (f.lift_openEmbedding IsOpenEmbedding.inl)) ∨
    (∃ f' : PartialHomeomorph M' H, f' ∈ (atlas H M') ∧ e = (f'.lift_openEmbedding IsOpenEmbedding.inr))

Full source

lemma ChartedSpace.mem_atlas_sum [h : Nonempty H]
    {e : PartialHomeomorph (M ⊕ M') H} (he : e ∈ atlas H (M ⊕ M')) :
    (∃ f : PartialHomeomorph M H, f ∈ (atlas H M) ∧ e = (f.lift_openEmbedding IsOpenEmbedding.inl))
    ∨ (∃ f' : PartialHomeomorph M' H, f' ∈ (atlas H M') ∧
      e = (f'.lift_openEmbedding IsOpenEmbedding.inr)) := by
  simp only [atlas, sum, h, ↓reduceDIte] at he
  obtain (⟨x, hx, hxe⟩ | ⟨x, hx, hxe⟩) := he
  · rw [← hxe]; left; use x
  · rw [← hxe]; right; use x

Characterization of Charts in Disjoint Union of Charted Spaces

Informal description

Let $M$ and $M'$ be charted spaces modeled on a non-empty topological space $H$, and let $M \oplus M'$ be their disjoint union. For any chart $e$ in the atlas of $M \oplus M'$, either: 1. There exists a chart $f$ in the atlas of $M$ such that $e$ is obtained by lifting $f$ via the left inclusion $\mathrm{inl} \colon M \to M \oplus M'$, or 2. There exists a chart $f'$ in the atlas of $M'$ such that $e$ is obtained by lifting $f'$ via the right inclusion $\mathrm{inr} \colon M' \to M \oplus M'$.

ChartedSpaceCore structure

(H : Type*) [TopologicalSpace H] (M : Type*)

Full source

/-- 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`. -/
structure ChartedSpaceCore (H : Type*) [TopologicalSpace H] (M : Type*) where
  /-- An atlas of charts, which are only `PartialEquiv`s -/
  atlas : Set (PartialEquiv M H)
  /-- The preferred chart at each point -/
  chartAt : M → PartialEquiv M H
  mem_chart_source : ∀ x, x ∈ (chartAt x).source
  chart_mem_atlas : ∀ x, chartAt x ∈ atlas
  open_source : ∀ e e' : PartialEquiv M H, e ∈ atlas → e' ∈ atlas → IsOpen (e.symm.trans e').source
  continuousOn_toFun : ∀ e e' : PartialEquiv M H, e ∈ atlas → e' ∈ atlas →
    ContinuousOn (e.symm.trans e') (e.symm.trans e').source

Charted space core structure

Informal description

A `ChartedSpaceCore` structure on a type `M` with respect to a model space `H` (equipped with a topology) consists of an atlas of partial equivalences (charts) from `M` to `H` such that the transition maps between any two charts in the atlas are partial homeomorphisms. This structure allows constructing a topology on `M` where the charts become partial homeomorphisms, thereby defining a genuine charted space structure.

ChartedSpaceCore.toTopologicalSpace definition

: TopologicalSpace M

Full source

/-- Topology generated by a set of charts on a Type. -/
protected def toTopologicalSpace : TopologicalSpace M :=
  TopologicalSpace.generateFrom <|
    ⋃ (e : PartialEquiv M H) (_ : e ∈ c.atlas) (s : Set H) (_ : IsOpen s),
      {e ⁻¹' s ∩ e.source}

Topology generated by a charted space core

Informal description

The topology on a type $M$ generated by a charted space core structure is the smallest topology for which all sets of the form $e^{-1}(s) \cap \text{source}(e)$ are open, where $e$ is a chart in the atlas and $s$ is an open subset of the model space $H$. Here, $e^{-1}(s)$ denotes the preimage of $s$ under the chart $e$, and $\text{source}(e)$ is the domain of definition of $e$.

ChartedSpaceCore.open_source' theorem

(he : e ∈ c.atlas) : IsOpen[c.toTopologicalSpace] e.source

Full source

theorem open_source' (he : e ∈ c.atlas) : IsOpen[c.toTopologicalSpace] e.source := by
  apply TopologicalSpace.GenerateOpen.basic
  simp only [exists_prop, mem_iUnion, mem_singleton_iff]
  refine ⟨e, he, univ, isOpen_univ, ?_⟩
  simp only [Set.univ_inter, Set.preimage_univ]

Openness of Chart Sources in Generated Topology

Informal description

For any chart $e$ in the atlas of a charted space core structure $c$ on $M$ with model space $H$, the source set $\text{source}(e)$ is open in the topology generated by $c$.

ChartedSpaceCore.open_target theorem

(he : e ∈ c.atlas) : IsOpen e.target

Full source

theorem open_target (he : e ∈ c.atlas) : IsOpen e.target := by
  have E : e.target ∩ e.symm ⁻¹' e.source = e.target :=
    Subset.antisymm inter_subset_left fun x hx ↦
      ⟨hx, PartialEquiv.target_subset_preimage_source _ hx⟩
  simpa [PartialEquiv.trans_source, E] using c.open_source e e he he

Openness of Chart Targets in Model Space

Informal description

For any chart $e$ in the atlas of a charted space core structure $c$ on $M$ with model space $H$, the target set $e.\text{target} \subseteq H$ is open in the topology of $H$.

ChartedSpaceCore.partialHomeomorph definition

(e : PartialEquiv M H) (he : e ∈ c.atlas) : @PartialHomeomorph M H c.toTopologicalSpace _

Full source

/-- 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. -/
protected def partialHomeomorph (e : PartialEquiv M H) (he : e ∈ c.atlas) :
    @PartialHomeomorph M H c.toTopologicalSpace _ :=
  { __ := c.toTopologicalSpace
    __ := e
    open_source := by convert c.open_source' he
    open_target := by convert c.open_target he
    continuousOn_toFun := by
      letI : TopologicalSpace M := c.toTopologicalSpace
      rw [continuousOn_open_iff (c.open_source' he)]
      intro s s_open
      rw [inter_comm]
      apply TopologicalSpace.GenerateOpen.basic
      simp only [exists_prop, mem_iUnion, mem_singleton_iff]
      exact ⟨e, he, ⟨s, s_open, rfl⟩⟩
    continuousOn_invFun := by
      letI : TopologicalSpace M := c.toTopologicalSpace
      apply continuousOn_isOpen_of_generateFrom
      intro t ht
      simp only [exists_prop, mem_iUnion, mem_singleton_iff] at ht
      rcases ht with ⟨e', e'_atlas, s, s_open, ts⟩
      rw [ts]
      let f := e.symm.trans e'
      have : IsOpen (f ⁻¹' sf ⁻¹' s ∩ f.source) := by
        simpa [f, inter_comm] using (continuousOn_open_iff (c.open_source e e' he e'_atlas)).1
          (c.continuousOn_toFun e e' he e'_atlas) s s_open
      have A : e' ∘ e.symme' ∘ e.symm ⁻¹' se' ∘ e.symm ⁻¹' s ∩ (e.target ∩ e.symm ⁻¹' e'.source) =
          e.target ∩ (e' ∘ e.symm ⁻¹' s ∩ e.symm ⁻¹' e'.source) := by
        rw [← inter_assoc, ← inter_assoc]
        congr 1
        exact inter_comm _ _
      simpa [f, PartialEquiv.trans_source, preimage_inter, preimage_comp.symm, A] using this }

Partial homeomorphism from charted space core atlas

Informal description

Given a charted space core structure on a type $M$ with respect to a model space $H$, and a partial equivalence $e$ from $M$ to $H$ that belongs to the atlas of this structure, this definition constructs a partial homeomorphism between $M$ (equipped with the topology generated by the charted space core) and $H$. The partial homeomorphism has: 1. Open source and target sets 2. Continuous forward and inverse maps when restricted to their respective domains 3. The underlying partial equivalence structure provided by $e$

ChartedSpaceCore.toChartedSpace definition

: @ChartedSpace H _ M c.toTopologicalSpace

Full source

/-- Given a charted space without topology, endow it with a genuine charted space structure with
respect to the topology constructed from the atlas. -/
def toChartedSpace : @ChartedSpace H _ M c.toTopologicalSpace :=
  { __ := c.toTopologicalSpace
    atlas := ⋃ (e : PartialEquiv M H) (he : e ∈ c.atlas), {c.partialHomeomorph e he}
    chartAt := fun x ↦ c.partialHomeomorph (c.chartAt x) (c.chart_mem_atlas x)
    mem_chart_source := fun x ↦ c.mem_chart_source x
    chart_mem_atlas := fun x ↦ by
      simp only [mem_iUnion, mem_singleton_iff]
      exact ⟨c.chartAt x, c.chart_mem_atlas x, rfl⟩}

Charted space structure from core

Informal description

Given a charted space core structure on a type $M$ with respect to a model space $H$, this definition constructs a genuine charted space structure on $M$ by: 1. Equipping $M$ with the topology generated by the charted space core 2. Defining the atlas as the collection of all partial homeomorphisms obtained from the partial equivalences in the core's atlas 3. Specifying that for each point $x \in M$, the preferred chart is the partial homeomorphism derived from the core's preferred chart at $x$ The resulting charted space has the property that all charts are partial homeomorphisms with respect to the generated topology, and their domains cover $M$.

HasGroupoid structure

{H : Type*} [TopologicalSpace H] (M : Type*) [TopologicalSpace M] [ChartedSpace H M] (G : StructureGroupoid H)

Full source

/-- A charted space has an atlas in a groupoid `G` if the change of coordinates belong to the
groupoid. -/
class HasGroupoid {H : Type*} [TopologicalSpace H] (M : Type*) [TopologicalSpace M]
    [ChartedSpace H M] (G : StructureGroupoid H) : Prop where
  compatible : ∀ {e e' : PartialHomeomorph M H}, e ∈ atlas H M → e' ∈ atlas H M → e.symm ≫ₕ e'e.symm ≫ₕ e' ∈ G

Charted space with structure groupoid

Informal description

A charted space $M$ modeled on a topological space $H$ is said to have a structure groupoid $G$ if all coordinate changes between any two charts in the atlas of $M$ belong to $G$. More precisely, for any two charts $e$ and $e'$ in the atlas of $M$, the composition $e^{-1} \circ e'$ (where defined) is an element of $G$.

StructureGroupoid.compatible theorem

 {H : Type*} [TopologicalSpace H] (G : StructureGroupoid H) {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
  [HasGroupoid M G] {e e' : PartialHomeomorph M H} (he : e ∈ atlas H M) (he' : e' ∈ atlas H M) : e.symm ≫ₕ e' ∈ G

Full source

/-- 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 StructureGroupoid.compatible {H : Type*} [TopologicalSpace H] (G : StructureGroupoid H)
    {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [HasGroupoid M G]
    {e e' : PartialHomeomorph M H} (he : e ∈ atlas H M) (he' : e' ∈ atlas H M) : e.symm ≫ₕ e'e.symm ≫ₕ e' ∈ G :=
  HasGroupoid.compatible he he'

Compatibility of Charts in a Charted Space with Structure Groupoid

Informal description

Let $M$ be a charted space modeled on a topological space $H$ with structure groupoid $G$. For any two charts $e$ and $e'$ in the atlas of $M$, the composition of the inverse of $e$ with $e'$ (denoted $e^{-1} \circ e'$) belongs to the groupoid $G$ when restricted to their common domain.

hasGroupoid_of_le theorem

{G₁ G₂ : StructureGroupoid H} (h : HasGroupoid M G₁) (hle : G₁ ≤ G₂) : HasGroupoid M G₂

Full source

theorem hasGroupoid_of_le {G₁ G₂ : StructureGroupoid H} (h : HasGroupoid M G₁) (hle : G₁ ≤ G₂) :
    HasGroupoid M G₂ :=
  ⟨fun he he' ↦ hle (h.compatible he he')⟩

Inheritance of Structure Groupoid by Inclusion

Informal description

Let $M$ be a charted space modeled on a topological space $H$, and let $G_1$ and $G_2$ be structure groupoids on $H$. If $M$ has the structure groupoid $G_1$ and $G_1$ is contained in $G_2$ (i.e., $G_1 \leq G_2$), then $M$ also has the structure groupoid $G_2$.

hasGroupoid_inf_iff theorem

{G₁ G₂ : StructureGroupoid H} : HasGroupoid M (G₁ ⊓ G₂) ↔ HasGroupoid M G₁ ∧ HasGroupoid M G₂

Full source

theorem hasGroupoid_inf_iff {G₁ G₂ : StructureGroupoid H} : HasGroupoidHasGroupoid M (G₁ ⊓ G₂) ↔
    HasGroupoid M G₁ ∧ HasGroupoid M G₂ :=
  ⟨(fun h ↦ ⟨hasGroupoid_of_le h inf_le_left, hasGroupoid_of_le h inf_le_right⟩),
  fun ⟨h1, h2⟩ ↦ { compatible := fun he he' ↦ ⟨h1.compatible he he', h2.compatible he he'⟩ }⟩

Characterization of Structure Groupoid Intersection for Charted Spaces

Informal description

For any two structure groupoids $G_1$ and $G_2$ on a topological space $H$, a charted space $M$ modeled on $H$ has the structure groupoid $G_1 \sqcap G_2$ if and only if it has both $G_1$ and $G_2$ as structure groupoids.

hasGroupoid_of_pregroupoid theorem

 (PG : Pregroupoid H)
  (h :
    ∀ {e e' : PartialHomeomorph M H},
      e ∈ atlas H M → e' ∈ atlas H M → PG.property (e.symm ≫ₕ e') (e.symm ≫ₕ e').source) :
  HasGroupoid M PG.groupoid

Full source

theorem hasGroupoid_of_pregroupoid (PG : Pregroupoid H) (h : ∀ {e e' : PartialHomeomorph M H},
    e ∈ atlas H M → e' ∈ atlas H M → PG.property (e.symm ≫ₕ e') (e.symm ≫ₕ e').source) :
    HasGroupoid M PG.groupoid :=
  ⟨fun he he' ↦ mem_groupoid_of_pregroupoid.mpr ⟨h he he', h he' he⟩⟩

Pregroupoid Property Implies Structure Groupoid Compatibility

Informal description

Let $M$ be a charted space modeled on a topological space $H$, and let $PG$ be a pregroupoid on $H$. Suppose that for any two charts $e$ and $e'$ in the atlas of $M$, the composition $e^{-1} \circ e'$ (defined on its maximal domain) satisfies the property defined by $PG$ on its source set. Then $M$ has the structure groupoid induced by $PG$.

hasGroupoid_model_space instance

(H : Type*) [TopologicalSpace H] (G : StructureGroupoid H) : HasGroupoid H G

Full source

/-- The trivial charted space structure on the model space is compatible with any groupoid. -/
instance hasGroupoid_model_space (H : Type*) [TopologicalSpace H] (G : StructureGroupoid H) :
    HasGroupoid H G where
  compatible {e e'} he he' := by
    rw [chartedSpaceSelf_atlas] at he he'
    simp [he, he', StructureGroupoid.id_mem]

Compatibility of Canonical Charted Space with Any Structure Groupoid

Informal description

For any topological space $H$ and any structure groupoid $G$ on $H$, the canonical charted space structure on $H$ (where the model space is $H$ itself with the identity as the only chart) is compatible with $G$. This means that all coordinate changes between charts in this structure belong to $G$.

hasGroupoid_continuousGroupoid instance

: HasGroupoid M (continuousGroupoid H)

Full source

/-- Any charted space structure is compatible with the groupoid of all partial homeomorphisms. -/
instance hasGroupoid_continuousGroupoid : HasGroupoid M (continuousGroupoid H) := by
  refine ⟨fun _ _ ↦ ?_⟩
  rw [continuousGroupoid, mem_groupoid_of_pregroupoid]
  simp only [and_self_iff]

Compatibility of Charted Spaces with the Continuous Groupoid

Informal description

For any charted space $M$ modeled on a topological space $H$, the space $M$ is compatible with the continuous groupoid on $H$, which consists of all partial homeomorphisms of $H$.

StructureGroupoid.trans_restricted theorem

 {e e' : PartialHomeomorph M H} {G : StructureGroupoid H} (he : e ∈ atlas H M) (he' : e' ∈ atlas H M) [HasGroupoid M G]
  [ClosedUnderRestriction G] {s : Opens M} (hs : Nonempty s) : (e.subtypeRestr hs).symm ≫ₕ e'.subtypeRestr hs ∈ G

Full source

/-- If `G` is closed under restriction, the transition function between the restriction of two
charts `e` and `e'` lies in `G`. -/
theorem StructureGroupoid.trans_restricted {e e' : PartialHomeomorph M H} {G : StructureGroupoid H}
    (he : e ∈ atlas H M) (he' : e' ∈ atlas H M)
    [HasGroupoid M G] [ClosedUnderRestriction G] {s : Opens M} (hs : Nonempty s) :
    (e.subtypeRestr hs).symm ≫ₕ e'.subtypeRestr hs(e.subtypeRestr hs).symm ≫ₕ e'.subtypeRestr hs ∈ G :=
  G.mem_of_eqOnSource (closedUnderRestriction' (G.compatible he he')
    (e.isOpen_inter_preimage_symm s.2)) (e.subtypeRestr_symm_trans_subtypeRestr hs e')

Compatibility of Restricted Charts in a Structure Groupoid

Informal description

Let $M$ be a charted space modeled on a topological space $H$ with structure groupoid $G$, where $G$ is closed under restriction. For any two charts $e$ and $e'$ in the atlas of $M$ and any nonempty open subset $s \subseteq M$, the composition of the inverse of the restriction $e|_s$ with the restriction $e'|_s$ belongs to $G$.

StructureGroupoid.maximalAtlas definition

: Set (PartialHomeomorph M H)

Full source

/-- 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. -/
def StructureGroupoid.maximalAtlas : Set (PartialHomeomorph M H) :=
  { e | ∀ e' ∈ atlas H M, e.symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e ∈ G }

Maximal atlas for a structure groupoid

Informal description

Given a charted space $M$ modeled on a topological space $H$ and admitting a structure groupoid $G$, the maximal atlas associated to $G$ is the set of all partial homeomorphisms $e$ from open subsets of $M$ to $H$ such that for every chart $e'$ in the atlas of $M$, both compositions $e^{-1} \circ e'$ and $e'^{-1} \circ e$ belong to $G$.

StructureGroupoid.subset_maximalAtlas theorem

[HasGroupoid M G] : atlas H M ⊆ G.maximalAtlas M

Full source

/-- The elements of the atlas belong to the maximal atlas for any structure groupoid. -/
theorem StructureGroupoid.subset_maximalAtlas [HasGroupoid M G] : atlasatlas H M ⊆ G.maximalAtlas M :=
  fun _ he _ he' ↦ ⟨G.compatible he he', G.compatible he' he⟩

Atlas Charts Belong to Maximal Atlas for Structure Groupoid

Informal description

For a charted space $M$ modeled on a topological space $H$ with structure groupoid $G$, the atlas of $M$ is contained in the maximal atlas associated to $G$. In other words, every chart in the atlas belongs to the maximal atlas for $G$.

StructureGroupoid.chart_mem_maximalAtlas theorem

[HasGroupoid M G] (x : M) : chartAt H x ∈ G.maximalAtlas M

Full source

theorem StructureGroupoid.chart_mem_maximalAtlas [HasGroupoid M G] (x : M) :
    chartAtchartAt H x ∈ G.maximalAtlas M :=
  G.subset_maximalAtlas (chart_mem_atlas H x)

Preferred Chart Belongs to Maximal Atlas for Structure Groupoid

Informal description

For any point $x$ in a charted space $M$ modeled on a topological space $H$ with structure groupoid $G$, the preferred chart $\text{chartAt}_H(x)$ at $x$ belongs to the maximal atlas associated with $G$.

mem_maximalAtlas_iff theorem

 {e : PartialHomeomorph M H} : e ∈ G.maximalAtlas M ↔ ∀ e' ∈ atlas H M, e.symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e ∈ G

Full source

theorem mem_maximalAtlas_iff {e : PartialHomeomorph M H} :
    e ∈ G.maximalAtlas Me ∈ G.maximalAtlas M ↔ ∀ e' ∈ atlas H M, e.symm ≫ₕ e' ∈ G ∧ e'.symm ≫ₕ e ∈ G :=
  Iff.rfl

Characterization of Maximal Atlas Membership via Compatibility with Atlas Charts

Informal description

Let $M$ be a charted space modeled on a topological space $H$ with structure groupoid $G$. A partial homeomorphism $e$ from $M$ to $H$ belongs to the maximal atlas of $G$ if and only if for every chart $e'$ in the atlas of $M$, both compositions $e^{-1} \circ e'$ and $e'^{-1} \circ e$ belong to $G$.

StructureGroupoid.compatible_of_mem_maximalAtlas theorem

{e e' : PartialHomeomorph M H} (he : e ∈ G.maximalAtlas M) (he' : e' ∈ G.maximalAtlas M) : e.symm ≫ₕ e' ∈ G

Full source

/-- Changing coordinates between two elements of the maximal atlas gives rise to an element
of the structure groupoid. -/
theorem StructureGroupoid.compatible_of_mem_maximalAtlas {e e' : PartialHomeomorph M H}
    (he : e ∈ G.maximalAtlas M) (he' : e' ∈ G.maximalAtlas M) : e.symm ≫ₕ e'e.symm ≫ₕ e' ∈ G := by
  refine G.locality fun x hx ↦ ?_
  set f := chartAt (H := H) (e.symm x)
  let s := e.target ∩ e.symm ⁻¹' f.source
  have hs : IsOpen s := by
    apply e.symm.continuousOn_toFun.isOpen_inter_preimage <;> apply open_source
  have xs : x ∈ s := by
    simp only [s, f, mem_inter_iff, mem_preimage, mem_chart_source, and_true]
    exact ((mem_inter_iff _ _ _).1 hx).1
  refine ⟨s, hs, xs, ?_⟩
  have A : e.symm ≫ₕ fe.symm ≫ₕ f ∈ G := (mem_maximalAtlas_iff.1 he f (chart_mem_atlas _ _)).1
  have B : f.symm ≫ₕ e'f.symm ≫ₕ e' ∈ G := (mem_maximalAtlas_iff.1 he' f (chart_mem_atlas _ _)).2
  have C : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e'(e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ∈ G := G.trans A B
  have D : (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e'(e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' ≈ (e.symm ≫ₕ e').restr s := calc
    (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' = e.symm ≫ₕ (f ≫ₕ f.symm) ≫ₕ e' := by simp only [trans_assoc]
    _ ≈ e.symm ≫ₕ ofSet f.source f.open_source ≫ₕ e'calc
    (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' = e.symm ≫ₕ (f ≫ₕ f.symm) ≫ₕ e' := by simp only [trans_assoc]
    _ ≈ e.symm ≫ₕ ofSet f.source f.open_source ≫ₕ e' :=
      EqOnSource.trans' (refl _) (EqOnSource.trans' (self_trans_symm _) (refl _))
    _ ≈ (e.symm ≫ₕ ofSet f.source f.open_source) ≫ₕ e'calc
    (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' = e.symm ≫ₕ (f ≫ₕ f.symm) ≫ₕ e' := by simp only [trans_assoc]
    _ ≈ e.symm ≫ₕ ofSet f.source f.open_source ≫ₕ e' :=
      EqOnSource.trans' (refl _) (EqOnSource.trans' (self_trans_symm _) (refl _))
    _ ≈ (e.symm ≫ₕ ofSet f.source f.open_source) ≫ₕ e' := by rw [trans_assoc]
    _ ≈ e.symm.restr s ≫ₕ e'calc
    (e.symm ≫ₕ f) ≫ₕ f.symm ≫ₕ e' = e.symm ≫ₕ (f ≫ₕ f.symm) ≫ₕ e' := by simp only [trans_assoc]
    _ ≈ e.symm ≫ₕ ofSet f.source f.open_source ≫ₕ e' :=
      EqOnSource.trans' (refl _) (EqOnSource.trans' (self_trans_symm _) (refl _))
    _ ≈ (e.symm ≫ₕ ofSet f.source f.open_source) ≫ₕ e' := by rw [trans_assoc]
    _ ≈ e.symm.restr s ≫ₕ e' := by rw [trans_of_set']; apply refl
    _ ≈ (e.symm ≫ₕ e').restr s := by rw [restr_trans]
  exact G.mem_of_eqOnSource C (Setoid.symm D)

Compatibility of Maximal Atlas Charts under Structure Groupoid

Informal description

Let $M$ be a charted space modeled on a topological space $H$ with structure groupoid $G$. For any two partial homeomorphisms $e$ and $e'$ in the maximal atlas of $G$, the composition $e^{-1} \circ e'$ belongs to $G$.

StructureGroupoid.mem_maximalAtlas_of_eqOnSource theorem

{e e' : PartialHomeomorph M H} (h : e' ≈ e) (he : e ∈ G.maximalAtlas M) : e' ∈ G.maximalAtlas M

Full source

/-- The maximal atlas of a structure groupoid is stable under equivalence. -/
lemma StructureGroupoid.mem_maximalAtlas_of_eqOnSource {e e' : PartialHomeomorph M H} (h : e' ≈ e)
    (he : e ∈ G.maximalAtlas M) : e' ∈ G.maximalAtlas M := by
  intro e'' he''
  obtain ⟨l, r⟩ := mem_maximalAtlas_iff.mp he e'' he''
  exact ⟨G.mem_of_eqOnSource l (EqOnSource.trans' (EqOnSource.symm' h) (e''.eqOnSource_refl)),
         G.mem_of_eqOnSource r (EqOnSource.trans' (e''.symm).eqOnSource_refl h)⟩

Maximal Atlas Stability under Source Equivalence

Informal description

Let $M$ be a charted space modeled on a topological space $H$ with structure groupoid $G$. For any two partial homeomorphisms $e$ and $e'$ from $M$ to $H$, if $e$ belongs to the maximal atlas of $G$ and $e'$ is equivalent to $e$ on their common source (i.e., they have the same source set and their forward maps coincide on this set), then $e'$ also belongs to the maximal atlas of $G$.

StructureGroupoid.id_mem_maximalAtlas theorem

: PartialHomeomorph.refl H ∈ G.maximalAtlas H

Full source

/-- In the model space, the identity is in any maximal atlas. -/
theorem StructureGroupoid.id_mem_maximalAtlas : PartialHomeomorph.reflPartialHomeomorph.refl H ∈ G.maximalAtlas H :=
  G.subset_maximalAtlas <| by simp

Identity Partial Homeomorphism Belongs to Maximal Atlas

Informal description

For any structure groupoid $G$ on a topological space $H$, the identity partial homeomorphism on $H$ belongs to the maximal atlas associated to $G$.

StructureGroupoid.mem_maximalAtlas_of_mem_groupoid theorem

{f : PartialHomeomorph H H} (hf : f ∈ G) : f ∈ G.maximalAtlas H

Full source

/-- In the model space, any element of the groupoid is in the maximal atlas. -/
theorem StructureGroupoid.mem_maximalAtlas_of_mem_groupoid {f : PartialHomeomorph H H}
    (hf : f ∈ G) : f ∈ G.maximalAtlas H := by
  rintro e (rfl : e = PartialHomeomorph.refl H)
  exact ⟨G.trans (G.symm hf) G.id_mem, G.trans (G.symm G.id_mem) hf⟩

Inclusion of Groupoid Elements in Maximal Atlas

Informal description

For any partial homeomorphism $f$ of the model space $H$ that belongs to a structure groupoid $G$, $f$ is included in the maximal atlas of $H$ associated to $G$.

StructureGroupoid.maximalAtlas_mono theorem

{G G' : StructureGroupoid H} (h : G ≤ G') : G.maximalAtlas M ⊆ G'.maximalAtlas M

Full source

theorem StructureGroupoid.maximalAtlas_mono {G G' : StructureGroupoid H} (h : G ≤ G') :
    G.maximalAtlas M ⊆ G'.maximalAtlas M :=
  fun _ he e' he' ↦ ⟨h (he e' he').1, h (he e' he').2⟩

Monotonicity of Maximal Atlas with Respect to Structure Groupoid Inclusion

Informal description

For any two structure groupoids $G$ and $G'$ on a topological space $H$, if $G$ is contained in $G'$ (i.e., every partial homeomorphism in $G$ also belongs to $G'$), then the maximal atlas associated to $G$ is contained in the maximal atlas associated to $G'$ for any charted space $M$ modeled on $H$.

PartialHomeomorph.singletonChartedSpace definition

(h : e.source = Set.univ) : ChartedSpace H α

Full source

/-- 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
`IsOpenEmbedding.singletonChartedSpace`.) -/
def singletonChartedSpace (h : e.source = Set.univ) : ChartedSpace H α where
  atlas := {e}
  chartAt _ := e
  mem_chart_source _ := by rw [h]; apply mem_univ
  chart_mem_atlas _ := by tauto

Charted space structure induced by a single global chart

Informal description

Given a partial homeomorphism $e$ from a topological space $\alpha$ to a model space $H$ such that the source of $e$ is the entire space $\alpha$ (i.e., $e.\text{source} = \text{univ}$), then $e$ induces a charted space structure on $\alpha$ modeled on $H$. In this structure, the atlas consists of the single chart $e$, and for any point $x \in \alpha$, the preferred chart at $x$ is $e$.

PartialHomeomorph.singletonChartedSpace_chartAt_eq theorem

(h : e.source = Set.univ) {x : α} : @chartAt H _ α _ (e.singletonChartedSpace h) x = e

Full source

@[simp, mfld_simps]
theorem singletonChartedSpace_chartAt_eq (h : e.source = Set.univ) {x : α} :
    @chartAt H _ α _ (e.singletonChartedSpace h) x = e :=
  rfl

Preferred Chart in Singleton Chart Structure Equals Inducing Chart

Informal description

Let $H$ be a topological space and $\alpha$ be a topological space with a charted space structure modeled on $H$ induced by a single global partial homeomorphism $e \colon \alpha \to H$ (i.e., $e.\text{source} = \text{univ}$). Then, for any point $x \in \alpha$, the preferred chart at $x$ in this charted space structure is equal to $e$.

PartialHomeomorph.singletonChartedSpace_chartAt_source theorem

(h : e.source = Set.univ) {x : α} : (@chartAt H _ α _ (e.singletonChartedSpace h) x).source = Set.univ

Full source

theorem singletonChartedSpace_chartAt_source (h : e.source = Set.univ) {x : α} :
    (@chartAt H _ α _ (e.singletonChartedSpace h) x).source = Set.univ :=
  h

Source of Preferred Chart in Singleton Chart Structure is Universal Set

Informal description

Let $H$ be a topological space and $\alpha$ be a topological space with a charted space structure induced by a single global partial homeomorphism $e \colon \alpha \to H$ (i.e., $e.\text{source} = \text{univ}$). Then, for any point $x \in \alpha$, the source of the preferred chart $\text{chartAt}_H(x)$ is the entire space $\alpha$, i.e., $(\text{chartAt}_H(x)).\text{source} = \text{univ}$.

PartialHomeomorph.singletonChartedSpace_mem_atlas_eq theorem

(h : e.source = Set.univ) (e' : PartialHomeomorph α H) (h' : e' ∈ (e.singletonChartedSpace h).atlas) : e' = e

Full source

theorem singletonChartedSpace_mem_atlas_eq (h : e.source = Set.univ) (e' : PartialHomeomorph α H)
    (h' : e' ∈ (e.singletonChartedSpace h).atlas) : e' = e :=
  h'

Uniqueness of Charts in Singleton Chart Structure

Informal description

Let $e$ be a partial homeomorphism from a topological space $\alpha$ to a model space $H$ such that the source of $e$ is all of $\alpha$ (i.e., $e.\text{source} = \text{univ}$). Then for any other partial homeomorphism $e'$ from $\alpha$ to $H$ that belongs to the atlas of the charted space structure induced by $e$, we have $e' = e$. In other words, when a charted space structure on $\alpha$ is defined by a single global chart $e$, the atlas consists only of $e$ itself.

PartialHomeomorph.singleton_hasGroupoid theorem

 (h : e.source = Set.univ) (G : StructureGroupoid H) [ClosedUnderRestriction G] :
  @HasGroupoid _ _ _ _ (e.singletonChartedSpace h) G

Full source

/-- 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. -/
theorem singleton_hasGroupoid (h : e.source = Set.univ) (G : StructureGroupoid H)
    [ClosedUnderRestriction G] : @HasGroupoid _ _ _ _ (e.singletonChartedSpace h) G :=
  { __ := e.singletonChartedSpace h
    compatible := by
      intro e' e'' he' he''
      rw [e.singletonChartedSpace_mem_atlas_eq h e' he',
        e.singletonChartedSpace_mem_atlas_eq h e'' he'']
      refine G.mem_of_eqOnSource ?_ e.symm_trans_self
      have hle : idRestrGroupoid ≤ G := (closedUnderRestriction_iff_id_le G).mp (by assumption)
      exact StructureGroupoid.le_iff.mp hle _ (idRestrGroupoid_mem _) }

Global Chart Induces Structure Groupoid on Space

Informal description

Let $e$ be a partial homeomorphism from a topological space $\alpha$ to a model space $H$ such that the source of $e$ covers all of $\alpha$ (i.e., $e.\text{source} = \text{univ}$). Then, for any structure groupoid $G$ on $H$ that is closed under restriction, the charted space structure on $\alpha$ induced by $e$ has $G$ as its structure groupoid.

Topology.IsOpenEmbedding.singletonChartedSpace definition

{f : α → H} (h : IsOpenEmbedding f) : ChartedSpace H α

Full source

/-- An open embedding of `α` into `H` induces an `H`-charted space structure on `α`.
See `PartialHomeomorph.singletonChartedSpace`. -/
def singletonChartedSpace {f : α → H} (h : IsOpenEmbedding f) : ChartedSpace H α :=
  (h.toPartialHomeomorph f).singletonChartedSpace (toPartialHomeomorph_source _ _)

Charted space structure induced by an open embedding

Informal description

Given an open embedding $f \colon \alpha \to H$ from a topological space $\alpha$ to a model space $H$, this defines a charted space structure on $\alpha$ modeled on $H$ where the atlas consists of the single partial homeomorphism induced by $f$.

Topology.IsOpenEmbedding.singletonChartedSpace_chartAt_eq theorem

{f : α → H} (h : IsOpenEmbedding f) {x : α} : ⇑(@chartAt H _ α _ h.singletonChartedSpace x) = f

Full source

theorem singletonChartedSpace_chartAt_eq {f : α → H} (h : IsOpenEmbedding f) {x : α} :
    ⇑(@chartAt H _ α _ h.singletonChartedSpace x) = f :=
  rfl

Equality of Chart and Embedding in Singleton Chart Structure

Informal description

Given an open embedding $f \colon \alpha \to H$ from a topological space $\alpha$ to a model space $H$, the chart at any point $x \in \alpha$ in the induced charted space structure coincides with $f$, i.e., $\text{chartAt}_H(x) = f$.

Topology.IsOpenEmbedding.singleton_hasGroupoid theorem

 {f : α → H} (h : IsOpenEmbedding f) (G : StructureGroupoid H) [ClosedUnderRestriction G] :
  @HasGroupoid _ _ _ _ h.singletonChartedSpace G

Full source

theorem singleton_hasGroupoid {f : α → H} (h : IsOpenEmbedding f) (G : StructureGroupoid H)
    [ClosedUnderRestriction G] : @HasGroupoid _ _ _ _ h.singletonChartedSpace G :=
  (h.toPartialHomeomorph f).singleton_hasGroupoid (toPartialHomeomorph_source _ _) G

Open embedding induces structure groupoid on singleton charted space

Informal description

Let $H$ be a topological space and $G$ be a structure groupoid on $H$ that is closed under restriction. Given an open embedding $f \colon \alpha \to H$ from a topological space $\alpha$ to $H$, the charted space structure on $\alpha$ induced by $f$ (where the atlas consists of the single partial homeomorphism induced by $f$) has $G$ as its structure groupoid.

TopologicalSpace.Opens.instChartedSpace instance

: ChartedSpace H s

Full source

/-- An open subset of a charted space is naturally a charted space. -/
protected instance instChartedSpace : ChartedSpace H s where
  atlas := ⋃ x : s, {(chartAt H x.1).subtypeRestr ⟨x⟩}
  chartAt x := (chartAt H x.1).subtypeRestr ⟨x⟩
  mem_chart_source x := ⟨trivial, mem_chart_source H x.1⟩
  chart_mem_atlas x := by
    simp only [mem_iUnion, mem_singleton_iff]
    use x

Open Subsets as Charted Spaces

Informal description

For any open subset $s$ of a charted space $M$ modeled on a topological space $H$, the subspace $s$ inherits a natural charted space structure where the charts are the restrictions of the charts of $M$ to $s$.

TopologicalSpace.Opens.chart_eq theorem

 {s : Opens M} (hs : Nonempty s) {e : PartialHomeomorph s H} (he : e ∈ atlas H s) :
  ∃ x : s, e = (chartAt H (x : M)).subtypeRestr hs

Full source

/-- If `s` is a non-empty open subset of `M`, every chart of `s` is the restriction
of some chart on `M`. -/
lemma chart_eq {s : Opens M} (hs : Nonempty s) {e : PartialHomeomorph s H} (he : e ∈ atlas H s) :
    ∃ x : s, e = (chartAt H (x : M)).subtypeRestr hs := by
  rcases he with ⟨xset, ⟨x, hx⟩, he⟩
  exact ⟨x, mem_singleton_iff.mp (by convert he)⟩

Charts on Open Subsets are Restrictions of Global Charts

Informal description

Let $M$ be a charted space modeled on a topological space $H$, and let $s$ be a non-empty open subset of $M$. For any chart $e$ in the atlas of $s$ (i.e., $e$ is a partial homeomorphism from $s$ to $H$), there exists a point $x \in s$ such that $e$ is equal to the restriction of the preferred chart $\text{chartAt}_H(x)$ (viewed as a chart on $M$) to the open subset $s$. In other words, every chart of a non-empty open subset $s \subseteq M$ is obtained by restricting some preferred chart of $M$ to $s$.

TopologicalSpace.Opens.chart_eq' theorem

 {t : Opens H} (ht : Nonempty t) {e' : PartialHomeomorph t H} (he' : e' ∈ atlas H t) :
  ∃ x : t, e' = (chartAt H ↑x).subtypeRestr ht

Full source

/-- If `t` is a non-empty open subset of `H`,
every chart of `t` is the restriction of some chart on `H`. -/
-- XXX: can I unify this with `chart_eq`?
lemma chart_eq' {t : Opens H} (ht : Nonempty t) {e' : PartialHomeomorph t H}
    (he' : e' ∈ atlas H t) : ∃ x : t, e' = (chartAt H ↑x).subtypeRestr ht := by
  rcases he' with ⟨xset, ⟨x, hx⟩, he'⟩
  exact ⟨x, mem_singleton_iff.mp (by convert he')⟩

Charts on Open Subsets as Restrictions of Global Charts

Informal description

Let $H$ be a topological space and $t$ be a non-empty open subset of $H$. For any chart $e'$ in the atlas of $t$ (viewed as a charted space), there exists a point $x \in t$ such that $e'$ is equal to the restriction of the preferred chart of $H$ at $x$ to the subset $t$.

TopologicalSpace.Opens.instHasGroupoid instance

[ClosedUnderRestriction G] : HasGroupoid s G

Full source

/-- If a groupoid `G` is `ClosedUnderRestriction`, then an open subset of a space which is
`HasGroupoid G` is naturally `HasGroupoid G`. -/
protected instance instHasGroupoid [ClosedUnderRestriction G] : HasGroupoid s G where
  compatible := by
    rintro e e' ⟨_, ⟨x, hc⟩, he⟩ ⟨_, ⟨x', hc'⟩, he'⟩
    rw [hc.symm, mem_singleton_iff] at he
    rw [hc'.symm, mem_singleton_iff] at he'
    rw [he, he']
    refine G.mem_of_eqOnSource ?_
      (subtypeRestr_symm_trans_subtypeRestr (s := s) _ (chartAt H x) (chartAt H x'))
    apply closedUnderRestriction'
    · exact G.compatible (chart_mem_atlas _ _) (chart_mem_atlas _ _)
    · exact isOpen_inter_preimage_symm (chartAt _ _) s.2

Inheritance of Structure Groupoid for Open Subsets of Charted Spaces

Informal description

For any open subset $s$ of a charted space $M$ modeled on a topological space $H$, if $M$ has a structure groupoid $G$ that is closed under restriction, then $s$ inherits a natural structure groupoid $G$ where the coordinate changes between charts are restrictions of the coordinate changes in $M$.

TopologicalSpace.Opens.chartAt_subtype_val_symm_eventuallyEq theorem

(U : Opens M) {x : U} : (chartAt H x.val).symm =ᶠ[𝓝 (chartAt H x.val x.val)] Subtype.val ∘ (chartAt H x).symm

Full source

theorem chartAt_subtype_val_symm_eventuallyEq (U : Opens M) {x : U} :
    (chartAt H x.val).symm =ᶠ[𝓝 (chartAt H x.val x.val)] Subtype.val ∘ (chartAt H x).symm := by
  set e := chartAt H x.val
  have heUx_nhds : (e.subtypeRestr ⟨x⟩).target ∈ 𝓝 (e x) := by
    apply (e.subtypeRestr ⟨x⟩).open_target.mem_nhds
    exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)
  exact Filter.eventuallyEq_of_mem heUx_nhds (e.subtypeRestr_symm_eqOn ⟨x⟩)

Local Equality of Chart Inverses for Open Subset Inclusion

Informal description

Let $M$ be a charted space modeled on a topological space $H$, and let $U$ be an open subset of $M$. For any point $x \in U$, the inverse of the preferred chart at $x$ (viewed as a point in $M$) is eventually equal to the composition of the inclusion map $U \hookrightarrow M$ with the inverse of the preferred chart at $x$ (viewed as a point in $U$), in a neighborhood of the image $\text{chartAt}_H(x)(x)$. More precisely, for $x \in U$, we have: $$(\text{chartAt}_H(x))^{-1} = \iota \circ (\text{chartAt}_H(x))^{-1}$$ eventually in a neighborhood of $\text{chartAt}_H(x)(x)$, where $\iota: U \hookrightarrow M$ is the inclusion map.

TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq theorem

 {U V : Opens M} (hUV : U ≤ V) {x : U} :
  (chartAt H (Opens.inclusion hUV x)).symm =ᶠ[𝓝 (chartAt H (Opens.inclusion hUV x) (Set.inclusion hUV x))]
    Opens.inclusion hUV ∘ (chartAt H x).symm

Full source

theorem chartAt_inclusion_symm_eventuallyEq {U V : Opens M} (hUV : U ≤ V) {x : U} :
    (chartAt H (Opens.inclusion hUV x)).symm
    =ᶠ[𝓝 (chartAt H (Opens.inclusion hUV x) (Set.inclusion hUV x))]
    Opens.inclusion hUV ∘ (chartAt H x).symm := by
  set e := chartAt H (x : M)
  have heUx_nhds : (e.subtypeRestr ⟨x⟩).target ∈ 𝓝 (e x) := by
    apply (e.subtypeRestr ⟨x⟩).open_target.mem_nhds
    exact e.map_subtype_source ⟨x⟩ (mem_chart_source _ _)
  exact Filter.eventuallyEq_of_mem heUx_nhds <| e.subtypeRestr_symm_eqOn_of_le ⟨x⟩
    ⟨Opens.inclusion hUV x⟩ hUV

Compatibility of Chart Inverses Under Inclusion of Open Subsets

Informal description

Let $M$ be a charted space modeled on a topological space $H$, and let $U$ and $V$ be open subsets of $M$ with $U \subseteq V$. For any point $x \in U$, the inverse of the preferred chart at the inclusion of $x$ in $V$ is eventually equal (in a neighborhood of the chart's image) to the composition of the inclusion map $U \hookrightarrow V$ with the inverse of the preferred chart at $x$. More precisely, for $x \in U$, we have: $$(\text{chartAt}_H(\iota_{U,V}(x)))^{-1} = \iota_{U,V} \circ (\text{chartAt}_H(x))^{-1}$$ eventually in a neighborhood of $\text{chartAt}_H(\iota_{U,V}(x))(\iota_{U,V}(x))$, where $\iota_{U,V}: U \hookrightarrow V$ is the inclusion map.

StructureGroupoid.restriction_in_maximalAtlas theorem

 {e : PartialHomeomorph M H} (he : e ∈ atlas H M) {s : Opens M} (hs : Nonempty s) {G : StructureGroupoid H}
  [HasGroupoid M G] [ClosedUnderRestriction G] : e.subtypeRestr hs ∈ G.maximalAtlas s

Full source

/-- 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. -/
lemma StructureGroupoid.restriction_in_maximalAtlas {e : PartialHomeomorph M H}
    (he : e ∈ atlas H M) {s : Opens M} (hs : Nonempty s) {G : StructureGroupoid H} [HasGroupoid M G]
    [ClosedUnderRestriction G] : e.subtypeRestr hs ∈ G.maximalAtlas s := by
  intro e' he'
  -- `e'` is the restriction of some chart of `M` at `x`,
  obtain ⟨x, this⟩ := Opens.chart_eq hs he'
  rw [this]
  -- The transition functions between the unrestricted charts lie in the groupoid,
  -- the transition functions of the restriction are the restriction of the transition function.
  exact ⟨G.trans_restricted he (chart_mem_atlas H (x : M)) hs,
         G.trans_restricted (chart_mem_atlas H (x : M)) he hs⟩

Restriction of a Chart to an Open Subset Belongs to the Maximal Atlas

Informal description

Let $M$ be a charted space modeled on a topological space $H$ with structure groupoid $G$, where $G$ is closed under restriction. For any chart $e$ in the atlas of $M$ and any nonempty open subset $s \subseteq M$, the restriction $e|_s$ of $e$ to $s$ belongs to the maximal atlas of $s$ associated to $G$.

Structomorph structure

(G : StructureGroupoid H) (M : Type*) (M' : Type*) [TopologicalSpace M]
  [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H M'] extends Homeomorph M M'

Full source

/-- 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. -/
structure Structomorph (G : StructureGroupoid H) (M : Type*) (M' : Type*) [TopologicalSpace M]
  [TopologicalSpace M'] [ChartedSpace H M] [ChartedSpace H M'] extends Homeomorph M M' where
  mem_groupoid : ∀ c : PartialHomeomorph M H, ∀ c' : PartialHomeomorph M' H, c ∈ atlas H M →
    c' ∈ atlas H M' → c.symm ≫ₕ toHomeomorph.toPartialHomeomorph ≫ₕ c'c.symm ≫ₕ toHomeomorph.toPartialHomeomorph ≫ₕ c' ∈ G

$G$-Structomorphism between charted spaces

Informal description

A $G$-structomorphism between two charted spaces $M$ and $M'$ modeled on the same topological space $H$ is a homeomorphism $f \colon M \to M'$ such that for every chart $e$ of $M$ and every chart $e'$ of $M'$, the composition $e' \circ f \circ e^{-1}$ (where defined) belongs to the structure groupoid $G$. This generalizes the notion of diffeomorphism to arbitrary structure groupoids.

Structomorph.refl definition

(M : Type*) [TopologicalSpace M] [ChartedSpace H M] [HasGroupoid M G] : Structomorph G M M

Full source

/-- The identity is a diffeomorphism of any charted space, for any groupoid. -/
def Structomorph.refl (M : Type*) [TopologicalSpace M] [ChartedSpace H M] [HasGroupoid M G] :
    Structomorph G M M :=
  { Homeomorph.refl M with
    mem_groupoid := fun c c' hc hc' ↦ by
      change PartialHomeomorph.symmPartialHomeomorph.symm c ≫ₕ PartialHomeomorph.refl M ≫ₕ c'PartialHomeomorph.symm c ≫ₕ PartialHomeomorph.refl M ≫ₕ c' ∈ G
      rw [PartialHomeomorph.refl_trans]
      exact G.compatible hc hc' }

Identity $G$-structomorphism

Informal description

The identity homeomorphism on a charted space $M$ modeled on $H$ with structure groupoid $G$ is a $G$-structomorphism. This means that for any charts $c$ and $c'$ in the atlas of $M$, the composition $c^{-1} \circ \text{id}_M \circ c'$ (where defined) belongs to the groupoid $G$.

Structomorph.symm definition

(e : Structomorph G M M') : Structomorph G M' M

Full source

/-- The inverse of a structomorphism is a structomorphism. -/
def Structomorph.symm (e : Structomorph G M M') : Structomorph G M' M :=
  { e.toHomeomorph.symm with
    mem_groupoid := by
      intro c c' hc hc'
      have : (c'.symm ≫ₕ e.toHomeomorph.toPartialHomeomorph ≫ₕ c).symm ∈ G :=
        G.symm (e.mem_groupoid c' c hc' hc)
      rwa [trans_symm_eq_symm_trans_symm, trans_symm_eq_symm_trans_symm, symm_symm, trans_assoc]
        at this }

Inverse of a $G$-structomorphism

Informal description

Given a $G$-structomorphism $e \colon M \to M'$ between charted spaces modeled on the same topological space $H$ with structure groupoid $G$, the inverse map $e^{-1} \colon M' \to M$ is also a $G$-structomorphism. This means that for any charts $c$ of $M'$ and $c'$ of $M$, the composition $c' \circ e^{-1} \circ c^{-1}$ (where defined) belongs to the structure groupoid $G$.

Structomorph.trans definition

(e : Structomorph G M M') (e' : Structomorph G M' M'') : Structomorph G M M''

Full source

/-- The composition of structomorphisms is a structomorphism. -/
def Structomorph.trans (e : Structomorph G M M') (e' : Structomorph G M' M'') :
    Structomorph G M M'' :=
  { Homeomorph.trans e.toHomeomorph e'.toHomeomorph with
    mem_groupoid := by
      /- Let c and c' be two charts in M and M''. We want to show that e' ∘ e is smooth in these
      charts, around any point x. For this, let y = e (c⁻¹ x), and consider a chart g around y.
      Then g ∘ e ∘ c⁻¹ and c' ∘ e' ∘ g⁻¹ are both smooth as e and e' are structomorphisms, so
      their composition is smooth, and it coincides with c' ∘ e' ∘ e ∘ c⁻¹ around x. -/
      intro c c' hc hc'
      refine G.locality fun x hx ↦ ?_
      let f₁ := e.toHomeomorph.toPartialHomeomorph
      let f₂ := e'.toHomeomorph.toPartialHomeomorph
      let f := (e.toHomeomorph.trans e'.toHomeomorph).toPartialHomeomorph
      have feq : f = f₁ ≫ₕ f₂ := Homeomorph.trans_toPartialHomeomorph _ _
      -- define the atlas g around y
      let y := (c.symm ≫ₕ f₁) x
      let g := chartAt (H := H) y
      have hg₁ := chart_mem_atlas (H := H) y
      have hg₂ := mem_chart_source (H := H) y
      let s := (c.symm ≫ₕ f₁).source ∩ c.symm ≫ₕ f₁ ⁻¹' g.source
      have open_s : IsOpen s := by
        apply (c.symm ≫ₕ f₁).continuousOn_toFun.isOpen_inter_preimage <;> apply open_source
      have : x ∈ s := by
        constructor
        · simp only [f₁, trans_source, preimage_univ, inter_univ,
            Homeomorph.toPartialHomeomorph_source]
          rw [trans_source] at hx
          exact hx.1
        · exact hg₂
      refine ⟨s, open_s, this, ?_⟩
      let F₁ := (c.symm ≫ₕ f₁ ≫ₕ g) ≫ₕ g.symm ≫ₕ f₂ ≫ₕ c'
      have A : F₁ ∈ G := G.trans (e.mem_groupoid c g hc hg₁) (e'.mem_groupoid g c' hg₁ hc')
      let F₂ := (c.symm ≫ₕ f ≫ₕ c').restr s
      have : F₁ ≈ F₂ := calc
        F₁ ≈ c.symm ≫ₕ f₁ ≫ₕ (g ≫ₕ g.symm) ≫ₕ f₂ ≫ₕ c' := by
            simp only [F₁, trans_assoc, _root_.refl]
        _ ≈ c.symm ≫ₕ f₁ ≫ₕ ofSet g.source g.open_source ≫ₕ f₂ ≫ₕ c'calc
        F₁ ≈ c.symm ≫ₕ f₁ ≫ₕ (g ≫ₕ g.symm) ≫ₕ f₂ ≫ₕ c' := by
            simp only [F₁, trans_assoc, _root_.refl]
        _ ≈ c.symm ≫ₕ f₁ ≫ₕ ofSet g.source g.open_source ≫ₕ f₂ ≫ₕ c' :=
          EqOnSource.trans' (_root_.refl _) (EqOnSource.trans' (_root_.refl _)
            (EqOnSource.trans' (self_trans_symm g) (_root_.refl _)))
        _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ ofSet g.source g.open_source) ≫ₕ f₂ ≫ₕ c'calc
        F₁ ≈ c.symm ≫ₕ f₁ ≫ₕ (g ≫ₕ g.symm) ≫ₕ f₂ ≫ₕ c' := by
            simp only [F₁, trans_assoc, _root_.refl]
        _ ≈ c.symm ≫ₕ f₁ ≫ₕ ofSet g.source g.open_source ≫ₕ f₂ ≫ₕ c' :=
          EqOnSource.trans' (_root_.refl _) (EqOnSource.trans' (_root_.refl _)
            (EqOnSource.trans' (self_trans_symm g) (_root_.refl _)))
        _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ ofSet g.source g.open_source) ≫ₕ f₂ ≫ₕ c' := by
          simp only [trans_assoc, _root_.refl]
        _ ≈ (c.symm ≫ₕ f₁).restr s ≫ₕ f₂ ≫ₕ c'calc
        F₁ ≈ c.symm ≫ₕ f₁ ≫ₕ (g ≫ₕ g.symm) ≫ₕ f₂ ≫ₕ c' := by
            simp only [F₁, trans_assoc, _root_.refl]
        _ ≈ c.symm ≫ₕ f₁ ≫ₕ ofSet g.source g.open_source ≫ₕ f₂ ≫ₕ c' :=
          EqOnSource.trans' (_root_.refl _) (EqOnSource.trans' (_root_.refl _)
            (EqOnSource.trans' (self_trans_symm g) (_root_.refl _)))
        _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ ofSet g.source g.open_source) ≫ₕ f₂ ≫ₕ c' := by
          simp only [trans_assoc, _root_.refl]
        _ ≈ (c.symm ≫ₕ f₁).restr s ≫ₕ f₂ ≫ₕ c' := by rw [trans_of_set']
        _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ f₂ ≫ₕ c').restr scalc
        F₁ ≈ c.symm ≫ₕ f₁ ≫ₕ (g ≫ₕ g.symm) ≫ₕ f₂ ≫ₕ c' := by
            simp only [F₁, trans_assoc, _root_.refl]
        _ ≈ c.symm ≫ₕ f₁ ≫ₕ ofSet g.source g.open_source ≫ₕ f₂ ≫ₕ c' :=
          EqOnSource.trans' (_root_.refl _) (EqOnSource.trans' (_root_.refl _)
            (EqOnSource.trans' (self_trans_symm g) (_root_.refl _)))
        _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ ofSet g.source g.open_source) ≫ₕ f₂ ≫ₕ c' := by
          simp only [trans_assoc, _root_.refl]
        _ ≈ (c.symm ≫ₕ f₁).restr s ≫ₕ f₂ ≫ₕ c' := by rw [trans_of_set']
        _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ f₂ ≫ₕ c').restr s := by rw [restr_trans]
        _ ≈ (c.symm ≫ₕ (f₁ ≫ₕ f₂) ≫ₕ c').restr scalc
        F₁ ≈ c.symm ≫ₕ f₁ ≫ₕ (g ≫ₕ g.symm) ≫ₕ f₂ ≫ₕ c' := by
            simp only [F₁, trans_assoc, _root_.refl]
        _ ≈ c.symm ≫ₕ f₁ ≫ₕ ofSet g.source g.open_source ≫ₕ f₂ ≫ₕ c' :=
          EqOnSource.trans' (_root_.refl _) (EqOnSource.trans' (_root_.refl _)
            (EqOnSource.trans' (self_trans_symm g) (_root_.refl _)))
        _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ ofSet g.source g.open_source) ≫ₕ f₂ ≫ₕ c' := by
          simp only [trans_assoc, _root_.refl]
        _ ≈ (c.symm ≫ₕ f₁).restr s ≫ₕ f₂ ≫ₕ c' := by rw [trans_of_set']
        _ ≈ ((c.symm ≫ₕ f₁) ≫ₕ f₂ ≫ₕ c').restr s := by rw [restr_trans]
        _ ≈ (c.symm ≫ₕ (f₁ ≫ₕ f₂) ≫ₕ c').restr s := by
          simp only [EqOnSource.restr, trans_assoc, _root_.refl]
        _ ≈ F₂ := by simp only [F₂, feq, _root_.refl]
      have : F₂ ∈ G := G.mem_of_eqOnSource A (Setoid.symm this)
      exact this }

Composition of $G$-structomorphisms

Informal description

Given two $G$-structomorphisms $e \colon M \to M'$ and $e' \colon M' \to M''$ between charted spaces modeled on $H$ with structure groupoid $G$, their composition $e' \circ e \colon M \to M''$ is also a $G$-structomorphism. This means that the composition preserves the structure groupoid $G$ in the sense that for any charts $c$ of $M$ and $c'$ of $M''$, the coordinate change $c' \circ (e' \circ e) \circ c^{-1}$ (where defined) belongs to $G$.

StructureGroupoid.restriction_mem_maximalAtlas_subtype theorem

 {e : PartialHomeomorph M H} (he : e ∈ atlas H M) (hs : Nonempty e.source) [HasGroupoid M G]
  [ClosedUnderRestriction G] :
  let s := { carrier := e.source, is_open' := e.open_source : Opens M }
  let t := { carrier := e.target, is_open' := e.open_target : Opens H }
  ∀ c' ∈ atlas H t, e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ c' ∈ G.maximalAtlas s

Full source

/-- Restricting a chart to its source `s ⊆ M` yields a chart in the maximal atlas of `s`. -/
theorem StructureGroupoid.restriction_mem_maximalAtlas_subtype
    {e : PartialHomeomorph M H} (he : e ∈ atlas H M)
    (hs : Nonempty e.source) [HasGroupoid M G] [ClosedUnderRestriction G] :
    let s := { carrier := e.source, is_open' := e.open_source : Opens M }
    let t := { carrier := e.target, is_open' := e.open_target : Opens H }
    ∀ c' ∈ atlas H t, e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ c' ∈ G.maximalAtlas s := by
  intro s t c' hc'
  have : Nonempty t := nonempty_coe_sort.mpr (e.mapsTo.nonempty (nonempty_coe_sort.mp hs))
  obtain ⟨x, hc'⟩ := Opens.chart_eq this hc'
  -- As H has only one chart, `chartAt H x` is the identity: i.e., `c'` is the inclusion.
  rw [hc', (chartAt_self_eq)]
  -- Our expression equals this chart, at least on its source.
  rw [PartialHomeomorph.subtypeRestr_def, PartialHomeomorph.trans_refl]
  let goal := e.toHomeomorphSourceTarget.toPartialHomeomorph ≫ₕ (t.partialHomeomorphSubtypeCoe this)
  have : goal ≈ e.subtypeRestr (s := s) hs :=
    (goal.eqOnSource_iff (e.subtypeRestr (s := s) hs)).mpr
      ⟨by
        simp only [trans_toPartialEquiv, PartialEquiv.trans_source,
          Homeomorph.toPartialHomeomorph_source, toFun_eq_coe, Homeomorph.toPartialHomeomorph_apply,
          Opens.partialHomeomorphSubtypeCoe_source, preimage_univ, inter_self, subtypeRestr_source,
          goal, s]
        exact Subtype.coe_preimage_self _ |>.symm, by intro _ _; rfl⟩
  exact G.mem_maximalAtlas_of_eqOnSource (M := s) this (G.restriction_in_maximalAtlas he hs)

Composition of Chart with Target Chart Belongs to Maximal Atlas of Source

Informal description

Let $M$ be a charted space modeled on a topological space $H$ with structure groupoid $G$, where $G$ is closed under restriction. For any chart $e$ in the atlas of $M$ with nonempty source, let $s$ and $t$ be the open subsets of $M$ and $H$ corresponding to the source and target of $e$ respectively. Then for any chart $c'$ in the atlas of $t$, the composition of the homeomorphism $e \colon s \to t$ with $c'$ belongs to the maximal atlas of $s$ associated to $G$.

PartialHomeomorph.toStructomorph definition

 {e : PartialHomeomorph M H} (he : e ∈ atlas H M) [HasGroupoid M G] [ClosedUnderRestriction G] :
  let s : Opens M := { carrier := e.source, is_open' := e.open_source }
  let t : Opens H := { carrier := e.target, is_open' := e.open_target }
  Structomorph G s t

Full source

/-- Each chart of a charted space is a structomorphism between its source and target. -/
def PartialHomeomorph.toStructomorph {e : PartialHomeomorph M H} (he : e ∈ atlas H M)
    [HasGroupoid M G] [ClosedUnderRestriction G] :
    let s : Opens M := { carrier := e.source, is_open' := e.open_source }
    let t : Opens H := { carrier := e.target, is_open' := e.open_target }
    Structomorph G s t := by
  intro s t
  by_cases h : Nonempty e.source
  · exact { e.toHomeomorphSourceTarget with
      mem_groupoid :=
        -- The atlas of H on itself has only one chart, hence c' is the inclusion.
        -- Then, compatibility of `G` *almost* yields our claim --- except that `e` is a chart
        -- on `M` and `c` is one on `s`: we need to show that restricting `e` to `s` and composing
        -- with `c'` yields a chart in the maximal atlas of `s`.
        fun c c' hc hc' ↦ G.compatible_of_mem_maximalAtlas (G.subset_maximalAtlas hc)
          (G.restriction_mem_maximalAtlas_subtype he h c' hc') }
  · have : IsEmpty s := not_nonempty_iff.mp h
    have : IsEmpty t := isEmpty_coe_sort.mpr
      (by convert e.image_source_eq_target ▸ image_eq_empty.mpr (isEmpty_coe_sort.mp this))
    exact { Homeomorph.empty with
      -- `c'` cannot exist: it would be the restriction of `chartAt H x` at some `x ∈ t`.
      mem_groupoid := fun _ c' _ ⟨_, ⟨x, _⟩, _⟩ ↦ (this.false x).elim }

Structomorphism induced by a chart

Informal description

Given a charted space $M$ modeled on a topological space $H$ with a structure groupoid $G$, and a chart $e$ in the atlas of $M$, the partial homeomorphism $e$ induces a $G$-structomorphism between its source and target. More precisely: 1. The source $s$ of $e$ is an open subset of $M$ equipped with the subspace topology. 2. The target $t$ of $e$ is an open subset of $H$ equipped with the subspace topology. 3. The restriction of $e$ to $s$ and $t$ forms a homeomorphism between these subspaces. 4. This homeomorphism is a $G$-structomorphism, meaning that for any charts $c$ of $s$ and $c'$ of $t$, the composition $c' \circ e \circ c^{-1}$ (where defined) belongs to the structure groupoid $G$. In the case where the source of $e$ is empty, the structomorphism is trivially given by the unique homeomorphism between empty spaces.