mathlib documentation

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 #

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) [has_scalar M α] [topological_space M] [topological_space α] :
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} [topological_space M] [topological_space α] [has_scalar M α] [has_continuous_smul M α] {f : β → M} {g : β → α} {l : filter β} {c : M} {a : α} (hf : filter.tendsto f l (𝓝 c)) (hg : filter.tendsto g l (𝓝 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} [topological_space M] [topological_space α] [has_scalar M α] [has_continuous_smul M α] {f : β → α} {l : filter β} {a : α} (hf : filter.tendsto f l (𝓝 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} [topological_space M] [topological_space α] [has_scalar M α] [has_continuous_smul M α] {f : β → M} {l : filter β} {c : M} (hf : filter.tendsto f l (𝓝 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} [topological_space M] [topological_space α] [has_scalar M α] [has_continuous_smul M α] [topological_space β] {f : β → M} {g : β → α} {b : β} {s : set β} (hf : continuous_within_at f s b) (hg : continuous_within_at g s 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} [topological_space M] [topological_space α] [has_scalar M α] [has_continuous_smul M α] [topological_space β] {g : β → α} {b : β} {s : set β} (hg : continuous_within_at g s 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} [topological_space M] [topological_space α] [has_scalar M α] [has_continuous_smul M α] [topological_space β] {f : β → M} {g : β → α} {b : β} (hf : continuous_at f b) (hg : continuous_at g b) :
continuous_at (λ (x : β), f x g x) b
theorem continuous_at.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space M] [topological_space α] [has_scalar M α] [has_continuous_smul M α] [topological_space β] {g : β → α} {b : β} (hg : continuous_at g b) (c : M) :
continuous_at (λ (x : β), c g x) b
theorem continuous_on.smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space M] [topological_space α] [has_scalar M α] [has_continuous_smul M α] [topological_space β] {f : β → M} {g : β → α} {s : set β} (hf : continuous_on f s) (hg : continuous_on g s) :
continuous_on (λ (x : β), f x g x) s
theorem continuous_on.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space M] [topological_space α] [has_scalar M α] [has_continuous_smul M α] [topological_space β] {g : β → α} {s : set β} (hg : continuous_on g s) (c : M) :
continuous_on (λ (x : β), c g x) s
theorem continuous.smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space M] [topological_space α] [has_scalar M α] [has_continuous_smul M α] [topological_space β] {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} [topological_space M] [topological_space α] [has_scalar M α] [has_continuous_smul M α] [topological_space β] {g : β → α} (hg : continuous g) (c : M) :
continuous (λ (x : β), c g x)
@[instance]
def units.has_continuous_smul {M : Type u_1} {α : Type u_2} [topological_space M] [topological_space α] [monoid M] [mul_action M α] [has_continuous_smul M α] :
theorem tendsto_const_smul_iff {α : Type u_2} {β : Type u_3} [topological_space α] {G : Type u_4} [topological_space G] [group G] [mul_action G α] [has_continuous_smul G α] {f : β → α} {l : filter β} {a : α} (c : G) :
filter.tendsto (λ (x : β), c f x) l (𝓝 (c a)) filter.tendsto f l (𝓝 a)
theorem continuous_within_at_const_smul_iff {α : Type u_2} {β : Type u_3} [topological_space α] {G : Type u_4} [topological_space G] [group G] [mul_action G α] [has_continuous_smul G α] [topological_space β] {f : β → α} {b : β} {s : set β} (c : G) :
continuous_within_at (λ (x : β), c f x) s b continuous_within_at f s b
theorem continuous_on_const_smul_iff {α : Type u_2} {β : Type u_3} [topological_space α] {G : Type u_4} [topological_space G] [group G] [mul_action G α] [has_continuous_smul G α] [topological_space β] {f : β → α} {s : set β} (c : G) :
continuous_on (λ (x : β), c f x) s continuous_on f s
theorem continuous_at_const_smul_iff {α : Type u_2} {β : Type u_3} [topological_space α] {G : Type u_4} [topological_space G] [group G] [mul_action G α] [has_continuous_smul G α] [topological_space β] {f : β → α} {b : β} (c : G) :
continuous_at (λ (x : β), c f x) b continuous_at f b
theorem continuous_const_smul_iff {α : Type u_2} {β : Type u_3} [topological_space α] {G : Type u_4} [topological_space G] [group G] [mul_action G α] [has_continuous_smul G α] [topological_space β] {f : β → α} (c : G) :
continuous (λ (x : β), c f x) continuous f
def homeomorph.smul {α : Type u_2} [topological_space α] {G : Type u_4} [topological_space G] [group G] [mul_action G α] [has_continuous_smul 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} [topological_space α] {G : Type u_4} [topological_space G] [group G] [mul_action G α] [has_continuous_smul G α] (c : G) :
is_open_map (λ (x : α), c x)
theorem is_closed_map_smul {α : Type u_2} [topological_space α] {G : Type u_4} [topological_space G] [group G] [mul_action G α] [has_continuous_smul G α] (c : G) :
is_closed_map (λ (x : α), c x)
theorem tendsto_const_smul_iff' {α : Type u_2} {β : Type u_3} [topological_space α] {G₀ : Type u_4} [topological_space G₀] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_smul G₀ α] {f : β → α} {l : filter β} {a : α} {c : G₀} (hc : c 0) :
filter.tendsto (λ (x : β), c f x) l (𝓝 (c a)) filter.tendsto f l (𝓝 a)
theorem continuous_within_at_const_smul_iff' {α : Type u_2} {β : Type u_3} [topological_space α] {G₀ : Type u_4} [topological_space G₀] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_smul G₀ α] [topological_space β] {f : β → α} {b : β} {c : G₀} {s : set β} (hc : c 0) :
continuous_within_at (λ (x : β), c f x) s b continuous_within_at f s b
theorem continuous_on_const_smul_iff' {α : Type u_2} {β : Type u_3} [topological_space α] {G₀ : Type u_4} [topological_space G₀] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_smul G₀ α] [topological_space β] {f : β → α} {c : G₀} {s : set β} (hc : c 0) :
continuous_on (λ (x : β), c f x) s continuous_on f s
theorem continuous_at_const_smul_iff' {α : Type u_2} {β : Type u_3} [topological_space α] {G₀ : Type u_4} [topological_space G₀] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_smul G₀ α] [topological_space β] {f : β → α} {b : β} {c : G₀} (hc : c 0) :
continuous_at (λ (x : β), c f x) b continuous_at f b
theorem continuous_const_smul_iff' {α : Type u_2} {β : Type u_3} [topological_space α] {G₀ : Type u_4} [topological_space G₀] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_smul G₀ α] [topological_space β] {f : β → α} {c : G₀} (hc : c 0) :
continuous (λ (x : β), c f x) continuous f
def homeomorph.smul_of_ne_zero {α : Type u_2} [topological_space α] {G₀ : Type u_4} [topological_space G₀] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_smul 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} [topological_space α] {G₀ : Type u_4} [topological_space G₀] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_smul G₀ α] {c : G₀} (hc : c 0) :
is_open_map (λ (x : α), c x)
theorem is_closed_map_smul' {α : Type u_2} [topological_space α] {G₀ : Type u_4} [topological_space G₀] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_smul 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 is_unit.tendsto_const_smul_iff {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space M] [topological_space α] [monoid M] [mul_action M α] [has_continuous_smul M α] {f : β → α} {l : filter β} {a : α} {c : M} (hc : is_unit c) :
filter.tendsto (λ (x : β), c f x) l (𝓝 (c a)) filter.tendsto f l (𝓝 a)
theorem is_unit.continuous_within_at_const_smul_iff {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space M] [topological_space α] [monoid M] [mul_action M α] [has_continuous_smul M α] [topological_space β] {f : β → α} {b : β} {c : M} {s : set β} (hc : is_unit c) :
continuous_within_at (λ (x : β), c f x) s b continuous_within_at f s b
theorem is_unit.continuous_on_const_smul_iff {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space M] [topological_space α] [monoid M] [mul_action M α] [has_continuous_smul M α] [topological_space β] {f : β → α} {c : M} {s : set β} (hc : is_unit c) :
continuous_on (λ (x : β), c f x) s continuous_on f s
theorem is_unit.continuous_at_const_smul_iff {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space M] [topological_space α] [monoid M] [mul_action M α] [has_continuous_smul M α] [topological_space β] {f : β → α} {b : β} {c : M} (hc : is_unit c) :
continuous_at (λ (x : β), c f x) b continuous_at f b
theorem is_unit.continuous_const_smul_iff {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space M] [topological_space α] [monoid M] [mul_action M α] [has_continuous_smul M α] [topological_space β] {f : β → α} {c : M} (hc : is_unit c) :
continuous (λ (x : β), c f x) continuous f
theorem is_unit.is_open_map_smul {M : Type u_1} {α : Type u_2} [topological_space M] [topological_space α] [monoid M] [mul_action M α] [has_continuous_smul 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} [topological_space M] [topological_space α] [monoid M] [mul_action M α] [has_continuous_smul M α] {c : M} (hc : is_unit c) :
is_closed_map (λ (x : α), c x)
@[instance]
def prod.has_continuous_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space M] [topological_space α] [topological_space β] [has_scalar M α] [has_scalar M β] [has_continuous_smul M α] [has_continuous_smul M β] :
@[instance]
def pi.has_continuous_smul {M : Type u_1} [topological_space M] {ι : Type u_2} {γ : ι → Type} [Π (i : ι), topological_space (γ i)] [Π (i : ι), has_scalar M (γ i)] [∀ (i : ι), has_continuous_smul M (γ i)] :
has_continuous_smul M (Π (i : ι), γ i)