Subductions

This file defines when a map to a target locally lifts through a map from a diffeological space, and uses it to define subductions: smooth surjections through which every plot of the target locally lifts to a plot of the source. A function out of the target of a subduction is diffeologically smooth exactly when its composite with the subduction is smooth.

References

• P. Iglesias-Zemmour, Diffeology, Mathematical Surveys and Monographs 185, American Mathematical Society (2013), Articles 1.46--1.51.

Local lifts

def TauCeti.Diffeology.LocallyLifts {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] (q : X → Q) {n : ℕ} (u : Set (EuclideanSpace ℝ (Fin n))) (p : EuclideanSpace ℝ (Fin n) → Q) : Prop

A map to the target locally lifts through a map on a subset if every point has an open neighborhood in the subset on which the map agrees with the image of a source plot.

theorem TauCeti.Diffeology.locallyLifts_iff {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] {n : ℕ} {q : X → Q} {u : Set (EuclideanSpace ℝ (Fin n))} {p : EuclideanSpace ℝ (Fin n) → Q} : LocallyLifts q u p ↔ ∀ z ∈ u, ∃ (v : Set (EuclideanSpace ℝ (Fin n))), IsOpen v ∧ z ∈ v ∧ v ⊆ u ∧ ∃ (lift : EuclideanSpace ℝ (Fin n) → X), IsPlotOn v lift ∧ Set.EqOn (q ∘ lift) p v

A map locally lifts on a subset exactly when every point has an open neighborhood in the subset on which the map agrees with the image of a source plot.

theorem TauCeti.Diffeology.IsPlotOn.locallyLifts_comp {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] {n : ℕ} (q : X → Q) {u : Set (EuclideanSpace ℝ (Fin n))} {lift : EuclideanSpace ℝ (Fin n) → X} (hlift : IsPlotOn u lift) (hu : IsOpen u) : LocallyLifts q u (q ∘ lift)

The image of a plot on an open subset locally lifts through the map on that subset.

theorem TauCeti.Diffeology.locallyLifts_const {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] {n : ℕ} (q : X → Q) {u : Set (EuclideanSpace ℝ (Fin n))} (hu : IsOpen u) (x : X) : LocallyLifts q u fun (x_1 : EuclideanSpace ℝ (Fin n)) => q x

The constant map at an image point locally lifts through the map on every open subset.

theorem TauCeti.Diffeology.LocallyLifts.congr {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] {n : ℕ} {q : X → Q} {u : Set (EuclideanSpace ℝ (Fin n))} {p p' : EuclideanSpace ℝ (Fin n) → Q} (hp : LocallyLifts q u p) (hpp' : Set.EqOn p p' u) : LocallyLifts q u p'

The local lifting property depends only on the restriction of the map to its domain.

theorem TauCeti.Diffeology.LocallyLifts.mono {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] {n : ℕ} {q : X → Q} {u v : Set (EuclideanSpace ℝ (Fin n))} {p : EuclideanSpace ℝ (Fin n) → Q} (hp : LocallyLifts q u p) (hv : IsOpen v) (hvu : v ⊆ u) : LocallyLifts q v p

The local lifting property passes to open subsets.

theorem TauCeti.Diffeology.LocallyLifts.comp_contDiffOn {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] {n m : ℕ} {q : X → Q} {u : Set (EuclideanSpace ℝ (Fin n))} {v : Set (EuclideanSpace ℝ (Fin m))} {p : EuclideanSpace ℝ (Fin n) → Q} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)} (hp : LocallyLifts q u p) (hv : IsOpen v) (hf : ContDiffOn ℝ (↑⊤) f v) (hfu : Set.MapsTo f v u) : LocallyLifts q v (p ∘ f)

Locally liftable maps are stable under smooth reparametrization on open subsets.

theorem TauCeti.Diffeology.locallyLifts_of_locally {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] {n : ℕ} {q : X → Q} {u : Set (EuclideanSpace ℝ (Fin n))} {p : EuclideanSpace ℝ (Fin n) → Q} (hu : IsOpen u) (hp : ∀ z ∈ u, ∃ (v : Set (EuclideanSpace ℝ (Fin n))), IsOpen v ∧ z ∈ v ∧ LocallyLifts q v p) : LocallyLifts q u p

A locally local lifting property glues to a local lifting property.

theorem TauCeti.Diffeology.LocallyLifts.comp_left {X : Type u_1} {Q : Type u_2} {Y : Type u_3} [DiffeologicalSpace X] {n : ℕ} {q : X → Q} {u : Set (EuclideanSpace ℝ (Fin n))} {p : EuclideanSpace ℝ (Fin n) → Q} (hp : LocallyLifts q u p) (f : Q → Y) : LocallyLifts (f ∘ q) u (f ∘ p)

Postcomposing both the map and the map lifted through with a function preserves the local lifting property.

theorem TauCeti.Diffeology.LocallyLifts.isPlotOn {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Q] {n : ℕ} {q : X → Q} {u : Set (EuclideanSpace ℝ (Fin n))} {p : EuclideanSpace ℝ (Fin n) → Q} (hp : LocallyLifts q u p) (hq : Diffeology.DSmooth q) : IsPlotOn u p

A map that locally lifts through a smooth map is a plot on its domain.

Subductions

structure TauCeti.Diffeology.IsSubduction {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Q] (q : X → Q) : Prop

A smooth surjection is a subduction if every target plot locally lifts to a source plot.

• surjective : Function.Surjective q

  A subduction is surjective.

• dSmooth : Diffeology.DSmooth q

  A subduction is smooth.

• locallyLifts {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → Q} : Diffeology.IsPlot p → LocallyLifts q Set.univ p

  Every plot of the target locally lifts through a subduction.

theorem TauCeti.Diffeology.IsSubduction.isPlot_iff {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Q] {q : X → Q} (hq : IsSubduction q) {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → Q} : Diffeology.IsPlot p ↔ LocallyLifts q Set.univ p

The plots of the target of a subduction are exactly the maps that locally lift through it.

theorem TauCeti.Diffeology.IsSubduction.dSmooth_iff {X : Type u_1} {Q : Type u_2} {Y : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Q] [DiffeologicalSpace Y] {q : X → Q} (hq : IsSubduction q) (f : Q → Y) : Diffeology.DSmooth f ↔ Diffeology.DSmooth (f ∘ q)

Descent along a subduction: a function from the target is smooth exactly when its composite with the subduction is smooth.