Reflexive diffeological spaces

This file deals with diffeological spaces X that are reflexive in the sense that they are fixed points of the adjunction between diffeological spaces and differential space, i.e. whose diffeology is induced by the differential space structure that it induces. Reflexive diffeological spaces correspond exactly to Frölicher spaces - see https://arxiv.org/abs/1712.04576v2.

Note that while differential spaces are certainly related we have not formalised them here, and instead went with a more explicit characterisation of reflexive diffeological spaces.

class ReflexiveDiffeologicalSpace (X : Type u_1) [DiffeologicalSpace X] : Prop

A diffeological space is called reflexive if the diffeology induced by the differential structure induced by the diffeology is again the diffeology itself. Since we don't have differential spaces yet, this is formulated as every function p : Eucl n → X for which all compositions with functions X → ℝ are smooth being a plot.

• isPlot_if {n : ℕ} (p : Eucl n → X) : (∀ (f : X → ℝ), DSmooth f → DSmooth (f ∘ p)) → IsPlot p

instance instReflexiveDiffeologicalSpaceOfFiniteDimensionalRealOfContDiffCompatible {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [DiffeologicalSpace X] [ContDiffCompatible X] : ReflexiveDiffeologicalSpace X

Finite-dimensional normed spaces with their natural diffeologies are reflexive.

def DiffeologicalSpace.toReflexive {X : Type u_1} {d : DiffeologicalSpace X} : DiffeologicalSpace X

The diffeology induced by the differential space structure induced by the diffeology d.

Equations

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

theorem dsmooth_toReflexive_iff {X : Type u_1} {Y : Type u_2} {dX : DiffeologicalSpace X} [DiffeologicalSpace Y] [ReflexiveDiffeologicalSpace Y] {f : X → Y} : DSmooth f ↔ DSmooth f

A function X → Y into a reflexive diffeological space is smooth with respect to dX : DiffeologicalSpace X iff it is smooth with respect to dX.toReflexive.

theorem reflexiveDiffeologicalSpace_toReflexive {X : Type u_1} {d : DiffeologicalSpace X} : ReflexiveDiffeologicalSpace X

d.toReflexive is a reflexive diffeology for any diffeology d.

theorem DiffeologicalSpace.le_toReflexive {X : Type u_1} {d : DiffeologicalSpace X} : d ≤ toReflexive

d.toReflexive is always at least as coarse as d.

theorem DiffeologicalSpace.eq_toReflexive_iff {X : Type u_1} {d : DiffeologicalSpace X} : d = toReflexive ↔ ReflexiveDiffeologicalSpace X

def ReflexiveDiffeologicalSpace.of (X : Type u_1) : Type u_1

Type synonym equipped with the reflexive diffeology induced by the diffeology on X.

Equations

• ReflexiveDiffeologicalSpace.of X = X

instance ReflexiveDiffeologicalSpace.instDiffeologicalSpaceOf {X : Type u_1} [d : DiffeologicalSpace X] : DiffeologicalSpace (of X)

Equations

• ReflexiveDiffeologicalSpace.instDiffeologicalSpaceOf = DiffeologicalSpace.toReflexive

instance ReflexiveDiffeologicalSpace.instOf {X : Type u_1} [DiffeologicalSpace X] : ReflexiveDiffeologicalSpace (of X)

def ReflexiveDiffeologicalSpace.unit {X : Type u_1} : X → of X

The natural map from a diffeological space to its type synonym with the reflexive diffeology.

Equations

• ReflexiveDiffeologicalSpace.unit = id

theorem ReflexiveDiffeologicalSpace.dsmooth_unit {X : Type u_1} [DiffeologicalSpace X] : DSmooth unit

structure ReflexiveDiffeology (X : Type u_1) extends DiffeologicalSpace X, ReflexiveDiffeologicalSpace X : Type u_1

The lattice of all reflexive diffeologies on X.

• plots (n : ℕ) : Set (Eucl n → X)
• constant_plots {n : ℕ} (x : X) : (fun (x_1 : Eucl n) => x) ∈ plots n
• plot_reparam {n m : ℕ} {p : Eucl m → X} {f : Eucl n → Eucl m} : p ∈ plots m → ContDiff ℝ (↑⊤) f → p ∘ f ∈ plots n
• locality {n : ℕ} {p : Eucl n → X} : (∀ (x : Eucl n), ∃ (u : Set (Eucl n)), IsOpen u ∧ x ∈ u ∧ ∀ {m : ℕ} {f : Eucl m → Eucl n}, (∀ (x : Eucl m), f x ∈ u) → ContDiff ℝ (↑⊤) f → p ∘ f ∈ plots m) → p ∈ plots n
• dTopology : TopologicalSpace X
• isOpen_iff_preimages_plots {u : Set X} : TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ}, ∀ p ∈ plots n, TopologicalSpace.IsOpen (p ⁻¹' u)
• isPlot_if {n : ℕ} (p : Eucl n → X) : (∀ (f : X → ℝ), DSmooth f → DSmooth (f ∘ p)) → IsPlot p

theorem ReflexiveDiffeology.toDiffeologicalSpace_injective {X : Type u_1} : Function.Injective toDiffeologicalSpace

theorem ReflexiveDiffeology.ext' {X : Type u_1} {d₁ d₂ : ReflexiveDiffeology X} (h : d₁.toDiffeologicalSpace = d₂.toDiffeologicalSpace) : d₁ = d₂

theorem ReflexiveDiffeology.ext'_iff {X : Type u_1} {d₁ d₂ : ReflexiveDiffeology X} : d₁ = d₂ ↔ d₁.toDiffeologicalSpace = d₂.toDiffeologicalSpace

instance instPartialOrderReflexiveDiffeology {X : Type u_1} : PartialOrder (ReflexiveDiffeology X)

Equations

• instPartialOrderReflexiveDiffeology = PartialOrder.lift ReflexiveDiffeology.toDiffeologicalSpace ⋯

@[simp]

theorem ReflexiveDiffeology.toDiffeologicalSpace_le {X : Type u_1} {d₁ d₂ : ReflexiveDiffeology X} : d₁.toDiffeologicalSpace ≤ d₂.toDiffeologicalSpace ↔ d₁ ≤ d₂

def DiffeologicalSpace.toReflexiveDiffeology {X : Type u_1} (d : DiffeologicalSpace X) : ReflexiveDiffeology X

Equations

• d.toReflexiveDiffeology = { toDiffeologicalSpace := DiffeologicalSpace.toReflexive, toReflexiveDiffeologicalSpace := ⋯ }

theorem DiffeologicalSpace.gc_toReflexiveDiffeology (X : Type u_1) : GaloisConnection toReflexiveDiffeology ReflexiveDiffeology.toDiffeologicalSpace

def DiffeologicalSpace.giToReflexiveDiffeology (X : Type u_1) : GaloisInsertion toReflexiveDiffeology ReflexiveDiffeology.toDiffeologicalSpace

The Galois insertion of reflexive diffeologies into all diffeologies on a type.

Equations

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

instance instCompleteLatticeReflexiveDiffeology {X : Type u_1} : CompleteLattice (ReflexiveDiffeology X)

Equations

• instCompleteLatticeReflexiveDiffeology = (DiffeologicalSpace.giToReflexiveDiffeology X).liftCompleteLattice

theorem DiffeologicalSpace.toReflexiveDiffeology_sup {X : Type u_1} (d₁ d₂ : DiffeologicalSpace X) : (d₁ ⊔ d₂).toReflexiveDiffeology = d₁.toReflexiveDiffeology ⊔ d₂.toReflexiveDiffeology

theorem DiffeologicalSpace.toReflexiveDiffeology_iSup {X : Type u_1} {ι : Type u_2} {D : ι → DiffeologicalSpace X} : (⨆ (i : ι), D i).toReflexiveDiffeology = ⨆ (i : ι), (D i).toReflexiveDiffeology

theorem DiffeologicalSpace.toReflexiveDiffeology_sSup {X : Type u_1} {D : Set (DiffeologicalSpace X)} : (sSup D).toReflexiveDiffeology = ⨆ d ∈ D, d.toReflexiveDiffeology

theorem ReflexiveDiffeology.toDiffeologicalSpace_inf {X : Type u_1} (d₁ d₂ : ReflexiveDiffeology X) : (d₁ ⊓ d₂).toDiffeologicalSpace = d₁.toDiffeologicalSpace ⊓ d₂.toDiffeologicalSpace

theorem ReflexiveDiffeology.toDiffeologicalSpace_iInf {X : Type u_1} {ι : Type u_2} {D : ι → ReflexiveDiffeology X} : (⨅ (i : ι), D i).toDiffeologicalSpace = ⨅ (i : ι), (D i).toDiffeologicalSpace

theorem ReflexiveDiffeology.toDiffeologicalSpace_sInf {X : Type u_1} {D : Set (ReflexiveDiffeology X)} : (sInf D).toDiffeologicalSpace = ⨅ d ∈ D, d.toDiffeologicalSpace

theorem ReflexiveDiffeologicalSpace.inf {X : Type u_1} {d₁ d₂ : DiffeologicalSpace X} (h₁ : ReflexiveDiffeologicalSpace X) (h₂ : ReflexiveDiffeologicalSpace X) : ReflexiveDiffeologicalSpace X

Infima (in the lattice of diffeologies) of reflexive diffeologies are again reflexive.

theorem ReflexiveDiffeologicalSpace.iInf {X : Type u_1} {ι : Type u_2} {D : ι → DiffeologicalSpace X} (h : ∀ (i : ι), ReflexiveDiffeologicalSpace X) : ReflexiveDiffeologicalSpace X

Infima (in the lattice of diffeologies) of reflexive diffeologies are again reflexive.