# Documentation

Mathlib.Topology.Algebra.MulAction

# Continuous monoid action #

In this file we define class ContinuousSMul. We say ContinuousSMul M X if M acts on X and the map (c, x) ↦ c • x is continuous on M × X. We reuse this class for topological (semi)modules, vector spaces and algebras.

## Main definitions #

• ContinuousSMul M X : typeclass saying that the map (c, x) ↦ c • x is continuous on M × X;
• Units.continuousSMul: scalar multiplication by Mˣ is continuous when scalar multiplication by M is continuous. This allows Homeomorph.smul to be used with on monoids with G = Mˣ.

-- Porting note: These have all moved

• Homeomorph.smul_of_ne_zero: if a group with zero G₀ (e.g., a field) acts on X and c : G₀ is a nonzero element of G₀, then scalar multiplication by c is a homeomorphism of X;
• Homeomorph.smul: scalar multiplication by an element of a group G acting on X is a homeomorphism of X.

## Main results #

Besides homeomorphisms mentioned above, in this file we provide lemmas like Continuous.smul or Filter.Tendsto.smul that provide dot-syntax access to ContinuousSMul.

class ContinuousSMul (M : Type u_1) (X : Type u_2) [SMul M X] [] [] :
• continuous_smul : Continuous fun p => p.fst p.snd

The scalar multiplication (•) is continuous.

Class ContinuousSMul M X says that the scalar multiplication (•) : M → X → X is continuous in both arguments. We use the same class for all kinds of multiplicative actions, including (semi)modules and algebras.

Instances
class ContinuousVAdd (M : Type u_1) (X : Type u_2) [VAdd M X] [] [] :
• continuous_vadd : Continuous fun p => p.fst +ᵥ p.snd

The additive action (+ᵥ) is continuous.

Class ContinuousVAdd M X says that the additive action (+ᵥ) : M → X → X is continuous in both arguments. We use the same class for all kinds of additive actions, including (semi)modules and algebras.

Instances
instance ContinuousVAdd.continuousConstVAdd {M : Type u_1} {X : Type u_2} [] [] [VAdd M X] [] :
theorem ContinuousVAdd.continuousConstVAdd.proof_1 {M : Type u_1} {X : Type u_2} [] [] [VAdd M X] [] :
instance ContinuousSMul.continuousConstSMul {M : Type u_1} {X : Type u_2} [] [] [SMul M X] [] :
theorem Filter.Tendsto.vadd {M : Type u_1} {X : Type u_2} {α : Type u_4} [] [] [VAdd M X] [] {f : αM} {g : αX} {l : } {c : M} {a : X} (hf : Filter.Tendsto f l (nhds c)) (hg : Filter.Tendsto g l (nhds a)) :
Filter.Tendsto (fun x => f x +ᵥ g x) l (nhds (c +ᵥ a))
theorem Filter.Tendsto.smul {M : Type u_1} {X : Type u_2} {α : Type u_4} [] [] [SMul M X] [] {f : αM} {g : αX} {l : } {c : M} {a : X} (hf : Filter.Tendsto f l (nhds c)) (hg : Filter.Tendsto g l (nhds a)) :
Filter.Tendsto (fun x => f x g x) l (nhds (c a))
theorem Filter.Tendsto.vadd_const {M : Type u_1} {X : Type u_2} {α : Type u_4} [] [] [VAdd M X] [] {f : αM} {l : } {c : M} (hf : Filter.Tendsto f l (nhds c)) (a : X) :
Filter.Tendsto (fun x => f x +ᵥ a) l (nhds (c +ᵥ a))
theorem Filter.Tendsto.smul_const {M : Type u_1} {X : Type u_2} {α : Type u_4} [] [] [SMul M X] [] {f : αM} {l : } {c : M} (hf : Filter.Tendsto f l (nhds c)) (a : X) :
Filter.Tendsto (fun x => f x a) l (nhds (c a))
theorem ContinuousWithinAt.vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [] [] [] [VAdd M X] [] {f : YM} {g : YX} {b : Y} {s : Set Y} (hf : ) (hg : ) :
ContinuousWithinAt (fun x => f x +ᵥ g x) s b
theorem ContinuousWithinAt.smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [] [] [] [SMul M X] [] {f : YM} {g : YX} {b : Y} {s : Set Y} (hf : ) (hg : ) :
ContinuousWithinAt (fun x => f x g x) s b
theorem ContinuousAt.vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [] [] [] [VAdd M X] [] {f : YM} {g : YX} {b : Y} (hf : ) (hg : ) :
ContinuousAt (fun x => f x +ᵥ g x) b
theorem ContinuousAt.smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [] [] [] [SMul M X] [] {f : YM} {g : YX} {b : Y} (hf : ) (hg : ) :
ContinuousAt (fun x => f x g x) b
theorem ContinuousOn.vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [] [] [] [VAdd M X] [] {f : YM} {g : YX} {s : Set Y} (hf : ) (hg : ) :
ContinuousOn (fun x => f x +ᵥ g x) s
theorem ContinuousOn.smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [] [] [] [SMul M X] [] {f : YM} {g : YX} {s : Set Y} (hf : ) (hg : ) :
ContinuousOn (fun x => f x g x) s
theorem Continuous.vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [] [] [] [VAdd M X] [] {f : YM} {g : YX} (hf : ) (hg : ) :
Continuous fun x => f x +ᵥ g x
theorem Continuous.smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [] [] [] [SMul M X] [] {f : YM} {g : YX} (hf : ) (hg : ) :
Continuous fun x => f x g x
theorem ContinuousVAdd.op.proof_1 {M : Type u_1} {X : Type u_2} [] [] [VAdd M X] [] [VAdd Mᵃᵒᵖ X] [] :
instance ContinuousVAdd.op {M : Type u_1} {X : Type u_2} [] [] [VAdd M X] [] [VAdd Mᵃᵒᵖ X] [] :

If an additive action is central, then its right action is continuous when its left action is.

instance ContinuousSMul.op {M : Type u_1} {X : Type u_2} [] [] [SMul M X] [] [SMul Mᵐᵒᵖ X] [] :

If a scalar action is central, then its right action is continuous when its left action is.

theorem AddOpposite.continuousVAdd.proof_1 {M : Type u_1} {X : Type u_2} [] [] [VAdd M X] [] :
instance AddOpposite.continuousVAdd {M : Type u_1} {X : Type u_2} [] [] [VAdd M X] [] :
instance MulOpposite.continuousSMul {M : Type u_1} {X : Type u_2} [] [] [SMul M X] [] :
theorem AddUnits.continuousVAdd.proof_1 {M : Type u_1} {X : Type u_2} [] [] [] [] [] :
instance AddUnits.continuousVAdd {M : Type u_1} {X : Type u_2} [] [] [] [] [] :
instance Units.continuousSMul {M : Type u_1} {X : Type u_2} [] [] [] [] [] :
instance AddSubmonoid.continuousVAdd {M : Type u_1} {X : Type u_2} [] [] [] [] [] {S : } :
ContinuousVAdd { x // x S } X
theorem AddSubmonoid.continuousVAdd.proof_1 {M : Type u_1} {X : Type u_2} [] [] [] [] [] {S : } :
ContinuousVAdd { x // x S } X
instance Submonoid.continuousSMul {M : Type u_1} {X : Type u_2} [] [] [] [] [] {S : } :
ContinuousSMul { x // x S } X
theorem AddSubgroup.continuousVAdd.proof_1 {M : Type u_1} {X : Type u_2} [] [] [] [] [] {S : } :
ContinuousVAdd { x // x S } X
instance AddSubgroup.continuousVAdd {M : Type u_1} {X : Type u_2} [] [] [] [] [] {S : } :
ContinuousVAdd { x // x S } X
instance Subgroup.continuousSMul {M : Type u_1} {X : Type u_2} [] [] [] [] [] {S : } :
ContinuousSMul { x // x S } X
instance Prod.continuousVAdd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [] [] [] [VAdd M X] [VAdd M Y] [] [] :
theorem Prod.continuousVAdd.proof_1 {M : Type u_1} {X : Type u_2} {Y : Type u_3} [] [] [] [VAdd M X] [VAdd M Y] [] [] :
instance Prod.continuousSMul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [] [] [] [SMul M X] [SMul M Y] [] [] :
theorem instContinuousVAddForAllInstVAddTopologicalSpace.proof_1 {M : Type u_1} [] {ι : Type u_2} {γ : ιType u_3} [(i : ι) → TopologicalSpace (γ i)] [(i : ι) → VAdd M (γ i)] [∀ (i : ι), ContinuousVAdd M (γ i)] :
ContinuousVAdd M ((i : ι) → γ i)
instance instContinuousVAddForAllInstVAddTopologicalSpace {M : Type u_1} [] {ι : Type u_5} {γ : ιType u_6} [(i : ι) → TopologicalSpace (γ i)] [(i : ι) → VAdd M (γ i)] [∀ (i : ι), ContinuousVAdd M (γ i)] :
ContinuousVAdd M ((i : ι) → γ i)
instance instContinuousSMulForAllInstSMulTopologicalSpace {M : Type u_1} [] {ι : Type u_5} {γ : ιType u_6} [(i : ι) → TopologicalSpace (γ i)] [(i : ι) → SMul M (γ i)] [∀ (i : ι), ContinuousSMul M (γ i)] :
ContinuousSMul M ((i : ι) → γ i)
theorem continuousVAdd_sInf {M : Type u_2} {X : Type u_3} [] [VAdd M X] {ts : } (h : ∀ (t : ), t ts) :
theorem continuousSMul_sInf {M : Type u_2} {X : Type u_3} [] [SMul M X] {ts : } (h : ∀ (t : ), t ts) :
theorem continuousVAdd_iInf {ι : Sort u_1} {M : Type u_2} {X : Type u_3} [] [VAdd M X] {ts' : ι} (h : ∀ (i : ι), ) :
theorem continuousSMul_iInf {ι : Sort u_1} {M : Type u_2} {X : Type u_3} [] [SMul M X] {ts' : ι} (h : ∀ (i : ι), ) :
theorem continuousVAdd_inf {M : Type u_2} {X : Type u_3} [] [VAdd M X] {t₁ : } {t₂ : } [] [] :
theorem continuousSMul_inf {M : Type u_2} {X : Type u_3} [] [SMul M X] {t₁ : } {t₂ : } [] [] :
theorem AddTorsor.connectedSpace (G : Type u_1) (P : Type u_2) [] [] [] [] [] :

An AddTorsor for a connected space is a connected space. This is not an instance because it loops for a group as a torsor over itself.