mathlib documentation

topology.algebra.const_mul_action

Monoid actions continuous in the second variable #

In this file we define class has_continuous_const_smul. We say has_continuous_const_smul Γ T if Γ acts on T and for each γ, the map x ↦ γ • x is continuous. (This differs from has_continuous_smul, which requires simultaneous continuity in both variables.)

Main definitions #

Main results #

Tags #

Hausdorff, discrete group, properly discontinuous, quotient space

@[class]
structure has_continuous_const_smul (Γ : Type u_1) (T : Type u_2) [topological_space T] [has_scalar Γ T] :
Prop
  • continuous_const_smul : ∀ (γ : Γ), continuous (λ (x : T), γ x)

Class has_continuous_const_smul Γ T says that the scalar multiplication (•) : Γ → T → T is continuous in the second argument. We use the same class for all kinds of multiplicative actions, including (semi)modules and algebras.

Instances
@[class]
structure has_continuous_const_vadd (Γ : Type u_1) (T : Type u_2) [topological_space T] [has_vadd Γ T] :
Prop
  • continuous_const_vadd : ∀ (γ : Γ), continuous (λ (x : T), γ +ᵥ x)

Class has_continuous_const_vadd Γ T says that the additive action (+ᵥ) : Γ → T → T is continuous in the second argument. We use the same class for all kinds of additive actions, including (semi)modules and algebras.

Instances
theorem filter.tendsto.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [has_scalar M α] [has_continuous_const_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.const_vadd {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [has_vadd M α] [has_continuous_const_vadd M α] {f : β → α} {l : filter β} {a : α} (hf : filter.tendsto f l (𝓝 a)) (c : M) :
filter.tendsto (λ (x : β), c +ᵥ f x) l (𝓝 (c +ᵥ a))
theorem continuous_within_at.const_vadd {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [has_vadd M α] [has_continuous_const_vadd 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_within_at.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [has_scalar M α] [has_continuous_const_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.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [has_scalar M α] [has_continuous_const_smul M α] [topological_space β] {g : β → α} {b : β} (hg : continuous_at g b) (c : M) :
continuous_at (λ (x : β), c g x) b
theorem continuous_at.const_vadd {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [has_vadd M α] [has_continuous_const_vadd M α] [topological_space β] {g : β → α} {b : β} (hg : continuous_at g b) (c : M) :
continuous_at (λ (x : β), c +ᵥ g x) b
theorem continuous_on.const_vadd {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [has_vadd M α] [has_continuous_const_vadd M α] [topological_space β] {g : β → α} {s : set β} (hg : continuous_on g s) (c : M) :
continuous_on (λ (x : β), c +ᵥ g x) s
theorem continuous_on.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [has_scalar M α] [has_continuous_const_smul M α] [topological_space β] {g : β → α} {s : set β} (hg : continuous_on g s) (c : M) :
continuous_on (λ (x : β), c g x) s
@[continuity]
theorem continuous.const_vadd {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [has_vadd M α] [has_continuous_const_vadd M α] [topological_space β] {g : β → α} (hg : continuous g) (c : M) :
continuous (λ (x : β), c +ᵥ g x)
@[continuity]
theorem continuous.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [has_scalar M α] [has_continuous_const_smul M α] [topological_space β] {g : β → α} (hg : continuous g) (c : M) :
continuous (λ (x : β), c g x)
@[protected, instance]

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

@[protected, instance]
def prod.has_continuous_const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [has_scalar M α] [has_continuous_const_smul M α] [topological_space β] [has_scalar M β] [has_continuous_const_smul M β] :
@[protected, instance]
def prod.has_continuous_const_vadd {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [has_vadd M α] [has_continuous_const_vadd M α] [topological_space β] [has_vadd M β] [has_continuous_const_vadd M β] :
@[protected, instance]
def pi.has_continuous_const_vadd {M : Type u_1} {ι : Type u_2} {γ : ι → Type u_3} [Π (i : ι), topological_space (γ i)] [Π (i : ι), has_vadd M (γ i)] [∀ (i : ι), has_continuous_const_vadd M (γ i)] :
has_continuous_const_vadd M (Π (i : ι), γ i)
@[protected, instance]
def pi.has_continuous_const_smul {M : Type u_1} {ι : Type u_2} {γ : ι → Type u_3} [Π (i : ι), topological_space (γ i)] [Π (i : ι), has_scalar M (γ i)] [∀ (i : ι), has_continuous_const_smul M (γ i)] :
has_continuous_const_smul M (Π (i : ι), γ i)
@[protected, instance]
@[protected, instance]
theorem smul_closure_subset {M : Type u_1} {α : Type u_2} [topological_space α] [monoid M] [mul_action M α] [has_continuous_const_smul M α] (c : M) (s : set α) :
theorem vadd_closure_subset {M : Type u_1} {α : Type u_2} [topological_space α] [add_monoid M] [add_action M α] [has_continuous_const_vadd M α] (c : M) (s : set α) :
theorem smul_closure_orbit_subset {M : Type u_1} {α : Type u_2} [topological_space α] [monoid M] [mul_action M α] [has_continuous_const_smul M α] (c : M) (x : α) :
theorem vadd_closure_orbit_subset {M : Type u_1} {α : Type u_2} [topological_space α] [add_monoid M] [add_action M α] [has_continuous_const_vadd M α] (c : M) (x : α) :
theorem tendsto_const_smul_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [topological_space α] [group G] [mul_action G α] [has_continuous_const_smul G α] {f : β → α} {l : filter β} {a : α} (c : G) :
filter.tendsto (λ (x : β), c f x) l (𝓝 (c a)) filter.tendsto f l (𝓝 a)
theorem tendsto_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [topological_space α] [add_group G] [add_action G α] [has_continuous_const_vadd 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} {G : Type u_4} [topological_space α] [group G] [mul_action G α] [has_continuous_const_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_within_at_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [topological_space α] [add_group G] [add_action G α] [has_continuous_const_vadd 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_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [topological_space α] [add_group G] [add_action G α] [has_continuous_const_vadd G α] [topological_space β] {f : β → α} {s : set β} (c : G) :
continuous_on (λ (x : β), c +ᵥ f x) s continuous_on f s
theorem continuous_on_const_smul_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [topological_space α] [group G] [mul_action G α] [has_continuous_const_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} {G : Type u_4} [topological_space α] [group G] [mul_action G α] [has_continuous_const_smul G α] [topological_space β] {f : β → α} {b : β} (c : G) :
continuous_at (λ (x : β), c f x) b continuous_at f b
theorem continuous_at_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [topological_space α] [add_group G] [add_action G α] [has_continuous_const_vadd 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} {G : Type u_4} [topological_space α] [group G] [mul_action G α] [has_continuous_const_smul G α] [topological_space β] {f : β → α} (c : G) :
continuous (λ (x : β), c f x) continuous f
theorem continuous_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [topological_space α] [add_group G] [add_action G α] [has_continuous_const_vadd G α] [topological_space β] {f : β → α} (c : G) :
continuous (λ (x : β), c +ᵥ f x) continuous f
def homeomorph.vadd {α : Type u_2} {G : Type u_4} [topological_space α] [add_group G] [add_action G α] [has_continuous_const_vadd G α] (γ : G) :
α ≃ₜ α

The homeomorphism given by affine-addition by an element of an additive group Γ acting on T is a homeomorphism from T to itself.

Equations
def homeomorph.smul {α : Type u_2} {G : Type u_4} [topological_space α] [group G] [mul_action G α] [has_continuous_const_smul G α] (γ : G) :
α ≃ₜ α

The homeomorphism given by scalar multiplication by a given element of a group Γ acting on T is a homeomorphism from T to itself.

Equations
theorem is_open_map_smul {α : Type u_2} {G : Type u_4} [topological_space α] [group G] [mul_action G α] [has_continuous_const_smul G α] (c : G) :
is_open_map (λ (x : α), c x)
theorem is_open_map_vadd {α : Type u_2} {G : Type u_4} [topological_space α] [add_group G] [add_action G α] [has_continuous_const_vadd G α] (c : G) :
is_open_map (λ (x : α), c +ᵥ x)
theorem is_open.vadd {α : Type u_2} {G : Type u_4} [topological_space α] [add_group G] [add_action G α] [has_continuous_const_vadd G α] {s : set α} (hs : is_open s) (c : G) :
theorem is_open.smul {α : Type u_2} {G : Type u_4} [topological_space α] [group G] [mul_action G α] [has_continuous_const_smul G α] {s : set α} (hs : is_open s) (c : G) :
is_open (c s)
theorem is_closed_map_vadd {α : Type u_2} {G : Type u_4} [topological_space α] [add_group G] [add_action G α] [has_continuous_const_vadd G α] (c : G) :
is_closed_map (λ (x : α), c +ᵥ x)
theorem is_closed_map_smul {α : Type u_2} {G : Type u_4} [topological_space α] [group G] [mul_action G α] [has_continuous_const_smul G α] (c : G) :
is_closed_map (λ (x : α), c x)
theorem is_closed.vadd {α : Type u_2} {G : Type u_4} [topological_space α] [add_group G] [add_action G α] [has_continuous_const_vadd G α] {s : set α} (hs : is_closed s) (c : G) :
theorem is_closed.smul {α : Type u_2} {G : Type u_4} [topological_space α] [group G] [mul_action G α] [has_continuous_const_smul G α] {s : set α} (hs : is_closed s) (c : G) :
theorem closure_vadd {α : Type u_2} {G : Type u_4} [topological_space α] [add_group G] [add_action G α] [has_continuous_const_vadd G α] (c : G) (s : set α) :
theorem closure_smul {α : Type u_2} {G : Type u_4} [topological_space α] [group G] [mul_action G α] [has_continuous_const_smul G α] (c : G) (s : set α) :
closure (c s) = c closure s
theorem interior_vadd {α : Type u_2} {G : Type u_4} [topological_space α] [add_group G] [add_action G α] [has_continuous_const_vadd G α] (c : G) (s : set α) :
theorem interior_smul {α : Type u_2} {G : Type u_4} [topological_space α] [group G] [mul_action G α] [has_continuous_const_smul G α] (c : G) (s : set α) :
theorem tendsto_const_smul_iff₀ {α : Type u_2} {β : Type u_3} {G₀ : Type u_4} [topological_space α] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_const_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} {G₀ : Type u_4} [topological_space α] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_const_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} {G₀ : Type u_4} [topological_space α] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_const_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} {G₀ : Type u_4} [topological_space α] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_const_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} {G₀ : Type u_4} [topological_space α] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_const_smul G₀ α] [topological_space β] {f : β → α} {c : G₀} (hc : c 0) :
continuous (λ (x : β), c f x) continuous f
@[protected]
def homeomorph.smul_of_ne_zero {α : Type u_2} {G₀ : Type u_4} [topological_space α] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_const_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} {G₀ : Type u_4} [topological_space α] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_const_smul G₀ α] {c : G₀} (hc : c 0) :
is_open_map (λ (x : α), c x)
theorem is_open.smul₀ {α : Type u_2} {G₀ : Type u_4} [topological_space α] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_const_smul G₀ α] {c : G₀} {s : set α} (hs : is_open s) (hc : c 0) :
is_open (c s)
theorem interior_smul₀ {α : Type u_2} {G₀ : Type u_4} [topological_space α] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_const_smul G₀ α] {c : G₀} (hc : c 0) (s : set α) :
theorem closure_smul₀ {G₀ : Type u_4} [group_with_zero G₀] {E : Type u_1} [has_zero E] [mul_action_with_zero G₀ E] [topological_space E] [t1_space E] [has_continuous_const_smul G₀ E] (c : G₀) (s : set E) :
closure (c s) = c closure s
theorem is_closed_map_smul_of_ne_zero {α : Type u_2} {G₀ : Type u_4} [topological_space α] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_const_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_closed.smul_of_ne_zero {α : Type u_2} {G₀ : Type u_4} [topological_space α] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_const_smul G₀ α] {c : G₀} {s : set α} (hs : is_closed s) (hc : c 0) :
theorem is_closed_map_smul₀ {𝕜 : Type u_1} {M : Type u_2} [division_ring 𝕜] [add_comm_monoid M] [topological_space M] [t1_space M] [module 𝕜 M] [has_continuous_const_smul 𝕜 M] (c : 𝕜) :
is_closed_map (λ (x : M), 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_closed.smul₀ {𝕜 : Type u_1} {M : Type u_2} [division_ring 𝕜] [add_comm_monoid M] [topological_space M] [t1_space M] [module 𝕜 M] [has_continuous_const_smul 𝕜 M] (c : 𝕜) {s : set M} (hs : is_closed s) :
theorem is_unit.tendsto_const_smul_iff {M : Type u_1} {α : Type u_2} {β : Type u_3} [monoid M] [topological_space α] [mul_action M α] [has_continuous_const_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} [monoid M] [topological_space α] [mul_action M α] [has_continuous_const_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} [monoid M] [topological_space α] [mul_action M α] [has_continuous_const_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} [monoid M] [topological_space α] [mul_action M α] [has_continuous_const_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} [monoid M] [topological_space α] [mul_action M α] [has_continuous_const_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} [monoid M] [topological_space α] [mul_action M α] [has_continuous_const_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} [monoid M] [topological_space α] [mul_action M α] [has_continuous_const_smul M α] {c : M} (hc : is_unit c) :
is_closed_map (λ (x : α), c x)
@[class]
structure properly_discontinuous_smul (Γ : Type u_4) (T : Type u_5) [topological_space T] [has_scalar Γ T] :
Prop

Class properly_discontinuous_smul Γ T says that the scalar multiplication (•) : Γ → T → T is properly discontinuous, that is, for any pair of compact sets K, L in T, only finitely many γ:Γ move K to have nontrivial intersection with L.

Instances
@[class]
structure properly_discontinuous_vadd (Γ : Type u_4) (T : Type u_5) [topological_space T] [has_vadd Γ T] :
Prop

Class properly_discontinuous_vadd Γ T says that the additive action (+ᵥ) : Γ → T → T is properly discontinuous, that is, for any pair of compact sets K, L in T, only finitely many γ:Γ move K to have nontrivial intersection with L.

Instances
@[protected, instance]
def fintype.properly_discontinuous_vadd {Γ : Type u_4} [add_group Γ] {T : Type u_5} [topological_space T] [add_action Γ T] [fintype Γ] :
@[protected, instance]
def fintype.properly_discontinuous_smul {Γ : Type u_4} [group Γ] {T : Type u_5} [topological_space T] [mul_action Γ T] [fintype Γ] :

A finite group action is always properly discontinuous

theorem is_open_map_quotient_mk_mul {Γ : Type u_4} [group Γ] {T : Type u_5} [topological_space T] [mul_action Γ T] [has_continuous_const_smul Γ T] :

The quotient map by a group action is open.

@[protected, instance]

The quotient by a discontinuous group action of a locally compact t2 space is t2.

theorem set_smul_mem_nhds_smul {α : Type u_2} {G₀ : Type u_6} [group_with_zero G₀] [mul_action G₀ α] [topological_space α] [has_continuous_const_smul G₀ α] {c : G₀} {s : set α} {x : α} (hs : s 𝓝 x) (hc : c 0) :
c s 𝓝 (c x)

Scalar multiplication preserves neighborhoods.

theorem set_smul_mem_nhds_smul_iff {α : Type u_2} {G₀ : Type u_6} [group_with_zero G₀] [mul_action G₀ α] [topological_space α] [has_continuous_const_smul G₀ α] {c : G₀} {s : set α} {x : α} (hc : c 0) :
c s 𝓝 (c x) s 𝓝 x
theorem set_smul_mem_nhds_zero_iff {α : Type u_2} {G₀ : Type u_6} [group_with_zero G₀] [add_monoid α] [distrib_mul_action G₀ α] [topological_space α] [has_continuous_const_smul G₀ α] {s : set α} {c : G₀} (hc : c 0) :
c s 𝓝 0 s 𝓝 0