Diffeological monoids

Adapted from Mathlib.Topology.Algebra.Monoid. For now this just contains a few basic definitions and lemmas, used to build up the theory of diffeological groups and vector spaces.

theorem dsmooth_one {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [One M] [DiffeologicalSpace X] : DSmooth 1

theorem dsmooth_zero {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [Zero M] [DiffeologicalSpace X] : DSmooth 0

class DSmoothAdd (M : Type u_1) [DiffeologicalSpace M] [Add M] : Prop

• dsmooth_add : DSmooth fun (p : M × M) => p.1 + p.2

class DSmoothMul (M : Type u_1) [DiffeologicalSpace M] [Mul M] : Prop

• dsmooth_mul : DSmooth fun (p : M × M) => p.1 * p.2

instance instDSmoothMulOrderDual {M : Type u_1} [DiffeologicalSpace M] [Mul M] [DSmoothMul M] : DSmoothMul Mᵒᵈ

instance instDSmoothAddOrderDual {M : Type u_1} [DiffeologicalSpace M] [Add M] [DSmoothAdd M] : DSmoothAdd Mᵒᵈ

theorem dsmooth_mul {M : Type u_1} [DiffeologicalSpace M] [Mul M] [DSmoothMul M] : DSmooth fun (p : M × M) => p.1 * p.2

theorem dsmooth_add {M : Type u_1} [DiffeologicalSpace M] [Add M] [DSmoothAdd M] : DSmooth fun (p : M × M) => p.1 + p.2

instance instDSmoothMulULift {M : Type u_1} [DiffeologicalSpace M] [Mul M] [DSmoothMul M] : DSmoothMul (ULift.{u_3, u_1} M)

instance instDSmoothAddULift {M : Type u_1} [DiffeologicalSpace M] [Add M] [DSmoothAdd M] : DSmoothAdd (ULift.{u_3, u_1} M)

instance DSmoothMul.to_dsmoothSMul {M : Type u_1} [DiffeologicalSpace M] [Mul M] [DSmoothMul M] : DSmoothSMul M M

instance DSmoothAdd.to_dsmoothVAdd {M : Type u_1} [DiffeologicalSpace M] [Add M] [DSmoothAdd M] : DSmoothVAdd M M

instance DSmoothMul.to_dsmoothSMul_op {M : Type u_1} [DiffeologicalSpace M] [Mul M] [DSmoothMul M] : DSmoothSMul Mᵐᵒᵖ M

instance DSmoothAdd.to_dsmoothVAdd_op {M : Type u_1} [DiffeologicalSpace M] [Add M] [DSmoothAdd M] : DSmoothVAdd Mᵃᵒᵖ M

theorem DSmooth.mul {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [Mul M] [DSmoothMul M] [DiffeologicalSpace X] {f g : X → M} (hf : DSmooth f) (hg : DSmooth g) : DSmooth fun (x : X) => f x * g x

theorem DSmooth.add {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [Add M] [DSmoothAdd M] [DiffeologicalSpace X] {f g : X → M} (hf : DSmooth f) (hg : DSmooth g) : DSmooth fun (x : X) => f x + g x

theorem dsmooth_mul_left {M : Type u_1} [DiffeologicalSpace M] [Mul M] [DSmoothMul M] (a : M) : DSmooth fun (b : M) => a * b

theorem dsmooth_add_left {M : Type u_1} [DiffeologicalSpace M] [Add M] [DSmoothAdd M] (a : M) : DSmooth fun (b : M) => a + b

theorem dsmooth_mul_right {M : Type u_1} [DiffeologicalSpace M] [Mul M] [DSmoothMul M] (a : M) : DSmooth fun (b : M) => b * a

theorem dsmooth_add_right {M : Type u_1} [DiffeologicalSpace M] [Add M] [DSmoothAdd M] (a : M) : DSmooth fun (b : M) => b + a

instance Prod.dsmoothMul {M : Type u_1} [DiffeologicalSpace M] [Mul M] [DSmoothMul M] {N : Type u_3} [DiffeologicalSpace N] [Mul N] [DSmoothMul N] : DSmoothMul (M × N)

instance Prod.dsmoothAdd {M : Type u_1} [DiffeologicalSpace M] [Add M] [DSmoothAdd M] {N : Type u_3} [DiffeologicalSpace N] [Add N] [DSmoothAdd N] : DSmoothAdd (M × N)

instance Pi.dsmoothMul {ι : Type u_3} {M : ι → Type u_4} [(i : ι) → DiffeologicalSpace (M i)] [(i : ι) → Mul (M i)] [∀ (i : ι), DSmoothMul (M i)] : DSmoothMul ((i : ι) → M i)

instance Pi.dsmoothAdd {ι : Type u_3} {M : ι → Type u_4} [(i : ι) → DiffeologicalSpace (M i)] [(i : ι) → Add (M i)] [∀ (i : ι), DSmoothAdd (M i)] : DSmoothAdd ((i : ι) → M i)

theorem IsDInducing.dsmoothMul {M : Type u_3} {N : Type u_4} {F : Type u_5} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] [DiffeologicalSpace M] [DiffeologicalSpace N] [DSmoothMul N] (f : F) (hf : IsDInducing ⇑f) : DSmoothMul M

For any monoid homomorphism to a diffeological monoid, the induced diffeology makes the domain a diffeological monoid too.

theorem IsDInducing.dsmoothAdd {M : Type u_3} {N : Type u_4} {F : Type u_5} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] [DiffeologicalSpace M] [DiffeologicalSpace N] [DSmoothAdd N] (f : F) (hf : IsDInducing ⇑f) : DSmoothAdd M

For any monoid homomorphism to a diffeological monoid, the induced diffeology makes the domain a diffeological monoid too.

theorem dsmoothMul_induced {M : Type u_3} {N : Type u_4} {F : Type u_5} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] [DiffeologicalSpace N] [DSmoothMul N] (f : F) : DSmoothMul M

theorem dsmoothAdd_induced {M : Type u_3} {N : Type u_4} {F : Type u_5} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] [DiffeologicalSpace N] [DSmoothAdd N] (f : F) : DSmoothAdd M

instance Subsemigroup.dsmoothMul {M : Type u_1} [DiffeologicalSpace M] [Semigroup M] [DSmoothMul M] (S : Subsemigroup M) : DSmoothMul ↥S

instance AddSubsemigroup.dsmoothAdd {M : Type u_1} [DiffeologicalSpace M] [AddSemigroup M] [DSmoothAdd M] (S : AddSubsemigroup M) : DSmoothAdd ↥S

instance Submonoid.dsmoothMul {M : Type u_1} [DiffeologicalSpace M] [Monoid M] [DSmoothMul M] (S : Submonoid M) : DSmoothMul ↥S

instance AddSubmonoid.dsmoothAdd {M : Type u_1} [DiffeologicalSpace M] [AddMonoid M] [DSmoothAdd M] (S : AddSubmonoid M) : DSmoothAdd ↥S

theorem dsmooth_list_prod {M : Type u_1} [DiffeologicalSpace M] [Monoid M] [DSmoothMul M] {X : Type u_2} [DiffeologicalSpace X] {ι : Type u_3} {f : ι → X → M} (l : List ι) (hf : ∀ i ∈ l, DSmooth (f i)) : DSmooth fun (a : X) => (List.map (fun (i : ι) => f i a) l).prod

theorem dsmooth_list_sum {M : Type u_1} [DiffeologicalSpace M] [AddMonoid M] [DSmoothAdd M] {X : Type u_2} [DiffeologicalSpace X] {ι : Type u_3} {f : ι → X → M} (l : List ι) (hf : ∀ i ∈ l, DSmooth (f i)) : DSmooth fun (a : X) => (List.map (fun (i : ι) => f i a) l).sum

theorem dsmooth_pow {M : Type u_1} [DiffeologicalSpace M] [Monoid M] [DSmoothMul M] (n : ℕ) : DSmooth fun (a : M) => a ^ n

theorem dsmooth_nsmul {M : Type u_1} [DiffeologicalSpace M] [AddMonoid M] [DSmoothAdd M] (n : ℕ) : DSmooth fun (a : M) => n • a

theorem DSmooth.pow {M : Type u_1} [DiffeologicalSpace M] [Monoid M] [DSmoothMul M] {X : Type u_2} [DiffeologicalSpace X] {f : X → M} (h : DSmooth f) (n : ℕ) : DSmooth fun (b : X) => f b ^ n

theorem DSmooth.nsmul {M : Type u_1} [DiffeologicalSpace M] [AddMonoid M] [DSmoothAdd M] {X : Type u_2} [DiffeologicalSpace X] {f : X → M} (h : DSmooth f) (n : ℕ) : DSmooth fun (b : X) => n • f b

instance MulOpposite.instDSmoothMul {M : Type u_1} [DiffeologicalSpace M] [Mul M] [DSmoothMul M] : DSmoothMul Mᵐᵒᵖ

If multiplication is smooth in α, then it also is in αᵐᵒᵖ.

instance AddOpposite.instDSmoothAdd {M : Type u_1} [DiffeologicalSpace M] [Add M] [DSmoothAdd M] : DSmoothAdd Mᵃᵒᵖ

If addition is smooth in α, then it also is in αᵃᵒᵖ.

instance Units.instDSmoothMul {M : Type u_1} [DiffeologicalSpace M] [Monoid M] [DSmoothMul M] : DSmoothMul Mˣ

If multiplication on a monoid is smooth, then multiplication on the units of the monoid, with respect to the induced diffeology, is also smooth.

instance AddUnits.instDSmoothAdd {M : Type u_1} [DiffeologicalSpace M] [AddMonoid M] [DSmoothAdd M] : DSmoothAdd (AddUnits M)

If addition on an additive monoid is smooth, then addition on the additive units of the monoid, with respect to the induced diffeology, is also smooth.

theorem DSmooth.units_map {M : Type u_1} [DiffeologicalSpace M] [Monoid M] {N : Type u_2} [DiffeologicalSpace N] [Monoid N] (f : M →* N) (hf : DSmooth ⇑f) : DSmooth ⇑(Units.map f)

theorem DSmooth.addUnits_map {M : Type u_1} [DiffeologicalSpace M] [AddMonoid M] {N : Type u_2} [DiffeologicalSpace N] [AddMonoid N] (f : M →+ N) (hf : DSmooth ⇑f) : DSmooth ⇑(AddUnits.map f)

theorem dsmooth_multiset_prod {M : Type u_1} [DiffeologicalSpace M] [CommMonoid M] [DSmoothMul M] {X : Type u_2} [DiffeologicalSpace X] {ι : Type u_3} {f : ι → X → M} (s : Multiset ι) : (∀ i ∈ s, DSmooth (f i)) → DSmooth fun (a : X) => (Multiset.map (fun (i : ι) => f i a) s).prod

theorem dsmooth_multiset_sum {M : Type u_1} [DiffeologicalSpace M] [AddCommMonoid M] [DSmoothAdd M] {X : Type u_2} [DiffeologicalSpace X] {ι : Type u_3} {f : ι → X → M} (s : Multiset ι) : (∀ i ∈ s, DSmooth (f i)) → DSmooth fun (a : X) => (Multiset.map (fun (i : ι) => f i a) s).sum

theorem dsmooth_finset_prod {M : Type u_1} [DiffeologicalSpace M] [CommMonoid M] [DSmoothMul M] {X : Type u_2} [DiffeologicalSpace X] {ι : Type u_3} {f : ι → X → M} (s : Finset ι) : (∀ i ∈ s, DSmooth (f i)) → DSmooth fun (a : X) => ∏ i ∈ s, f i a

theorem dsmooth_finset_sum {M : Type u_1} [DiffeologicalSpace M] [AddCommMonoid M] [DSmoothAdd M] {X : Type u_2} [DiffeologicalSpace X] {ι : Type u_3} {f : ι → X → M} (s : Finset ι) : (∀ i ∈ s, DSmooth (f i)) → DSmooth fun (a : X) => ∑ i ∈ s, f i a

instance instDSmoothAddAdditiveOfDSmoothMul {M : Type u_1} [DiffeologicalSpace M] [Mul M] [DSmoothMul M] : DSmoothAdd (Additive M)

instance instDSmoothMulMultiplicativeOfDSmoothAdd {M : Type u_1} [DiffeologicalSpace M] [Add M] [DSmoothAdd M] : DSmoothMul (Multiplicative M)

theorem dsmoothMul_sInf {M : Type u_1} [Mul M] {D : Set (DiffeologicalSpace M)} (h : ∀ d ∈ D, DSmoothMul M) : DSmoothMul M

theorem dsmoothAdd_sInf {M : Type u_1} [Add M] {D : Set (DiffeologicalSpace M)} (h : ∀ d ∈ D, DSmoothAdd M) : DSmoothAdd M

theorem dsmoothMul_iInf {M : Type u_1} {ι : Type u_2} [Mul M] {D : ι → DiffeologicalSpace M} (h' : ∀ (i : ι), DSmoothMul M) : DSmoothMul M

theorem dsmoothAdd_iInf {M : Type u_1} {ι : Type u_2} [Add M] {D : ι → DiffeologicalSpace M} (h' : ∀ (i : ι), DSmoothAdd M) : DSmoothAdd M

theorem dsmoothMul_inf {M : Type u_1} [Mul M] {d₁ d₂ : DiffeologicalSpace M} (h₁ : DSmoothMul M) (h₂ : DSmoothMul M) : DSmoothMul M

theorem dsmoothAdd_inf {M : Type u_1} [Add M] {d₁ d₂ : DiffeologicalSpace M} (h₁ : DSmoothAdd M) (h₂ : DSmoothAdd M) : DSmoothAdd M

theorem DSmoothMul.continuousMul {M : Type u_1} [DiffeologicalSpace M] [Monoid M] [DSmoothMul M] [LocallyCompactSpace M] : ContinuousMul M

If the D-topology makes M locally compact, then any smooth multiplication on X is also continuous. Local compactness is needed here because multiplication is a priori only continuous with respect to the D-topology on M × M, not the product topology - when M is locally compact the topologies agree, but otherwise the product topology could be fine enough for multiplication to not be continuous.

theorem DSmoothAdd.continuousAdd {M : Type u_1} [DiffeologicalSpace M] [AddMonoid M] [DSmoothAdd M] [LocallyCompactSpace M] : ContinuousAdd M

If the D-topology makes M locally compact, then any smooth addition on X is also continuous. Local compactness is needed here because addition is a priori only continuous with respect to the D-topology on M × M, not the product topology - when M is locally compact the topologies agree, but otherwise the product topology could be fine enough for addition to not be continuous.

instance instContinuousMulOfDTopCompatibleOfDSmoothMulOfLocallyCompactSpace {M : Type u_1} [Monoid M] [DiffeologicalSpace M] [TopologicalSpace M] [DTopCompatible M] [DSmoothMul M] [LocallyCompactSpace M] : ContinuousMul M

Variant of DSmoothMul.continuousMul phrased in terms of spaces equipped with DTopCompatible topologies.

instance instContinuousAddOfDTopCompatibleOfDSmoothAddOfLocallyCompactSpace {M : Type u_1} [AddMonoid M] [DiffeologicalSpace M] [TopologicalSpace M] [DTopCompatible M] [DSmoothAdd M] [LocallyCompactSpace M] : ContinuousAdd M

Variant of DSmoothAdd.continuousAdd phrased in terms of spaces equipped with DTopCompatible topologies.