Smooth modules

This file introduces diffeological modules and the "fine diffeology", the finest diffeology turning a given module into a diffeological module. This is comparable to Topology.Algebra.Module.ModuleTopology, although the file structure and naming are different for historical reasons.

While in practice we mostly care about diffeological vector spaces over ℝ, we work over general rings here just in case.

Main definitions / results:

• DiffeologicalRing R: typeclass saying that addition, negation and multiplication in the ring R are smooth
• arbitrary products of diffeological modules are again diffeological modules
• diffeologies induced by linear maps to diffeological modules are module diffeologies
• ModuleDiffeology R X: the type of R-module diffeologies on X. Forms a complete lattice.
• fineDiffeology R X: the finest diffeology on X making it into a topological R-module.
• fineDiffeology_eq_euclideanDiffeology: on finite-dimensional real vector spaces, the fine diffeology agrees with the standard diffeology for any choice of norm

Note that we do not actually define a typeclass DiffeologicalModule R X analogous to DiffeologicalGroup or DiffeologicalRing - the reason is such a class could not extend DiffeologicalAddGroup X without breaking typeclass synthesis, because of the extra parameter R. The class would therefore instead have to take in [DiffeologicalAddGroup X] as an assumption, but at that point it would be nothing more than a synonym for DSmoothSMul R X. We therefore avoid defining such a class completely, and instead use [DiffeologicalAddGroup X] [DSmoothSMul R X] whereever we want X to be a diffeological module over R. This is likely also the reason that mathlib has no TopologicalModule class.

As a consequence, statements like "arbitrary products of diffeological modules are diffeological modules" and "diffeologies induced by linear maps to diffeological modules are module diffeologies" also had to be split up into two statements each, one about the underlying additive group and one about scalar multiplication. Since these lemmas already exist in the respective files, we do not reintroduce them here.

TODO

• the fine diffeology is generated by all linear plots
• explicit characterisation of plots of the fine diffeology
• results about the D-topology of the fine diffeology
• is the fine diffeology preserved under products?

class DiffeologicalRing (R : Type u_1) [DiffeologicalSpace R] [NonUnitalNonAssocRing R] extends DiffeologicalAddGroup R, DSmoothMul R : Prop

A diffeological ring is a ring in which addition, negation and multiplication are smooth.

• dsmooth_add : DSmooth fun (p : R × R) => p.1 + p.2
• dsmooth_neg : DSmooth fun (a : R) => -a
• dsmooth_mul : DSmooth fun (p : R × R) => p.1 * p.2

instance instDiffeologicalRingReal : DiffeologicalRing ℝ

The main example we care about: ℝ is a diffeological ring.

instance instDiffeologicalRingComplex : DiffeologicalRing ℂ

instance instDiffeologicalAddGroupOfContDiffCompatible (X : Type u_1) [NormedAddCommGroup X] [NormedSpace ℝ X] [DiffeologicalSpace X] [ContDiffCompatible X] : DiffeologicalAddGroup X

Normed spaces with their natural diffeologies are diffeological groups under addition.

instance instDSmoothSMulRealOfContDiffCompatible (X : Type u_1) [NormedAddCommGroup X] [NormedSpace ℝ X] [DiffeologicalSpace X] [ContDiffCompatible X] : DSmoothSMul ℝ X

Normed spaces with their natural diffeologies are diffeological vector spaces.

theorem LinearMap.isPlot (X : Type u_1) [AddCommGroup X] [Module ℝ X] [DiffeologicalSpace X] [DSmoothAdd X] [DSmoothSMul ℝ X] {n : ℕ} (p : Eucl n →ₗ[ℝ] X) : IsPlot ⇑p

Every linear map from Eucl n into a diffeological vector space is a plot.

Lattice of module diffeologies

Analogous to GroupDiffeology G, we define for any R-module X the type ModuleDiffeology R X of all diffeologies that turn X into a diffeological module. This is interesting because, like DiffeologicalSpace X, ModuleDiffeology R X is always a complete lattice - its top element is always the indiscrete diffeology, while its bottom element is generally nontrivial. Note that the discrete diffeology is not a module diffeology because scalar multiplication fails to be continuous.

structure ModuleDiffeology (R : Type u_1) [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] (X : Type u_2) [AddCommGroup X] [Module R X] extends DiffeologicalSpace X, DiffeologicalAddGroup X, DSmoothSMul R X : Type u_2

A module diffeology on a module X is a diffeology with which X is a diffeological module.

• 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)
• dsmooth_add : DSmooth fun (p : X × X) => p.1 + p.2
• dsmooth_neg : DSmooth fun (a : X) => -a
• dsmooth_smul : DSmooth fun (p : R × X) => p.1 • p.2

def ModuleDiffeology.toAddGroupDiffeology {R : Type u_1} [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] {X : Type u_2} [AddCommGroup X] [Module R X] (d : ModuleDiffeology R X) : AddGroupDiffeology X

Equations

• d.toAddGroupDiffeology = { toDiffeologicalSpace := d.toDiffeologicalSpace, toDiffeologicalAddGroup := ⋯ }

theorem ModuleDiffeology.dsmooth_add' {R : Type u_1} [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] {X : Type u_2} [AddCommGroup X] [Module R X] (d : ModuleDiffeology R X) : DSmooth fun (p : X × X) => p.1 + p.2

A version of the global dsmooth_add suitable for dot notation.

theorem ModuleDiffeology.dsmooth_neg' {R : Type u_1} [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] {X : Type u_2} [AddCommGroup X] [Module R X] (d : ModuleDiffeology R X) : DSmooth Neg.neg

A version of the global dsmooth_neg suitable for dot notation.

theorem ModuleDiffeology.dsmooth_smul' {R : Type u_1} [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] {X : Type u_2} [AddCommGroup X] [Module R X] (d : ModuleDiffeology R X) : DSmooth fun (p : R × X) => p.1 • p.2

A version of the global dsmooth_smul suitable for dot notation.

theorem ModuleDiffeology.toDiffeologicalSpace_injective {R : Type u_1} [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] {X : Type u_2} [AddCommGroup X] [Module R X] : Function.Injective toDiffeologicalSpace

theorem ModuleDiffeology.toAddGroupDiffeology_injective {R : Type u_1} [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] {X : Type u_2} [AddCommGroup X] [Module R X] : Function.Injective toAddGroupDiffeology

theorem ModuleDiffeology.ext' {R : Type u_1} [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] {X : Type u_2} [AddCommGroup X] [Module R X] {d₁ d₂ : ModuleDiffeology R X} (h : d₁.toDiffeologicalSpace = d₂.toDiffeologicalSpace) : d₁ = d₂

theorem ModuleDiffeology.ext'_iff {R : Type u_1} [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] {X : Type u_2} [AddCommGroup X] [Module R X] {d₁ d₂ : ModuleDiffeology R X} : d₁ = d₂ ↔ d₁.toDiffeologicalSpace = d₂.toDiffeologicalSpace

instance ModuleDiffeology.instPartialOrder {R : Type u_1} [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] {X : Type u_2} [AddCommGroup X] [Module R X] : PartialOrder (ModuleDiffeology R X)

Equations

• ModuleDiffeology.instPartialOrder = PartialOrder.lift ModuleDiffeology.toDiffeologicalSpace ⋯

theorem ModuleDiffeology.toDiffeologicalSpace_le {R : Type u_1} [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] {X : Type u_2} [AddCommGroup X] [Module R X] {d₁ d₂ : ModuleDiffeology R X} : d₁.toDiffeologicalSpace ≤ d₂.toDiffeologicalSpace ↔ d₁ ≤ d₂

def ModuleDiffeology.reflector {R : Type u_1} [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] {X : Type u_2} [AddCommGroup X] [Module R X] (d : DiffeologicalSpace X) : ModuleDiffeology R X

The coarsest module diffeology that is finer than a given diffeology. Called reflector for the lack of a better name and because it is left-adjoint to ModuleDiffeology.toDiffeologicalSpace.

Equations

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

theorem ModuleDiffeology.gc_toDiffeologicalSpace {R : Type u_1} [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] {X : Type u_2} [AddCommGroup X] [Module R X] : GaloisConnection reflector toDiffeologicalSpace

def ModuleDiffeology.gci_toDiffeologicalSpace {R : Type u_1} [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] {X : Type u_2} [AddCommGroup X] [Module R X] : GaloisInsertion reflector toDiffeologicalSpace

The galois insertion between ModuleDiffeology R X and DiffeologicalSpace X whose lower part sends each diffeology to the finest coarser module diffeology, and whose upper part sends each module diffeology to itself.

Equations

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

instance ModuleDiffeology.instCompleteLattice {R : Type u_1} [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] {X : Type u_2} [AddCommGroup X] [Module R X] : CompleteLattice (ModuleDiffeology R X)

R-module diffeologies on X form a complete lattice.

Equations

• ModuleDiffeology.instCompleteLattice = ModuleDiffeology.gci_toDiffeologicalSpace.liftCompleteLattice

The fine diffeology

On any module X over a diffeological ring R, the fine diffeology is defined as the finest diffeology making it into a topological module, i.e. the bottom element of ModuleDiffeology R X. Although we do not show it here, the plots of this diffeology are precisely those maps that locally restrict to smooth maps to finite-dimensional subspaces of X with their standard diffeologies. In particular, on all finite-dimensional normed spaces this coincides with the smooth diffeology given by the norm - see Zemmour's diffeology book for more details.

It's not yet clear to me whether the D-topology of this diffeology always coincides with the finest topology making X into a topological module - if it does, it might make sense to redefine this to make the D-topology defeq to mathlib's moduleTopology R X.

def fineDiffeology (R : Type u_1) [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] (X : Type u_2) [AddCommGroup X] [Module R X] : DiffeologicalSpace X

The finest diffeology turning a given module over a diffeological ring into a diffeological module.

Equations

• fineDiffeology R X = ⊥.toDiffeologicalSpace

class IsFineDiffeology (R : Type u_1) [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] (X : Type u_2) [AddCommGroup X] [Module R X] [d : DiffeologicalSpace X] : Prop

A typeclass asserting that the diffeology on X equals fineDiffeology R X.

• eq_fineDiffeology' : d = fineDiffeology R X

  Slightly awkward because all arguments are implicit - use eq_fineDiffeology R X instead.

theorem eq_fineDiffeology (R : Type u_1) [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] (X : Type u_2) [AddCommGroup X] [Module R X] [d : DiffeologicalSpace X] [IsFineDiffeology R X] : d = fineDiffeology R X

instance instIsFineDiffeology (R : Type u_1) [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] (X : Type u_2) [AddCommGroup X] [Module R X] : IsFineDiffeology R X

theorem IsFineDiffeology.diffeologicalAddGroup (R : Type u_1) [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] (X : Type u_2) [AddCommGroup X] [Module R X] [DiffeologicalSpace X] [IsFineDiffeology R X] : DiffeologicalAddGroup X

Every module equipped with the fine diffeology is an additive diffeological group. This unfortunately can't be an instance because the parameter R can't be inferred from the conclusion of the lemma (i.e., when lean is trying to synthesise an instance DiffeologicalAddGroup X, it wouldn't know which ring R to use with this lemma).

instance IsFineDiffeology.diffeologicalAddGroupReal (X : Type u_1) [AddCommGroup X] [Module ℝ X] [DiffeologicalSpace X] [IsFineDiffeology ℝ X] : DiffeologicalAddGroup X

Since real diffeological vector spaces are the most important special case of diffeological modules, we register at least IsFineDiffeology.diffeologicalAddGroup ℝ X as an instance.

instance IsFineDiffeology.dsmoothSMul (R : Type u_1) [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] (X : Type u_2) [AddCommGroup X] [Module R X] [DiffeologicalSpace X] [IsFineDiffeology R X] : DSmoothSMul R X

Scalar multiplication is smooth on any module that is equipped with the fine diffeology. Together with IsFineDiffeology.diffeologicalAddGroup this means that every module carrying the fine diffeology is a diffeological module.

theorem fineDiffeology_le (R : Type u_1) [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] (X : Type u_2) [AddCommGroup X] [Module R X] [d : DiffeologicalSpace X] [DiffeologicalAddGroup X] [DSmoothSMul R X] : fineDiffeology R X ≤ d

The fine diffeology is finer than any other diffeology making X a diffeological module.

theorem LinearMap.dsmooth (R : Type u_1) [DiffeologicalSpace R] [Ring R] [DiffeologicalRing R] {X : Type u_2} [AddCommGroup X] [Module R X] [DiffeologicalSpace X] [IsFineDiffeology R X] {Y : Type u_3} [AddCommGroup Y] [Module R Y] [DiffeologicalSpace Y] [DiffeologicalAddGroup Y] [DSmoothSMul R Y] (f : X →ₗ[R] Y) : DSmooth ⇑f

Any linear map from a fine diffeological module to another diffeological module is smooth.

theorem fineDiffeology_eq_euclideanDiffeology (X : Type u_1) [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] : fineDiffeology ℝ X = euclideanDiffeology

On finite-dimensional normed spaces, the fine diffeology equals the standard diffeology consisting of plots that are smooth with respect to the norm. Since the fine diffeology does not depend on any norm, this in particular shows that euclideanDiffeology does not actually depend on the choice of norm either.

instance instContDiffCompatibleOfFiniteDimensionalOfIsFineDiffeologyReal {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [DiffeologicalSpace X] [IsFineDiffeology ℝ X] : ContDiffCompatible X

instance instIsFineDiffeologyRealOfFiniteDimensionalOfContDiffCompatible {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [FiniteDimensional ℝ X] [DiffeologicalSpace X] [ContDiffCompatible X] : IsFineDiffeology ℝ X