Diffeological manifolds

Some lemmas and theorems on manifolds as diffeological spaces, as defined in CatDG.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.

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.contMDiff {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 : BoundarylessManifold I M] {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 contMDiff_iff_dsmooth {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 : BoundarylessManifold I M] {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} : ContMDiff I I' (↑⊤) f ↔ DSmooth f

Maps between boundaryless manifolds are smooth iff they are diffeologically smooth.

def ContMDiffMap.equivDSmoothMap {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 : BoundarylessManifold I M] {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] : ContMDiffMap I I' M N ↑⊤ ≃ DSmoothMap M N

The canonical bijection ContMDiffMap I I' M N ∞ ≃ DSmoothMap M N stemming from the fact that functions between boundaryless manifolds are smooth iff they are diffeologically smooth.

Equations

• ContMDiffMap.equivDSmoothMap = { toFun := fun (f : ContMDiffMap I I' M N ↑⊤) => { toFun := ⇑f, dsmooth := ⋯ }, invFun := fun (f : DSmoothMap M N) => ⟨⇑f, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

instance instDTopCompatibleOfFiniteDimensionalOfBoundarylessManifoldReal {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 : BoundarylessManifold I M] : have x := IsManifold.toDiffeology I M; DTopCompatible M

The D-topology agrees with the standard topology on all boundaryless manifolds.

Note that this is at least a priori not a special case of the previous instance, because it allows for the spaces that the manifolds are modelled on to have boundary and corners, even if the manifolds do not. It might however still turn out to be a special case if we can prove that every model with corners is DTopCompatible.

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_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_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_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_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_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 OpenPartialHomeomorph.fromHomeomorphSourceTarget {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} (e : ↑s ≃ₜ ↑t) (hs : IsOpen s) (ht : IsOpen t) (a : ↑s) : OpenPartialHomeomorph α β

Equations

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

@[simp]

theorem OpenPartialHomeomorph.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 OpenPartialHomeomorph.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 OpenPartialHomeomorph.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 OpenPartialHomeomorph.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 OpenPartialHomeomorph.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.