# mathlibdocumentation

topology.algebra.mul_action

# Continuous monoid action #

In this file we define class has_continuous_smul. We say has_continuous_smul 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 #

• has_continuous_smul M X : typeclass saying that the map (c, x) ↦ c • x is continuous on M × X;
• 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.
• units.has_continuous_smul: 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ˣ.

## 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 continuous_smul.

@[class]
structure has_continuous_smul (M : Type u_1) (X : Type u_2) [ X]  :
Prop

Class has_continuous_smul 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 of this typeclass
@[class]
structure has_continuous_vadd (M : Type u_1) (X : Type u_2) [ X]  :
Prop

Class has_continuous_vadd 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 of this typeclass
@[protected, instance]
def has_continuous_smul.has_continuous_const_smul {M : Type u_1} {X : Type u_2} [ X] [ X] :
@[protected, instance]
def has_continuous_vadd.has_continuous_const_vadd {M : Type u_1} {X : Type u_2} [ X] [ X] :
theorem filter.tendsto.vadd {M : Type u_1} {X : Type u_2} {α : Type u_4} [ X] [ X] {f : α → M} {g : α → X} {l : filter α} {c : M} {a : X} (hf : (nhds c)) (hg : (nhds a)) :
filter.tendsto (λ (x : α), f x +ᵥ g x) l (nhds (c +ᵥ a))
theorem filter.tendsto.smul {M : Type u_1} {X : Type u_2} {α : Type u_4} [ X] [ X] {f : α → M} {g : α → X} {l : filter α} {c : M} {a : X} (hf : (nhds c)) (hg : (nhds a)) :
filter.tendsto (λ (x : α), f x g x) l (nhds (c a))
theorem filter.tendsto.smul_const {M : Type u_1} {X : Type u_2} {α : Type u_4} [ X] [ X] {f : α → M} {l : filter α} {c : M} (hf : (nhds c)) (a : X) :
filter.tendsto (λ (x : α), f x a) l (nhds (c a))
theorem filter.tendsto.vadd_const {M : Type u_1} {X : Type u_2} {α : Type u_4} [ X] [ X] {f : α → M} {l : filter α} {c : M} (hf : (nhds c)) (a : X) :
filter.tendsto (λ (x : α), f x +ᵥ a) l (nhds (c +ᵥ a))
theorem continuous_within_at.smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [ X] [ X] {f : Y → M} {g : Y → X} {b : Y} {s : set Y} (hf : b) (hg : b) :
continuous_within_at (λ (x : Y), f x g x) s b
theorem continuous_within_at.vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [ X] [ X] {f : Y → M} {g : Y → X} {b : Y} {s : set Y} (hf : b) (hg : b) :
continuous_within_at (λ (x : Y), f x +ᵥ g x) s b
theorem continuous_at.smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [ X] [ X] {f : Y → M} {g : Y → X} {b : Y} (hf : b) (hg : b) :
continuous_at (λ (x : Y), f x g x) b
theorem continuous_at.vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [ X] [ X] {f : Y → M} {g : Y → X} {b : Y} (hf : b) (hg : b) :
continuous_at (λ (x : Y), f x +ᵥ g x) b
theorem continuous_on.vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [ X] [ X] {f : Y → M} {g : Y → X} {s : set Y} (hf : s) (hg : s) :
continuous_on (λ (x : Y), f x +ᵥ g x) s
theorem continuous_on.smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [ X] [ X] {f : Y → M} {g : Y → X} {s : set Y} (hf : s) (hg : s) :
continuous_on (λ (x : Y), f x g x) s
@[continuity]
theorem continuous.smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [ X] [ X] {f : Y → M} {g : Y → X} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : Y), f x g x)
@[continuity]
theorem continuous.vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [ X] [ X] {f : Y → M} {g : Y → X} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : Y), f x +ᵥ g x)
@[protected, instance]
def has_continuous_smul.op {M : Type u_1} {X : Type u_2} [ X] [ X] [ X] [ X] :

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

@[protected, instance]
def add_opposite.has_continuous_vadd {M : Type u_1} {X : Type u_2} [ X] [ X] :
@[protected, instance]
def mul_opposite.has_continuous_smul {M : Type u_1} {X : Type u_2} [ X] [ X] :
@[protected, instance]
def units.has_continuous_smul {M : Type u_1} {X : Type u_2} [monoid M] [ X] [ X] :
@[protected, instance]
def add_units.has_continuous_vadd {M : Type u_1} {X : Type u_2} [add_monoid M] [ X] [ X] :
@[protected, instance]
def prod.has_continuous_smul {M : Type u_1} {X : Type u_2} {Y : Type u_3} [ X] [ Y] [ X] [ Y] :
(X × Y)
@[protected, instance]
def prod.has_continuous_vadd {M : Type u_1} {X : Type u_2} {Y : Type u_3} [ X] [ Y] [ X] [ Y] :
(X × Y)
@[protected, instance]
def pi.has_continuous_vadd {M : Type u_1} {ι : Type u_2} {γ : ι → Type u_3} [Π (i : ι), topological_space (γ i)] [Π (i : ι), (γ i)] [∀ (i : ι), (γ i)] :
(Π (i : ι), γ i)
@[protected, instance]
def pi.has_continuous_smul {M : Type u_1} {ι : Type u_2} {γ : ι → Type u_3} [Π (i : ι), topological_space (γ i)] [Π (i : ι), (γ i)] [∀ (i : ι), (γ i)] :
(Π (i : ι), γ i)
theorem has_continuous_vadd_Inf {M : Type u_2} {X : Type u_3} [ X] {ts : set } (h : ∀ (t : , t ts) :
theorem has_continuous_smul_Inf {M : Type u_2} {X : Type u_3} [ X] {ts : set } (h : ∀ (t : , t ts) :
theorem has_continuous_vadd_infi {ι : Sort u_1} {M : Type u_2} {X : Type u_3} [ X] {ts' : ι → } (h : ∀ (i : ι), ) :
theorem has_continuous_smul_infi {ι : Sort u_1} {M : Type u_2} {X : Type u_3} [ X] {ts' : ι → } (h : ∀ (i : ι), ) :
theorem has_continuous_vadd_inf {M : Type u_2} {X : Type u_3} [ X] {t₁ t₂ : topological_space X} [ X] [ X] :
theorem has_continuous_smul_inf {M : Type u_2} {X : Type u_3} [ X] {t₁ t₂ : topological_space X} [ X] [ X] :