# mathlibdocumentation

topology.algebra.mul_action

# Continuous monoid action #

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

## Main definitions #

• has_continuous_smul M α : typeclass saying that the map (c, x) ↦ c • x is continuous on M × α;
• homeomorph.smul_of_unit: scalar multiplication by a unit of M as a homeomorphism of α;
• homeomorph.smul_of_ne_zero: if a group with zero G₀ (e.g., a field) acts on α and c : G₀ is a nonzero element of G₀, then scalar multiplication by c is a homeomorphism of α;
• homeomorph.smul: scalar multiplication by an element of a group G acting on α is a homeomorphism of α.

## 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) (α : Type u_2) [ α]  :
Prop

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

Instances
theorem filter.tendsto.smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [ α] [ α] {f : β → M} {g : β → α} {l : filter β} {c : M} {a : α} (hf : (𝓝 c)) (hg : (𝓝 a)) :
filter.tendsto (λ (x : β), f x g x) l (𝓝 (c a))
theorem filter.tendsto.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [ α] [ α] {f : β → α} {l : filter β} {a : α} (hf : (𝓝 a)) (c : M) :
filter.tendsto (λ (x : β), c f x) l (𝓝 (c a))
theorem filter.tendsto.smul_const {M : Type u_1} {α : Type u_2} {β : Type u_3} [ α] [ α] {f : β → M} {l : filter β} {c : M} (hf : (𝓝 c)) (a : α) :
filter.tendsto (λ (x : β), f x a) l (𝓝 (c a))
theorem continuous_within_at.smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [ α] [ α] {f : β → M} {g : β → α} {b : β} {s : set β} (hf : b) (hg : b) :
continuous_within_at (λ (x : β), f x g x) s b
theorem continuous_within_at.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [ α] [ α] {g : β → α} {b : β} {s : set β} (hg : b) (c : M) :
continuous_within_at (λ (x : β), c g x) s b
theorem continuous_at.smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [ α] [ α] {f : β → M} {g : β → α} {b : β} (hf : b) (hg : b) :
continuous_at (λ (x : β), f x g x) b
theorem continuous_at.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [ α] [ α] {g : β → α} {b : β} (hg : b) (c : M) :
continuous_at (λ (x : β), c g x) b
theorem continuous_on.smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [ α] [ α] {f : β → M} {g : β → α} {s : set β} (hf : s) (hg : s) :
continuous_on (λ (x : β), f x g x) s
theorem continuous_on.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [ α] [ α] {g : β → α} {s : set β} (hg : s) (c : M) :
continuous_on (λ (x : β), c g x) s
theorem continuous.smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [ α] [ α] {f : β → M} {g : β → α} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : β), f x g x)
theorem continuous.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [ α] [ α] {g : β → α} (hg : continuous g) (c : M) :
continuous (λ (x : β), c g x)
theorem units.tendsto_const_smul_iff {M : Type u_1} {α : Type u_2} {β : Type u_3} [monoid M] [ α] [ α] {f : β → α} {l : filter β} {a : α} (u : units M) :
filter.tendsto (λ (x : β), u f x) l (𝓝 (u a)) (𝓝 a)
theorem is_unit.tendsto_const_smul_iff {M : Type u_1} {α : Type u_2} {β : Type u_3} [monoid M] [ α] [ α] {f : β → α} {l : filter β} {a : α} {c : M} (hc : is_unit c) :
filter.tendsto (λ (x : β), c f x) l (𝓝 (c a)) (𝓝 a)
theorem is_unit.continuous_within_at_const_smul_iff {M : Type u_1} {α : Type u_2} {β : Type u_3} [monoid M] [ α] [ α] {f : β → α} {b : β} {c : M} {s : set β} (hc : is_unit c) :
continuous_within_at (λ (x : β), c f x) s b b
theorem is_unit.continuous_on_const_smul_iff {M : Type u_1} {α : Type u_2} {β : Type u_3} [monoid M] [ α] [ α] {f : β → α} {c : M} {s : set β} (hc : is_unit c) :
continuous_on (λ (x : β), c f x) s
theorem is_unit.continuous_at_const_smul_iff {M : Type u_1} {α : Type u_2} {β : Type u_3} [monoid M] [ α] [ α] {f : β → α} {b : β} {c : M} (hc : is_unit c) :
continuous_at (λ (x : β), c f x) b
theorem is_unit.continuous_const_smul_iff {M : Type u_1} {α : Type u_2} {β : Type u_3} [monoid M] [ α] [ α] {f : β → α} {c : M} (hc : is_unit c) :
continuous (λ (x : β), c f x)
def homeomorph.smul_of_unit {M : Type u_1} {α : Type u_2} [monoid M] [ α] [ α] (u : units M) :
α ≃ₜ α

Scalar multiplication by a unit of a monoid M acting on α is a homeomorphism from α to itself.

Equations
theorem is_unit.is_open_map_smul {M : Type u_1} {α : Type u_2} [monoid M] [ α] [ α] {c : M} (hc : is_unit c) :
is_open_map (λ (x : α), c x)
theorem is_unit.is_closed_map_smul {M : Type u_1} {α : Type u_2} [monoid M] [ α] [ α] {c : M} (hc : is_unit c) :
is_closed_map (λ (x : α), c x)
theorem tendsto_const_smul_iff' {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [group_with_zero G₀] [ α] [ α] {f : β → α} {l : filter β} {a : α} {c : G₀} (hc : c 0) :
filter.tendsto (λ (x : β), c f x) l (𝓝 (c a)) (𝓝 a)
theorem continuous_within_at_const_smul_iff' {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [group_with_zero G₀] [ α] [ α] {f : β → α} {b : β} {c : G₀} {s : set β} (hc : c 0) :
continuous_within_at (λ (x : β), c f x) s b b
theorem continuous_on_const_smul_iff' {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [group_with_zero G₀] [ α] [ α] {f : β → α} {c : G₀} {s : set β} (hc : c 0) :
continuous_on (λ (x : β), c f x) s
theorem continuous_at_const_smul_iff' {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [group_with_zero G₀] [ α] [ α] {f : β → α} {b : β} {c : G₀} (hc : c 0) :
continuous_at (λ (x : β), c f x) b
theorem continuous_const_smul_iff' {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [group_with_zero G₀] [ α] [ α] {f : β → α} {c : G₀} (hc : c 0) :
continuous (λ (x : β), c f x)
def homeomorph.smul_of_ne_zero {α : Type u_2} {G₀ : Type u_4} [group_with_zero G₀] [ α] [ α] (c : G₀) (hc : c 0) :
α ≃ₜ α

Scalar multiplication by a non-zero element of a group with zero acting on α is a homeomorphism from α onto itself.

Equations
theorem is_open_map_smul' {α : Type u_2} {G₀ : Type u_4} [group_with_zero G₀] [ α] [ α] {c : G₀} (hc : c 0) :
is_open_map (λ (x : α), c x)
theorem is_closed_map_smul' {α : Type u_2} {G₀ : Type u_4} [group_with_zero G₀] [ α] [ α] {c : G₀} (hc : c 0) :
is_closed_map (λ (x : α), c x)

smul is a closed map in the second argument.

The lemma that smul is a closed map in the first argument (for a normed space over a complete normed field) is is_closed_map_smul_left in analysis.normed_space.finite_dimension.

theorem tendsto_const_smul_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [group G] [ α] [ α] {f : β → α} {l : filter β} {a : α} (c : G) :
filter.tendsto (λ (x : β), c f x) l (𝓝 (c a)) (𝓝 a)
theorem continuous_within_at_const_smul_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [group G] [ α] [ α] {f : β → α} {b : β} {s : set β} (c : G) :
continuous_within_at (λ (x : β), c f x) s b b
theorem continuous_on_const_smul_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [group G] [ α] [ α] {f : β → α} {s : set β} (c : G) :
continuous_on (λ (x : β), c f x) s
theorem continuous_at_const_smul_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [group G] [ α] [ α] {f : β → α} {b : β} (c : G) :
continuous_at (λ (x : β), c f x) b
theorem continuous_const_smul_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [group G] [ α] [ α] {f : β → α} (c : G) :
continuous (λ (x : β), c f x)
def homeomorph.smul {α : Type u_2} {G : Type u_4} [group G] [ α] [ α] (c : G) :
α ≃ₜ α

Scalar multiplication by a unit of a monoid M acting on α is a homeomorphism from α to itself.

Equations
theorem is_open_map_smul {α : Type u_2} {G : Type u_4} [group G] [ α] [ α] (c : G) :
is_open_map (λ (x : α), c x)
theorem is_closed_map_smul {α : Type u_2} {G : Type u_4} [group G] [ α] [ α] (c : G) :
is_closed_map (λ (x : α), c x)
@[instance]
def has_continuous_mul.has_continuous_smul {M : Type u_1} [monoid M]  :
@[instance]
def prod.has_continuous_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [ α] [ β] [ α] [ β] :
× β)