Continuous diffeology

Defines the continuous diffeology on topological spaces, i.e. the diffeology consisting of all continuous plots. On the level of categories, this forms a right-adjoint to the D-topology functor (which is proven in Orbifolds.Diffeology.DiffSp); on the level of individual types, this means that it forms a Galois connection with @DTop X : DiffeologicalSpace X → TopologicalSpace X. This is also used to show a few more properties of the D-topology. See https://ncatlab.org/nlab/show/adjunction+between+topological+spaces+and+diffeological+spaces.

def continuousDiffeology (X : Type u) [TopologicalSpace X] : DiffeologicalSpace X

The continuous diffeology on a topological space X.

Equations

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

theorem dTop_continuousDiffeology {X : Type u} [TopologicalSpace X] : DTop = TopologicalSpace.deltaGenerated X

The D-topology of the continuous diffeology is the delta-generification of the original topology.

theorem dTop_continuousDiffeology_eq_self {X : Type u} [t : TopologicalSpace X] [DeltaGeneratedSpace X] : DTop = t

For delta-generated spaces, the D-topology of the continuous diffeology is the topology itself.

def withContinuousDiffeology (X : Type u) [TopologicalSpace X] : Type u

Type synonym to get equipped with the continuous diffeology.

Equations

• withContinuousDiffeology X = X

instance instDiffeologicalSpaceWithContinuousDiffeology (X : Type u) [TopologicalSpace X] : DiffeologicalSpace (withContinuousDiffeology X)

Equations

• instDiffeologicalSpaceWithContinuousDiffeology X = continuousDiffeology X

theorem Continuous.dsmooth {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) : DSmooth f

Every continuous map is smooth with respect to the continuous diffeologies.

theorem Continuous.dsmooth' {X Y : Type u} {dX : DiffeologicalSpace X} {tY : TopologicalSpace Y} {f : X → Y} (hf : Continuous f) : DSmooth f

Every continuous map into a space carrying the continuous diffeology is smooth.

theorem dTop_le_iff_le_continuousDiffeology {X : Type u} {d : DiffeologicalSpace X} {t : TopologicalSpace X} : DTop ≤ t ↔ d ≤ continuousDiffeology X

theorem gc_dTop (X : Type u_1) : GaloisConnection (@DTop X) (@continuousDiffeology X)

The D-topology and continuous diffeology form a Galois connection between diffeologies and topologies on X.

theorem dTop_mono {X : Type u_1} {d₁ d₂ : DiffeologicalSpace X} (h : d₁ ≤ d₂) : DTop ≤ DTop

theorem continuousDiffeology_mono {X : Type u_1} {t₁ t₂ : TopologicalSpace X} (h : t₁ ≤ t₂) : continuousDiffeology X ≤ continuousDiffeology X

theorem dTop_continuousDiffeology_le {X : Type u} {t : TopologicalSpace X} : DTop ≤ t

theorem le_continuousDiffeology_dTop {X : Type u} {d : DiffeologicalSpace X} : d ≤ continuousDiffeology X

theorem dTop_sup {X : Type u} (d₁ d₂ : DiffeologicalSpace X) : DTop = DTop ⊔ DTop

theorem dTop_iSup {X : Type u} {ι : Type u_1} {D : ι → DiffeologicalSpace X} : DTop = ⨆ (i : ι), DTop

theorem dTop_sSup {X : Type u} {D : Set (DiffeologicalSpace X)} : DTop = ⨆ d ∈ D, DTop

theorem continuousDiffeology_inf {X : Type u} (t₁ t₂ : TopologicalSpace X) : continuousDiffeology X = continuousDiffeology X ⊓ continuousDiffeology X

theorem continuousDiffeology_iInf {X : Type u} {ι : Type u_1} {T : ι → TopologicalSpace X} : continuousDiffeology X = ⨅ (i : ι), continuousDiffeology X

theorem continuousDiffeology_sInf {X : Type u} {T : Set (TopologicalSpace X)} : continuousDiffeology X = ⨅ t ∈ T, continuousDiffeology X

theorem dTop_generateFrom_eq_iSup {X : Type u_1} {g : Set ((n : ℕ) × (Eucl n → X))} : DTop = ⨆ p ∈ g, TopologicalSpace.coinduced p.snd inferInstance

The D-topology of the diffeology generated by g is coinduced by all plots in g.

theorem isOpen_dTop_generateFrom {X : Type u_1} {g : Set ((n : ℕ) × (Eucl n → X))} {u : Set X} : IsOpen u ↔ ∀ (n : ℕ) (p : Eucl n → X), ⟨n, p⟩ ∈ g → IsOpen (p ⁻¹' u)

A version of dTop_generateFrom_eq_iSup stated in terms of individual open sets.