Locally Modelled Spaces

Diffeological space that are locally modelled on a family of other diffeological spaces. This mainly functions are infrastructure for manifolds and orbifolds, setting up their definitions and a few basic facts they have in common.

class LocallyModelled {ι : Type u_1} (M : ι → Type u_2) [(i : ι) → DiffeologicalSpace (M i)] (X : Type u_3) [DiffeologicalSpace X] : Prop

A diffeological space is locally modelled by a family of diffeological spaces if each point in it has a neighbourhood that's diffeomorphic to a space in the family.

• locally_modelled (x : X) : ∃ (u : Set X), IsOpen u ∧ x ∈ u ∧ ∃ (i : ι) (v : Set (M i)), IsOpen v ∧ Nonempty (↑u ᵈ≃ ↑v)

@[reducible, inline]

abbrev IsDiffeologicalManifold (n : ℕ) (X : Type u_1) [DiffeologicalSpace X] : Prop

A diffeological space is a manifold if it is locally modelled by R^n. We do not require Hausdorffness or second-countability here.

Equations

• IsDiffeologicalManifold n X = LocallyModelled (fun (x : Unit) => Eucl n) X

@[reducible, inline]

abbrev IsManifoldWithBoundary (n : ℕ) [Zero (Fin n)] (X : Type u_1) [DiffeologicalSpace X] : Prop

A diffeological space is a manifold with boundary if it is locally modelled by the half-space H^n. We do not require Hausdorffness or second-countability here.

Equations

• IsManifoldWithBoundary n X = LocallyModelled (fun (x : Unit) => ↑{x : Eucl n | 0 ≤ x 0}) X

@[reducible, inline]

abbrev IsOrbifold (n : ℕ) (X : Type u_1) [DiffeologicalSpace X] : Prop

A diffeological space is an orbifold if it is locally modelled by quotients of R^n by finite subgroups of GL(n).

Equations

• IsOrbifold n X = LocallyModelled (fun (Γ : ↑{Γ : Subgroup (Eucl n ≃ₗ[ℝ] Eucl n) | Finite ↥Γ}) => MulAction.orbitRel.Quotient (↥↑Γ) (Eucl n)) X

theorem IsOpen.locallyModelled {X : Type u_1} {ι : Type u_2} [DiffeologicalSpace X] {M : ι → Type u_3} [(i : ι) → DiffeologicalSpace (M i)] (h : LocallyModelled M X) {u : Set X} (hu : IsOpen u) : LocallyModelled M ↑u

Any D-open subset of a locally modelled space is locally modelled by the same family of spaces.

theorem IsOpen.isDiffeologicalManifold {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} (h : IsDiffeologicalManifold n X) {u : Set X} (hu : IsOpen u) : IsDiffeologicalManifold n ↑u

Any D-open subset of a diffeological manifold is a diffeological manifold.

theorem IsOpen.isManifoldWithBoundary {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} [Zero (Fin n)] (h : IsManifoldWithBoundary n X) {u : Set X} (hu : IsOpen u) : IsManifoldWithBoundary n ↑u

Any D-open subset of a diffeological manifold with boundary is a diffeological manifold with boundary.

theorem IsOpen.isOrbifold {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} [Zero (Fin n)] (h : IsOrbifold n X) {u : Set X} (hu : IsOpen u) : IsOrbifold n ↑u

Any D-open subset of a diffeological orbifold is a diffeological orbifold.

instance instIsDiffeologicalManifoldEucl {n : ℕ} : IsDiffeologicalManifold n (Eucl n)

Eucl n is a diffeological manifold.

instance instIsManifoldWithBoundaryOfIsDiffeologicalManifold {n : ℕ} {X : Type u_1} [Zero (Fin n)] [DiffeologicalSpace X] [hm : IsDiffeologicalManifold n X] : IsManifoldWithBoundary n X

Any diffeological manifold is also a diffeological manifold with boundary.

instance instIsOrbifoldOfIsDiffeologicalManifold {n : ℕ} {X : Type u_1} [DiffeologicalSpace X] [hm : IsDiffeologicalManifold n X] : IsOrbifold n X

Any diffeological manifold is also a diffeological orbifold.

theorem LocallyModelled.locallyCompactSpace {X : Type u_1} {ι : Type u_2} [DiffeologicalSpace X] {M : ι → Type u_3} [(i : ι) → TopologicalSpace (M i)] [(i : ι) → DiffeologicalSpace (M i)] [∀ (i : ι), DTopCompatible (M i)] [∀ (i : ι), LocallyCompactSpace (M i)] (h : LocallyModelled M X) : LocallyCompactSpace X

Spaces that are modelled on locally compact spaces are locally compact.

instance instLocallyCompactSpaceQuotientSubtypeLinearEquivRealIdEuclMemSubgroupValSetSetOfFinite {n : ℕ} {Γ : ↑{Γ : Subgroup (Eucl n ≃ₗ[ℝ] Eucl n) | Finite ↥Γ}} : LocallyCompactSpace (MulAction.orbitRel.Quotient (↥↑Γ) (Eucl n))

The quotient spaces that orbifolds are modelled on are locally compact.

theorem IsOrbifold.locallyCompactSpace {X : Type u_1} [TopologicalSpace X] [DiffeologicalSpace X] [DTopCompatible X] {n : ℕ} [hX : IsOrbifold n X] : LocallyCompactSpace X

Orbifolds are locally compact. Not an instance because lean can't infer typeclasses that don't depend on n from ones that do. TODO: solve by allowing orbifolds of mixed dimension?