Diffeological manifolds

Some lemmas and theorems on manifolds as diffeological spaces, as defined in Orbifolds.Diffeology.LocallyModelled. The main purpose of this file is to show how this relates to the notion of smooth manifolds defined in mathlib , i.e. that those are indeed equivalent.

def IsManifold.toDiffeology {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] : DiffeologicalSpace M

The diffeology defined by a manifold structure on M, with the plots given by the maps that are smooth in the sense of mathlib's ContMDiff-API. This can not be an instance because IsManifold I M depends on I while DiffeologicalSpace M does not, and because it would probably lead to instance diamonds on things like products even if some workaround was found.

Equations

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

theorem isPlot_iff_contMDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [m : IsManifold I (↑⊤) M] {n : ℕ} {p : Eucl n → M} : IsPlot p ↔ ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) I (↑⊤) p

The plots of a manifold are by definition precisely the smooth maps.

theorem IsManifold.toDiffeology_eq_euclideanDiffeology {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : toDiffeology (modelWithCornersSelf ℝ E) E = euclideanDiffeology

def ModelWithCorners.toHomeomorphTarget {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) : H ≃ₜ ↑I.target

Equations

• I.toHomeomorphTarget = { toFun := fun (x : H) => ⟨↑I x, ⋯⟩, invFun := fun (y : ↑I.target) => I.invFun ↑y, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem IsManifold.dTop_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [tM : TopologicalSpace M] [ChartedSpace H M] [m : IsManifold I (↑⊤) M] : DTop ≤ tM

The D-topology on a manifold is always at least as fine as the usual topology.

instance instDTopCompatibleOfElemTarget {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [tH : TopologicalSpace H] (I : ModelWithCorners ℝ E H) [DTopCompatible ↑I.target] (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [m : IsManifold I (↑⊤) M] : have x := IsManifold.toDiffeology I M; DTopCompatible M

If the subspace topology and D-topology agree on the set H that the manifold is modelled on, the topology of the manifold agrees with the D-topology as well.

instance instDTopCompatibleOfFiniteDimensionalOfBoundarylessReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [hI : I.Boundaryless] (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [m : IsManifold I (↑⊤) M] : have x := IsManifold.toDiffeology I M; DTopCompatible M

In particular, the D-topology agrees with the standard topology on all manifolds modelled on a "boundaryless" model. TODO: It would be nice to have this (and all lemmas depending on it) for all boundaryless manifolds in the sense of BoundarylessManifold, such as manifolds with corners whose boundary just happens to be empty, but that would require either redoing the above lemma in slightly greater generality or passing from manifolds with empty boundary to manifolds modelled on a boundaryless model, both of which sound like a lot of work for something that is not a high priority.

theorem ContMDiff.dsmooth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [m : IsManifold I (↑⊤) M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [m' : IsManifold I' (↑⊤) N] {f : M → N} (hf : ContMDiff I I' (↑⊤) f) : DSmooth f

Every smooth map between manifolds is also D-smooth, i.e. this construction defines a functor of concrete categories.

theorem ContMDiffOn.dsmooth_restrict {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [m : IsManifold I (↑⊤) M] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [m' : IsManifold I' (↑⊤) N] {f : M → N} {s : Set M} (hf : ContMDiffOn I I' (↑⊤) f s) : have x := IsManifold.toDiffeology I M; have x_1 := IsManifold.toDiffeology I' N; DSmooth (s.restrict f)

Every map between manifolds that is smooth on a subset is also smooth diffeologically with respect to the subspace diffeology.

theorem IsOpen.dsmooth_iff_smoothOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [m : IsManifold I (↑⊤) M] [hI : I.Boundaryless] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} (N : Type u_6) [TopologicalSpace N] [ChartedSpace H' N] [m' : IsManifold I' (↑⊤) N] {f : M → N} {s : Set M} (hs : IsOpen s) : have x := IsManifold.toDiffeology I M; have x_1 := IsManifold.toDiffeology I' N; DSmooth (s.restrict f) ↔ ContMDiffOn I I' (↑⊤) f s

Every D-smooth map from a boundaryless manifold to another manifold is also smooth. This could probably be proven in quite a lot greater generality.

theorem DSmooth.smooth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [m : IsManifold I (↑⊤) M] [hI : I.Boundaryless] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {H' : Type u_5} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E' H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [m' : IsManifold I' (↑⊤) N] {f : M → N} (hf : DSmooth f) : ContMDiff I I' (↑⊤) f

Every D-smooth map from a boundaryless manifold to another manifold is also smooth. This could probably be proven in quite a lot greater generality.

theorem IsManifold.isDiffeologicalManifold {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [m : IsManifold I (↑⊤) M] [hI : I.Boundaryless] : IsDiffeologicalManifold (Module.finrank ℝ E) M

A finite-dimensional, boundaryless smooth manifold with corners in the sense of IsManifold is also a manifold in the sense of IsDiffeologicalManifold.

noncomputable def PartialEquiv.fromEquivSourceTarget {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (e : ↑s ≃ ↑t) (a : ↑s) : PartialEquiv α β

Equations

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

@[simp]

theorem PartialEquiv.fromEquivSourceTarget_apply {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (e : ↑s ≃ ↑t) (a : ↑s) (x : α) : ↑(fromEquivSourceTarget e a) x = if hx : x ∈ s then ↑(e ⟨x, hx⟩) else ↑(e a)

@[simp]

theorem PartialEquiv.fromEquivSourceTarget_target {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (e : ↑s ≃ ↑t) (a : ↑s) : (fromEquivSourceTarget e a).target = t

@[simp]

theorem PartialEquiv.fromEquivSourceTarget_symm_apply {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (e : ↑s ≃ ↑t) (a : ↑s) (y : β) : ↑(fromEquivSourceTarget e a).symm y = if hy : y ∈ t then ↑(e.symm ⟨y, hy⟩) else ↑a

@[simp]

theorem PartialEquiv.fromEquivSourceTarget_source {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (e : ↑s ≃ ↑t) (a : ↑s) : (fromEquivSourceTarget e a).source = s

@[simp]

theorem PartialEquiv.fromEquivSourceTarget_restrict {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (e : ↑s ≃ ↑t) (a : ↑s) : s.restrict ↑(fromEquivSourceTarget e a) = Subtype.val ∘ ⇑e

@[simp]

theorem PartialEquiv.fromEquivSourceTarget_symm_restrict {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (e : ↑s ≃ ↑t) (a : ↑s) : t.restrict ↑(fromEquivSourceTarget e a).symm = Subtype.val ∘ ⇑e.symm

@[simp]

theorem PartialEquiv.fromEquivSourceTarget_toEquiv {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (e : ↑s ≃ ↑t) (a : ↑s) : (fromEquivSourceTarget e a).toEquiv = e

noncomputable def PartialHomeomorph.fromHomeomorphSourceTarget {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} (e : ↑s ≃ₜ ↑t) (hs : IsOpen s) (ht : IsOpen t) (a : ↑s) : PartialHomeomorph α β

Equations

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

@[simp]

theorem PartialHomeomorph.fromHomeomorphSourceTarget_symm_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} (e : ↑s ≃ₜ ↑t) (hs : IsOpen s) (ht : IsOpen t) (a : ↑s) (y : β) : ↑(fromHomeomorphSourceTarget e hs ht a).symm y = if hy : y ∈ t then ↑(e.symm ⟨y, hy⟩) else ↑a

@[simp]

theorem PartialHomeomorph.fromHomeomorphSourceTarget_target {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} (e : ↑s ≃ₜ ↑t) (hs : IsOpen s) (ht : IsOpen t) (a : ↑s) : (fromHomeomorphSourceTarget e hs ht a).target = t

@[simp]

theorem PartialHomeomorph.fromHomeomorphSourceTarget_source {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} (e : ↑s ≃ₜ ↑t) (hs : IsOpen s) (ht : IsOpen t) (a : ↑s) : (fromHomeomorphSourceTarget e hs ht a).source = s

@[simp]

theorem PartialHomeomorph.fromHomeomorphSourceTarget_apply {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} (e : ↑s ≃ₜ ↑t) (hs : IsOpen s) (ht : IsOpen t) (a : ↑s) (x : α) : ↑(fromHomeomorphSourceTarget e hs ht a) x = if hx : x ∈ s then ↑(e ⟨x, hx⟩) else ↑(e a)

@[simp]

theorem PartialHomeomorph.fromHomeomorphSourceTarget_toPartialEquiv {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} (e : ↑s ≃ₜ ↑t) (hs : IsOpen s) (ht : IsOpen t) (a : ↑s) : (fromHomeomorphSourceTarget e hs ht a).toPartialEquiv = PartialEquiv.fromEquivSourceTarget e.toEquiv a

noncomputable def IsDiffeologicalManifold.toChartedSpace {M : Type u_1} [DiffeologicalSpace M] {n : ℕ} [hM : IsDiffeologicalManifold n M] : ChartedSpace (Eucl n) M

Charted space structure of a diffeological manifold, consisting of all local diffeomorphisms between M and Eucl n.

Equations

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