@[reducible, inline]

abbrev Eucl (n : ℕ) : Type

Equations

• Eucl n = EuclideanSpace ℝ (Fin n)

class DiffeologicalSpace (X : Type u_1) : Type u_1

A diffeology on X, given by the smooth functions (or "plots") from ℝⁿ to 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)

def DTop {X : Type u_1} [DiffeologicalSpace X] : TopologicalSpace X

D-topology of a diffeological space. This is a definition rather than an instance because the D-topology might not agree with already registered topologies like the one on normed spaces.

Equations

• DTop = DiffeologicalSpace.dTopology

def IsPlot {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} (p : Eucl n → X) : Prop

Equations

• IsPlot p = (p ∈ DiffeologicalSpace.plots n)

def DSmooth {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (f : X → Y) : Prop

A function between diffeological spaces is smooth iff composition with it preserves smoothness of plots.

Equations

• DSmooth f = ∀ (n : ℕ) (p : Eucl n → X), IsPlot p → IsPlot (f ∘ p)

def DTop_of : Lean.ParserDescr

Equations

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

def IsPlot_of : Lean.ParserDescr

Equations

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

def DSmooth_of : Lean.ParserDescr

Equations

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

theorem DiffeologicalSpace.ext {X : Type u_1} {d₁ d₂ : DiffeologicalSpace X} (h : @IsPlot X d₁ = @IsPlot X d₂) : d₁ = d₂

theorem DiffeologicalSpace.ext_iff {X : Type u_1} {d₁ d₂ : DiffeologicalSpace X} : d₁ = d₂ ↔ @IsPlot X d₁ = @IsPlot X d₂

theorem isPlot_const {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {x : X} : IsPlot fun (x_1 : Eucl n) => x

theorem isPlot_reparam {X : Type u_1} [DiffeologicalSpace X] {n m : ℕ} {p : Eucl m → X} {f : Eucl n → Eucl m} (hp : IsPlot p) (hf : ContDiff ℝ (↑⊤) f) : IsPlot (p ∘ f)

theorem isOpen_iff_preimages_plots {X : Type u_1} [DiffeologicalSpace X] {u : Set X} : IsOpen u ↔ ∀ (n : ℕ) (p : Eucl n → X), IsPlot p → IsOpen (p ⁻¹' u)

theorem IsPlot.continuous {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {p : Eucl n → X} (hp : IsPlot p) : Continuous p

theorem DSmooth.continuous {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {f : X → Y} (hf : DSmooth f) : Continuous f

theorem dsmooth_iff {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {f : X → Y} : DSmooth f ↔ ∀ (n : ℕ) (p : Eucl n → X), IsPlot p → IsPlot (f ∘ p)

theorem dsmooth_id {X : Type u_1} [DiffeologicalSpace X] : DSmooth id

theorem dsmooth_id' {X : Type u_1} [DiffeologicalSpace X] : DSmooth fun (x : X) => x

theorem DSmooth.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : DSmooth g) (hf : DSmooth f) : DSmooth (g ∘ f)

theorem DSmooth.comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : DSmooth g) (hf : DSmooth f) : DSmooth fun (x : X) => g (f x)

theorem dsmooth_const {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {y : Y} : DSmooth fun (x : X) => y

def DiffeologicalSpace.withDTopology {X : Type u_4} (d : DiffeologicalSpace X) (t : TopologicalSpace X) (h : DTop = t) : DiffeologicalSpace X

Replaces the D-topology of a diffeology with another topology equal to it. Useful to construct diffeologies with better definitional equalities.

Equations

• d.withDTopology t h = { plots := DiffeologicalSpace.plots, constant_plots := ⋯, plot_reparam := ⋯, locality := ⋯, dTopology := t, isOpen_iff_preimages_plots := ⋯ }

theorem DiffeologicalSpace.withDTopology_eq {X : Type u_4} {d : DiffeologicalSpace X} {t : TopologicalSpace X} {h : DTop = t} : d.withDTopology t h = d

structure DiffeologicalSpace.CorePlotsOn (X : Type u_4) : Type u_4

A structure with plots specified on open subsets of ℝⁿ rather than ℝⁿ itself. Useful for constructing diffeologies, as it often makes the locality condition easiert to prove.

• isPlotOn {n : ℕ} {u : Set (Eucl n)} (hu : IsOpen u) : (Eucl n → X) → Prop
• isPlotOn_congr {n : ℕ} {u : Set (Eucl n)} (hu : IsOpen u) {p q : Eucl n → X} (h : Set.EqOn p q u) : self.isPlotOn hu p ↔ self.isPlotOn hu q
• isPlot {n : ℕ} : (Eucl n → X) → Prop

  The predicate that the diffeology built from this structure will use. Can be overwritten to allow for better definitional equalities.

• isPlotOn_univ {n : ℕ} {p : Eucl n → X} : self.isPlotOn ⋯ p ↔ self.isPlot p
• isPlot_const {n : ℕ} (x : X) : self.isPlot fun (x_1 : Eucl n) => x
• isPlotOn_reparam {n m : ℕ} {u : Set (Eucl n)} {v : Set (Eucl m)} {hu : IsOpen u} (hv : IsOpen v) {p : Eucl n → X} {f : Eucl m → Eucl n} (h : Set.MapsTo f v u) : self.isPlotOn hu p → ContDiffOn ℝ (↑⊤) f v → self.isPlotOn hv (p ∘ f)
• locality {n : ℕ} {u : Set (Eucl n)} (hu : IsOpen u) {p : Eucl n → X} : (∀ x ∈ u, ∃ (v : Set (Eucl n)) (hv : IsOpen v), x ∈ v ∧ self.isPlotOn hv p) → self.isPlotOn hu p

  The locality axiom of diffeologies, phrased in terms of isPlotOn.

• dTopology : TopologicalSpace X

  The D-topology that the diffeology built from this structure will use. Can be overwritten to allow for better definitional equalities.

• isOpen_iff_preimages_plots {u : Set X} : TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ} (p : Eucl n → X), self.isPlot p → TopologicalSpace.IsOpen (p ⁻¹' u)

def DiffeologicalSpace.mkOfPlotsOn {X : Type u_4} (d : CorePlotsOn X) : DiffeologicalSpace X

Constructs a diffeology from plots defined on open subsets or ℝⁿ rather than ℝⁿ itself, organised in the form of the auxiliary CorePlotsOn structure. This is more involved in most regards, but also often makes it quite a lot easier to prove the locality condition.

Equations

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

def euclideanDiffeology {X : Type u_4} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] : DiffeologicalSpace X

Diffeology on a finite-dimensional normed space. We make this a definition instead of an instance because we also want to have product diffeologies as an instance, and having both would cause instance diamonds on spaces like Fin n → ℝ.

Equations

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

class ContDiffCompatible (X : Type u_4) [NormedAddCommGroup X] [NormedSpace ℝ X] [DiffeologicalSpace X] : Prop

Technical condition saying that the diffeology on a space is the one coming from smoothness in the sense of ContDiff ℝ ∞. Necessary as a hypothesis for some theorems because some normed spaces carry a diffeology that is equal but not defeq to the normed space diffeology (for example the product diffeology in the case of Fin n → ℝ), so the information that these theorems still holds needs to be made available via this typeclass.

• isPlot_iff {n : ℕ} {p : Eucl n → X} : IsPlot p ↔ ContDiff ℝ (↑⊤) p

class DTopCompatible (X : Type u_4) [t : TopologicalSpace X] [DiffeologicalSpace X] : Prop

Technical condition saying that the topology on a type agrees with the D-topology. Necessary because the D-topologies on for example products and subspaces don't agree with the product and subspace topologies.

• dTop_eq : DTop = t

theorem dTop_eq (X : Type u_4) [t : TopologicalSpace X] [DiffeologicalSpace X] [DTopCompatible X] : DTop = t

theorem DSmooth.continuous' {X : Type u_4} {Y : Type u_5} [TopologicalSpace X] [DiffeologicalSpace X] [DTopCompatible X] [TopologicalSpace Y] [DiffeologicalSpace Y] [DTopCompatible Y] {f : X → Y} (hf : DSmooth f) : Continuous f

A smooth function between spaces that are equipped with the D-topology is continuous.

instance instContDiffCompatible {X : Type u_4} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] : ContDiffCompatible X

theorem contDiffCompatible_iff_eq_euclideanDiffeology {X : Type u_4} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [d : DiffeologicalSpace X] : ContDiffCompatible X ↔ d = euclideanDiffeology

instance instDTopCompatible {X : Type u_4} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] : DTopCompatible X

instance instDiffeologicalSpaceReal : DiffeologicalSpace ℝ

Equations

• instDiffeologicalSpaceReal = euclideanDiffeology

noncomputable instance instDiffeologicalSpaceComplex : DiffeologicalSpace ℂ

Equations

• instDiffeologicalSpaceComplex = euclideanDiffeology

noncomputable instance instDiffeologicalSpaceEuclideanSpaceRealOfFintype {ι : Type u_4} [Fintype ι] : DiffeologicalSpace (EuclideanSpace ℝ ι)

Equations

• instDiffeologicalSpaceEuclideanSpaceRealOfFintype = euclideanDiffeology

theorem IsPlot.dsmooth {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {p : Eucl n → X} (hp : IsPlot p) : DSmooth p

theorem DSmooth.isPlot {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {p : Eucl n → X} (hp : DSmooth p) : IsPlot p

theorem isPlot_iff_dsmooth {X : Type u_1} [DiffeologicalSpace X] {n : ℕ} {p : Eucl n → X} : IsPlot p ↔ DSmooth p

theorem isPlot_iff_contDiff {X : Type u_4} [NormedAddCommGroup X] [NormedSpace ℝ X] [DiffeologicalSpace X] [ContDiffCompatible X] {n : ℕ} {p : Eucl n → X} : IsPlot p ↔ ContDiff ℝ (↑⊤) p

theorem ContDiff.dsmooth {X : Type u_4} {Y : Type u_5} [NormedAddCommGroup X] [NormedSpace ℝ X] [DiffeologicalSpace X] [ContDiffCompatible X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [DiffeologicalSpace Y] [ContDiffCompatible Y] {f : X → Y} (hf : ContDiff ℝ (↑⊤) f) : DSmooth f

theorem DSmooth.contDiff {X : Type u_4} {Y : Type u_5} [NormedAddCommGroup X] [NormedSpace ℝ X] [DiffeologicalSpace X] [ContDiffCompatible X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [DiffeologicalSpace Y] [ContDiffCompatible Y] [FiniteDimensional ℝ X] {f : X → Y} (hf : DSmooth f) : ContDiff ℝ (↑⊤) f

theorem dsmooth_iff_contDiff {X : Type u_4} {Y : Type u_5} [NormedAddCommGroup X] [NormedSpace ℝ X] [DiffeologicalSpace X] [ContDiffCompatible X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [DiffeologicalSpace Y] [ContDiffCompatible Y] [FiniteDimensional ℝ X] {f : X → Y} : DSmooth f ↔ ContDiff ℝ (↑⊤) f

def DiffeologicalSpace.toPlots {X : Type u_4} : DiffeologicalSpace X → Set ((n : ℕ) × (Eucl n → X))

The plots belonging to a diffeology, as a subset of (n : ℕ) × (Eucl n → X).

Equations

• x✝.toPlots = {p : (n : ℕ) × (Eucl n → X) | IsPlot p.snd}

theorem DiffeologicalSpace.injective_toPlots {X : Type u_4} : Function.Injective toPlots

def DiffeologicalSpace.generatePlots {X : Type u_4} (g : Set ((n : ℕ) × (Eucl n → X))) : Set ((n : ℕ) × (Eucl n → X))

The plots belonging to the diffeology generated by g.

Equations

• DiffeologicalSpace.generatePlots g = ⋂ d ∈ {d : DiffeologicalSpace X | g ⊆ d.toPlots}, d.toPlots

def DiffeologicalSpace.generateFrom {X : Type u_4} (g : Set ((n : ℕ) × (Eucl n → X))) : DiffeologicalSpace X

The diffeology generated by a set g of plots.

Equations

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

theorem DiffeologicalSpace.self_subset_toPlots_generateFrom {X : Type u_4} (g : Set ((n : ℕ) × (Eucl n → X))) : g ⊆ (generateFrom g).toPlots

theorem DiffeologicalSpace.isPlot_generateFrom_of_mem {X : Type u_4} {g : Set ((n : ℕ) × (Eucl n → X))} {n : ℕ} {p : Eucl n → X} (hp : ⟨n, p⟩ ∈ g) : IsPlot p

instance DiffeologicalSpace.instPartialOrder {X : Type u_4} : PartialOrder (DiffeologicalSpace X)

Equations

• DiffeologicalSpace.instPartialOrder = PartialOrder.lift DiffeologicalSpace.toPlots ⋯

theorem DiffeologicalSpace.le_def {X : Type u_4} {d₁ d₂ : DiffeologicalSpace X} : d₁ ≤ d₂ ↔ d₁.toPlots ⊆ d₂.toPlots

theorem DiffeologicalSpace.le_iff {X : Type u_4} {d₁ d₂ : DiffeologicalSpace X} : d₁ ≤ d₂ ↔ ∀ (n : ℕ), plots n ⊆ plots n

theorem DiffeologicalSpace.le_iff' {X : Type u_4} {d₁ d₂ : DiffeologicalSpace X} : d₁ ≤ d₂ ↔ ∀ (n : ℕ) (p : Eucl n → X), IsPlot p → IsPlot p

theorem DiffeologicalSpace.generateFrom_le_iff_subset_toPlots {X : Type u_4} {g : Set ((n : ℕ) × (Eucl n → X))} {d : DiffeologicalSpace X} : generateFrom g ≤ d ↔ g ⊆ d.toPlots

theorem DiffeologicalSpace.generateFrom_le_iff {X : Type u_4} {g : Set ((n : ℕ) × (Eucl n → X))} {d : DiffeologicalSpace X} : generateFrom g ≤ d ↔ ∀ (n : ℕ) (p : Eucl n → X), ⟨n, p⟩ ∈ g → IsPlot p

Version of generateFrom_le_iff_subset_toPlots that is stated in terms of IsPlot instead of toPlots.

def DiffeologicalSpace.mkOfClosure {X : Type u_4} (g : Set ((n : ℕ) × (Eucl n → X))) (hg : (generateFrom g).toPlots = g) : DiffeologicalSpace X

The diffeology defined by g. Same as generateFrom g, except that its set of plots is definitionally equal to g.

Equations

• DiffeologicalSpace.mkOfClosure g hg = { plots := fun (n : ℕ) => {p : Eucl n → X | ⟨n, p⟩ ∈ g}, constant_plots := ⋯, plot_reparam := ⋯, locality := ⋯, isOpen_iff_preimages_plots := ⋯ }

theorem DiffeologicalSpace.mkOfClosure_eq_generateFrom {X : Type u_4} {g : Set ((n : ℕ) × (Eucl n → X))} {hg : (generateFrom g).toPlots = g} : DiffeologicalSpace.mkOfClosure g hg = generateFrom g

theorem DiffeologicalSpace.gc_generateFrom (X : Type u_5) : GaloisConnection generateFrom toPlots

def DiffeologicalSpace.giGenerateFrom (X : Type u_5) : GaloisInsertion generateFrom toPlots

The Galois insertion between DiffeologicalSpace α and Set ((n : ℕ) × (Eucl n → X)) whose lower part sends a collection of plots in X to the diffeology they generate, and whose upper part sends a diffeology to its collection of plots.

Equations

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

instance DiffeologicalSpace.instCompleteLattice {X : Type u_4} : CompleteLattice (DiffeologicalSpace X)

Equations

• DiffeologicalSpace.instCompleteLattice = (DiffeologicalSpace.giGenerateFrom X).liftCompleteLattice

theorem DiffeologicalSpace.generateFrom_mono {X : Type u_4} {g₁ g₂ : Set ((n : ℕ) × (Eucl n → X))} (h : g₁ ⊆ g₂) : generateFrom g₁ ≤ generateFrom g₂

theorem DiffeologicalSpace.generateFrom_toPlots {X : Type u_4} (d : DiffeologicalSpace X) : generateFrom d.toPlots = d

theorem DiffeologicalSpace.leftInverse_generateFrom {X : Type u_4} : Function.LeftInverse generateFrom toPlots

theorem DiffeologicalSpace.generateFrom_surjective {X : Type u_4} : Function.Surjective generateFrom

theorem DiffeologicalSpace.generateFrom_union {X : Type u_4} (g₁ g₂ : Set ((n : ℕ) × (Eucl n → X))) : generateFrom (g₁ ∪ g₂) = generateFrom g₁ ⊔ generateFrom g₂

theorem DiffeologicalSpace.generateFrom_iUnion {X : Type u_4} {ι : Type u_5} {g : ι → Set ((n : ℕ) × (Eucl n → X))} : generateFrom (⋃ (i : ι), g i) = ⨆ (i : ι), generateFrom (g i)

theorem DiffeologicalSpace.generateFrom_sUnion {X : Type u_4} {G : Set (Set ((n : ℕ) × (Eucl n → X)))} : generateFrom (⋃₀ G) = ⨆ s ∈ G, generateFrom s

theorem DiffeologicalSpace.toPlots_inf {X : Type u_4} (d₁ d₂ : DiffeologicalSpace X) : (d₁ ⊓ d₂).toPlots = d₁.toPlots ∩ d₂.toPlots

theorem DiffeologicalSpace.toPlots_iInf {X : Type u_4} {ι : Type u_5} {D : ι → DiffeologicalSpace X} : (⨅ (i : ι), D i).toPlots = ⋂ (i : ι), (D i).toPlots

theorem DiffeologicalSpace.toPlots_sInf {X : Type u_4} {D : Set (DiffeologicalSpace X)} : (sInf D).toPlots = ⋂ d ∈ D, d.toPlots

theorem DiffeologicalSpace.generateFrom_union_toPlots {X : Type u_4} (d₁ d₂ : DiffeologicalSpace X) : generateFrom (d₁.toPlots ∪ d₂.toPlots) = d₁ ⊔ d₂

theorem DiffeologicalSpace.generateFrom_iUnion_toPlots {X : Type u_4} {ι : Type u_5} (D : ι → DiffeologicalSpace X) : generateFrom (⋃ (i : ι), (D i).toPlots) = ⨆ (i : ι), D i

theorem DiffeologicalSpace.generateFrom_inter_toPlots {X : Type u_4} (d₁ d₂ : DiffeologicalSpace X) : generateFrom (d₁.toPlots ∩ d₂.toPlots) = d₁ ⊓ d₂

theorem DiffeologicalSpace.generateFrom_iInter_toPlots {X : Type u_4} {ι : Type u_5} (D : ι → DiffeologicalSpace X) : generateFrom (⋂ (i : ι), (D i).toPlots) = ⨅ (i : ι), D i

theorem DiffeologicalSpace.generateFrom_iInter_of_generateFrom_eq_self {X : Type u_4} {ι : Type u_5} (G : ι → Set ((n : ℕ) × (Eucl n → X))) (hG : ∀ (i : ι), (generateFrom (G i)).toPlots = G i) : generateFrom (⋂ (i : ι), G i) = ⨅ (i : ι), generateFrom (G i)

theorem DiffeologicalSpace.isPlot_inf_iff {X : Type u_4} {d₁ d₂ : DiffeologicalSpace X} {n : ℕ} {p : Eucl n → X} : IsPlot p ↔ IsPlot p ∧ IsPlot p

theorem DiffeologicalSpace.isPlot_iInf_iff {X : Type u_4} {ι : Type u_5} {D : ι → DiffeologicalSpace X} {n : ℕ} {p : Eucl n → X} : IsPlot p ↔ ∀ (i : ι), IsPlot p

theorem DiffeologicalSpace.isPlot_sInf_iff {X : Type u_4} {D : Set (DiffeologicalSpace X)} {n : ℕ} {p : Eucl n → X} : IsPlot p ↔ ∀ d ∈ D, IsPlot p

theorem DiffeologicalSpace.isPlot_generateFrom_iff {X : Type u_4} (g : Set ((n : ℕ) × (Eucl n → X))) {n : ℕ} {p : Eucl n → X} : IsPlot p ↔ (∃ (y : X), p = fun (x : Eucl n) => y) ∨ ∀ (x : Eucl n), ∃ p' ∈ g, ∃ (f : Eucl n → Eucl p'.fst), (∃ u ∈ nhds x, ContDiffOn ℝ (↑⊤) f u) ∧ p =ᶠ[nhds x] p'.snd ∘ f

A map is a plot in the diffeology generated g iff it is constant or locally a reparametrisation of maps in g.