Coinduced and quotient diffeologies

This file constructs the diffeology coinduced by an arbitrary map q : X → Q from a diffeological space. A map from an open subset of a Cartesian space to Q is a plot precisely when, near each point, it either lifts through q to a plot of X or is constant. This is the finest diffeology making q smooth, and a function out of Q is diffeologically smooth exactly when its composite with q is smooth.

When q is surjective, the constant case is subsumed by lifts, so the coinduced diffeology is the quotient diffeology: its plots are the maps that locally lift through q. The surjection q is then a subduction, and a diffeology on Q makes q a subduction exactly when it is the coinduced diffeology.

The D-topology of the coinduced diffeology is the topology coinduced by q from the D-topology of X. In particular, every subduction is a quotient map for the D-topologies, so a subduction that is also a quotient map for given topologies carries compatibility of the topology with the D-topology from its source to its target.

References

• P. Iglesias-Zemmour, Diffeology, Mathematical Surveys and Monographs 185, American Mathematical Society (2013), Articles 1.43--1.51, and Chapter 2 for the D-topology.

Local lifts or constants

def TauCeti.Diffeology.LocallyLiftsOrConst {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 or is locally constant on a subset if every point has an open neighborhood in the subset on which the map either locally lifts or is constant.

theorem TauCeti.Diffeology.locallyLiftsOrConst_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} : LocallyLiftsOrConst q u p ↔ ∀ z ∈ u, ∃ (v : Set (EuclideanSpace ℝ (Fin n))), IsOpen v ∧ z ∈ v ∧ v ⊆ u ∧ (LocallyLifts q v p ∨ ∃ (y : Q), Set.EqOn p (fun (x : EuclideanSpace ℝ (Fin n)) => y) v)

A map locally lifts or is locally constant on a subset exactly when every point has an open neighborhood in the subset on which the map either locally lifts or is constant.

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

Constant maps on an open set are local lifts or constants.

theorem TauCeti.Diffeology.LocallyLifts.locallyLiftsOrConst {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] {n : ℕ} {q : X → Q} {u : Set (EuclideanSpace ℝ (Fin n))} {p : EuclideanSpace ℝ (Fin n) → Q} (hp : LocallyLifts q u p) (hu : IsOpen u) : LocallyLiftsOrConst q u p

Local lifts are local lifts or constants.

theorem TauCeti.Diffeology.locallyLiftsOrConst_iff_locallyLifts {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] {n : ℕ} {q : X → Q} (hq : Function.Surjective q) {u : Set (EuclideanSpace ℝ (Fin n))} (hu : IsOpen u) {p : EuclideanSpace ℝ (Fin n) → Q} : LocallyLiftsOrConst q u p ↔ LocallyLifts q u p

Through a surjection, local lifts or constants on an open set are just local lifts.

theorem TauCeti.Diffeology.LocallyLiftsOrConst.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 : LocallyLiftsOrConst q u p) (hpp' : Set.EqOn p p' u) : LocallyLiftsOrConst q u p'

Local lifts or constants depend only on the restriction of the map to its domain.

theorem TauCeti.Diffeology.LocallyLiftsOrConst.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 : LocallyLiftsOrConst q u p) (hv : IsOpen v) (hf : ContDiffOn ℝ (↑⊤) f v) (hfu : Set.MapsTo f v u) : LocallyLiftsOrConst q v (p ∘ f)

Local lifts or constants are stable under smooth reparametrization on open subsets.

theorem TauCeti.Diffeology.locallyLiftsOrConst_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 ∧ LocallyLiftsOrConst q v p) : LocallyLiftsOrConst q u p

Locally holding local lifts or constants glue to local lifts or constants.

theorem TauCeti.Diffeology.LocallyLiftsOrConst.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 : LocallyLiftsOrConst q u p) (f : Q → Y) : LocallyLiftsOrConst (f ∘ q) u (f ∘ p)

Postcomposing both the map and the map lifted through with a function preserves local lifts or constants.

theorem TauCeti.Diffeology.LocallyLiftsOrConst.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 : LocallyLiftsOrConst q u p) (hq : Diffeology.DSmooth q) : IsPlotOn u p

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

The coinduced diffeology

@[instance_reducible]

def TauCeti.Diffeology.coinducedDiffeology {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] (q : X → Q) : DiffeologicalSpace Q

The diffeology coinduced by a map. Its plots are the maps that, near each point, lift through the map to plots of the source or are constant. This is the pushforward diffeology of Iglesias-Zemmour, Diffeology, Article 1.43.

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

A map is a plot of the coinduced diffeology exactly when, near each point, it lifts to a source plot or is constant.

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

For a surjection, a map is a plot of the coinduced diffeology exactly when it locally lifts through the surjection.

theorem TauCeti.Diffeology.dSmooth_coinducedDiffeology_rng {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] (q : X → Q) : Diffeology.DSmooth q

A map is smooth for the diffeology it coinduces.

theorem TauCeti.Diffeology.coinducedDiffeology_le_iff {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] (q : X → Q) {d : DiffeologicalSpace Q} : coinducedDiffeology q ≤ d ↔ Diffeology.DSmooth q

The coinduced diffeology is the finest diffeology making the map smooth.

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

A function from a coinduced diffeology is smooth exactly when its composite with the map is smooth.

Quotient diffeologies

theorem TauCeti.Diffeology.isSubduction_coinducedDiffeology {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] {q : X → Q} (hq : Function.Surjective q) : IsSubduction q

A surjection, equipped with the diffeology it coinduces, is a subduction.

theorem TauCeti.Diffeology.isSubduction_iff_eq_coinducedDiffeology {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] [d : DiffeologicalSpace Q] {q : X → Q} : IsSubduction q ↔ Function.Surjective q ∧ d = coinducedDiffeology q

A map is a subduction exactly when it is surjective and the target carries the coinduced diffeology.

D-topologies

theorem TauCeti.Diffeology.dTopology_coinducedDiffeology {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] (q : X → Q) : Diffeology.dTopology = TopologicalSpace.coinduced q Diffeology.dTopology

The D-topology of the coinduced diffeology is the topology coinduced from the D-topology of the source.

theorem TauCeti.Diffeology.IsSubduction.isQuotientMap_dTopology {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Q] {q : X → Q} (hq : IsSubduction q) : Topology.IsQuotientMap q

A subduction is a quotient map for the D-topologies.

theorem TauCeti.Diffeology.IsSubduction.isDTopologyCompatible {X : Type u_1} {Q : Type u_2} [DiffeologicalSpace X] [TopologicalSpace X] [Diffeology.IsDTopologyCompatible X] [TopologicalSpace Q] [DiffeologicalSpace Q] {q : X → Q} (hq : IsSubduction q) (h : Topology.IsQuotientMap q) : Diffeology.IsDTopologyCompatible Q

If the topology of the source of a subduction is its D-topology and the subduction is a quotient map for given topologies, then the topology of the target is its D-topology.