Quotient diffeologies on quotient types

This file equips the quotient Quotient s of a diffeological space by a setoid with the quotient diffeology, the diffeology coinduced by Quotient.mk s. It is the diffeological counterpart of Mathlib's quotient topology instTopologicalSpaceQuotient. A map from a Cartesian space to the quotient is a plot exactly when it locally lifts to plots of the space, the projection is a subduction, and a function out of the quotient is smooth exactly when its composite with the projection is.

Since MulAction.orbitRel.Quotient G X is by definition the quotient by the orbit relation, this is in particular the diffeology on the orbit space of a group action, for instance the coarse smooth structure on the quotient of a chart by a finite group acting smoothly. No finiteness or smoothness of the action is needed for the statements here.

The D-topology of the quotient diffeology is the quotient of the D-topology of the space. Hence, whenever the topology of the space is its D-topology, the D-topology of the quotient is the ordinary quotient topology, so the quotient diffeology is compatible with Mathlib's topology on the quotient type (TauCeti.Diffeology.instIsDTopologyCompatibleQuotient).

References

• P. Iglesias-Zemmour, Diffeology, Mathematical Surveys and Monographs 185, American Mathematical Society (2013), Article 1.50 for quotient diffeologies and Chapter 2 for the D-topology.

@[instance_reducible]

instance TauCeti.Diffeology.instDiffeologicalSpaceQuotient {X : Type u_1} [DiffeologicalSpace X] (s : Setoid X) : DiffeologicalSpace (Quotient s)

The quotient diffeology on a quotient type: the diffeology coinduced by the projection.

theorem TauCeti.Diffeology.isPlot_quotient_iff {X : Type u_1} [DiffeologicalSpace X] (s : Setoid X) {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → Quotient s} : Diffeology.IsPlot p ↔ LocallyLifts (Quotient.mk s) Set.univ p

A map is a plot of the quotient exactly when it locally lifts through the projection.

theorem TauCeti.Diffeology.isSubduction_quotient_mk {X : Type u_1} [DiffeologicalSpace X] (s : Setoid X) : IsSubduction (Quotient.mk s)

The projection onto a quotient is a subduction.

theorem TauCeti.Diffeology.dSmooth_quotient_mk {X : Type u_1} [DiffeologicalSpace X] (s : Setoid X) : Diffeology.DSmooth (Quotient.mk s)

The projection onto a quotient is smooth.

@[simp]

theorem TauCeti.Diffeology.dSmooth_quotient_lift_iff {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {s : Setoid X} {f : X → Y} (hs : ∀ (a b : X), a ≈ b → f a = f b) : Diffeology.DSmooth (Quotient.lift f hs) ↔ Diffeology.DSmooth f

Descent to a quotient: a function out of a quotient is smooth exactly when the function on the space it descends from is smooth.

theorem Diffeology.DSmooth.quotient_lift {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {s : Setoid X} {f : X → Y} (hf : DSmooth f) (hs : ∀ (a b : X), a ≈ b → f a = f b) : DSmooth (Quotient.lift f hs)

A smooth function that is constant on equivalence classes descends to a smooth function on the quotient.

theorem Diffeology.DSmooth.quotient_map {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {s : Setoid X} {t : Setoid Y} {f : X → Y} (hf : DSmooth f) (h : ∀ ⦃a b : X⦄, a ≈ b → f a ≈ f b) : DSmooth (Quotient.map f h)

A smooth map respecting two equivalence relations induces a smooth map of quotients.

theorem TauCeti.Diffeology.isQuotientMap_dTopology_quotient_mk {X : Type u_1} [DiffeologicalSpace X] {s : Setoid X} : Topology.IsQuotientMap (Quotient.mk s)

The D-topology of a quotient diffeology is the quotient of the D-topology of the space.

instance TauCeti.Diffeology.instIsDTopologyCompatibleQuotient {X : Type u_1} [DiffeologicalSpace X] {s : Setoid X} [TopologicalSpace X] [Diffeology.IsDTopologyCompatible X] : Diffeology.IsDTopologyCompatible (Quotient s)

If the topology of a space is its D-topology, then the D-topology of a quotient is the quotient topology.