Smooth actions by monoids

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

class DSmoothVAdd (M : Type u_1) (X : Type u_2) [VAdd M X] [DiffeologicalSpace M] [DiffeologicalSpace X] : Prop

Class ContinuousVAdd M X saying that the additive action (+ᵥ) : M → X → X is smooth in both arguments.

• dsmooth_vadd : DSmooth fun (p : M × X) => p.1 +ᵥ p.2

class DSmoothSMul (M : Type u_1) (X : Type u_2) [SMul M X] [DiffeologicalSpace M] [DiffeologicalSpace X] : Prop

Class DSmoothSMul M X saying that the scalar multiplication (•) : M → X → X is smooth in both arguments.

• dsmooth_smul : DSmooth fun (p : M × X) => p.1 • p.2

instance instDSmoothSMulULift {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [SMul M X] [DSmoothSMul M X] : DSmoothSMul (ULift.{u_4, u_1} M) X

instance instDSmoothVAddULift {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [VAdd M X] [DSmoothVAdd M X] : DSmoothVAdd (ULift.{u_4, u_1} M) X

theorem DSmooth.smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [SMul M X] [DSmoothSMul M X] {f : Y → M} {g : Y → X} (hf : DSmooth f) (hg : DSmooth g) : DSmooth fun (x : Y) => f x • g x

theorem DSmooth.vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [VAdd M X] [DSmoothVAdd M X] {f : Y → M} {g : Y → X} (hf : DSmooth f) (hg : DSmooth g) : DSmooth fun (x : Y) => f x +ᵥ g x

instance DSmoothSMul.op {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [SMul M X] [DSmoothSMul M X] [SMul Mᵐᵒᵖ X] [IsCentralScalar M X] : DSmoothSMul Mᵐᵒᵖ X

instance DSmoothVAdd.op {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [VAdd M X] [DSmoothVAdd M X] [VAdd Mᵃᵒᵖ X] [IsCentralVAdd M X] : DSmoothVAdd Mᵃᵒᵖ X

instance MulOpposite.dsmoothSMul {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [SMul M X] [DSmoothSMul M X] : DSmoothSMul M Xᵐᵒᵖ

instance AddOpposite.dsmoothVAdd {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [VAdd M X] [DSmoothVAdd M X] : DSmoothVAdd M Xᵃᵒᵖ

theorem dsmoothSMul_induced {M : Type u_1} {X : Type u_2} {Y : Type u_3} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [SMul M X] [DSmoothSMul M X] {N : Type u_4} [SMul N Y] [DiffeologicalSpace N] (g : Y → X) {f : N → M} (hf : DSmooth f) (hsmul : ∀ {c : N} {x : Y}, g (c • x) = f c • g x) : DSmoothSMul N Y

For any action homomorphism where the action on the codomain is smooth, the induced diffeology makes the action on the domain smooth too.

theorem dsmoothVAdd_induced {M : Type u_1} {X : Type u_2} {Y : Type u_3} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [VAdd M X] [DSmoothVAdd M X] {N : Type u_4} [VAdd N Y] [DiffeologicalSpace N] (g : Y → X) {f : N → M} (hf : DSmooth f) (hvadd : ∀ {c : N} {x : Y}, g (c +ᵥ x) = f c +ᵥ g x) : DSmoothVAdd N Y

For any action homomorphism where the action on the codomain is smooth, the induced diffeology makes the action on the domain smooth too.

theorem IsDInducing.dsmoothSMul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [SMul M X] [DSmoothSMul M X] {N : Type u_4} [SMul N Y] [DiffeologicalSpace N] {g : Y → X} {f : N → M} (hg : IsDInducing g) (hf : DSmooth f) (hsmul : ∀ {c : N} {x : Y}, g (c • x) = f c • g x) : DSmoothSMul N Y

For any action homomorphism where the action on the codomain is smooth, the induced diffeology makes the action on the domain smooth too.

theorem IsDInducing.dsmoothVAdd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [VAdd M X] [DSmoothVAdd M X] {N : Type u_4} [VAdd N Y] [DiffeologicalSpace N] {g : Y → X} {f : N → M} (hg : IsDInducing g) (hf : DSmooth f) (hvadd : ∀ {c : N} {x : Y}, g (c +ᵥ x) = f c +ᵥ g x) : DSmoothVAdd N Y

For any action homomorphism where the action on the codomain is smooth, the induced diffeology makes the action on the domain smooth too.

instance SMulMemClass.dsmoothSMul {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [SMul M X] [DSmoothSMul M X] {S : Type u_4} [SetLike S X] [SMulMemClass S M X] (s : S) : DSmoothSMul M ↥s

instance VAddMemClass.dsmoothVAdd {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [VAdd M X] [DSmoothVAdd M X] {S : Type u_4} [SetLike S X] [VAddMemClass S M X] (s : S) : DSmoothVAdd M ↥s

instance Units.dsmoothSMul {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [Monoid M] [MulAction M X] [DSmoothSMul M X] : DSmoothSMul Mˣ X

instance AddUnits.dsmoothVAdd {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [AddMonoid M] [AddAction M X] [DSmoothVAdd M X] : DSmoothVAdd (AddUnits M) X

theorem MulAction.dsmoothSMul_compHom {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [Monoid M] [MulAction M X] [DSmoothSMul M X] {N : Type u_4} [DiffeologicalSpace N] [Monoid N] {f : N →* M} (hf : DSmooth ⇑f) : DSmoothSMul N X

Composing a smooth action with a smooth homomorphism results in a smooth action.

theorem AddAction.dsmoothVAdd_compHom {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [AddMonoid M] [AddAction M X] [DSmoothVAdd M X] {N : Type u_4} [DiffeologicalSpace N] [AddMonoid N] {f : N →+ M} (hf : DSmooth ⇑f) : DSmoothVAdd N X

instance Submonoid.dsmoothSMul {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [Monoid M] [MulAction M X] [DSmoothSMul M X] {S : Submonoid M} : DSmoothSMul (↥S) X

instance AddSubmonoid.dsmoothVAdd {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [AddMonoid M] [AddAction M X] [DSmoothVAdd M X] {S : AddSubmonoid M} : DSmoothVAdd (↥S) X

instance Subgroup.dsmoothSMul {M : Type u_1} {X : Type u_2} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [Group M] [MulAction M X] [DSmoothSMul M X] {S : Subgroup M} : DSmoothSMul (↥S) X

instance Prod.dsmoothSMul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [SMul M X] [SMul M Y] [DSmoothSMul M X] [DSmoothSMul M Y] : DSmoothSMul M (X × Y)

instance Prod.dsmoothVAdd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [DiffeologicalSpace M] [dX : DiffeologicalSpace X] [dY : DiffeologicalSpace Y] [VAdd M X] [VAdd M Y] [DSmoothVAdd M X] [DSmoothVAdd M Y] : DSmoothVAdd M (X × Y)

instance instDSmoothSMulForall {M : Type u_1} [DiffeologicalSpace M] {ι : Type u_4} {γ : ι → Type u_5} [(i : ι) → DiffeologicalSpace (γ i)] [(i : ι) → SMul M (γ i)] [∀ (i : ι), DSmoothSMul M (γ i)] : DSmoothSMul M ((i : ι) → γ i)

instance instDSmoothVAddForall {M : Type u_1} [DiffeologicalSpace M] {ι : Type u_4} {γ : ι → Type u_5} [(i : ι) → DiffeologicalSpace (γ i)] [(i : ι) → VAdd M (γ i)] [∀ (i : ι), DSmoothVAdd M (γ i)] : DSmoothVAdd M ((i : ι) → γ i)

theorem dsmoothSMul_sInf {M : Type u_1} [DiffeologicalSpace M] {X : Type u_4} [SMul M X] {D : Set (DiffeologicalSpace X)} (h : ∀ d ∈ D, DSmoothSMul M X) : DSmoothSMul M X

theorem dsmoothVAdd_sInf {M : Type u_1} [DiffeologicalSpace M] {X : Type u_4} [VAdd M X] {D : Set (DiffeologicalSpace X)} (h : ∀ d ∈ D, DSmoothVAdd M X) : DSmoothVAdd M X

theorem dsmoothSMul_iInf {M : Type u_1} [DiffeologicalSpace M] {X : Type u_4} {ι : Type u_5} [SMul M X] {D : ι → DiffeologicalSpace X} (h : ∀ (i : ι), DSmoothSMul M X) : DSmoothSMul M X

theorem dsmoothVAdd_iInf {M : Type u_1} [DiffeologicalSpace M] {X : Type u_4} {ι : Type u_5} [VAdd M X] {D : ι → DiffeologicalSpace X} (h : ∀ (i : ι), DSmoothVAdd M X) : DSmoothVAdd M X

theorem dsmoothSMul_inf {M : Type u_1} [DiffeologicalSpace M] {X : Type u_4} [SMul M X] {d₁ d₂ : DiffeologicalSpace X} [DSmoothSMul M X] [DSmoothSMul M X] : DSmoothSMul M X

theorem dsmoothVAdd_inf {M : Type u_1} [DiffeologicalSpace M] {X : Type u_4} [VAdd M X] {d₁ d₂ : DiffeologicalSpace X} [DSmoothVAdd M X] [DSmoothVAdd M X] : DSmoothVAdd M X

theorem DSmoothSMul.continuousSMul {M : Type u_4} {X : Type u_5} [SMul M X] [DiffeologicalSpace M] [DiffeologicalSpace X] [DSmoothSMul M X] [LocallyCompactSpace X] : ContinuousSMul M X

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

theorem DSmoothVAdd.continuousVAdd {M : Type u_4} {X : Type u_5} [VAdd M X] [DiffeologicalSpace M] [DiffeologicalSpace X] [DSmoothVAdd M X] [LocallyCompactSpace X] : ContinuousVAdd M X

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

instance instContinuousSMulOfDTopCompatibleOfDSmoothSMulOfLocallyCompactSpace {M : Type u_4} {X : Type u_5} [SMul M X] [DiffeologicalSpace M] [DiffeologicalSpace X] [TopologicalSpace M] [TopologicalSpace X] [DTopCompatible M] [DTopCompatible X] [DSmoothSMul M X] [LocallyCompactSpace X] : ContinuousSMul M X

Variant of DSmoothSMul.continuousSMul phrased in terms of spaces equipped with DTopCompatible topologies.

instance instContinuousVAddOfDTopCompatibleOfDSmoothVAddOfLocallyCompactSpace {M : Type u_4} {X : Type u_5} [VAdd M X] [DiffeologicalSpace M] [DiffeologicalSpace X] [TopologicalSpace M] [TopologicalSpace X] [DTopCompatible M] [DTopCompatible X] [DSmoothVAdd M X] [LocallyCompactSpace X] : ContinuousVAdd M X

Variant of DSmoothVAdd.continuousVAdd phrased in terms of spaces equipped with DTopCompatible topologies.