mathlib3 documentation

topology.algebra.const_mul_action

Monoid actions continuous in the second variable #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_smul Γ T] :
Prop

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.

Note that both has_continuous_const_smul α α and has_continuous_const_smul αᵐᵒᵖ α are weaker versions of has_continuous_mul α.

Instances of this typeclass
theorem filter.tendsto.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [has_smul M α] [has_continuous_const_smul M α] {f : β α} {l : filter β} {a : α} (hf : filter.tendsto f l (nhds a)) (c : M) :
filter.tendsto (λ (x : β), c f x) l (nhds (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 (nhds a)) (c : M) :
filter.tendsto (λ (x : β), c +ᵥ f x) l (nhds (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_smul 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_smul 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_smul 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_smul 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]

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

@[protected, instance]
@[protected, instance]
@[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_smul M (γ i)] [ (i : ι), has_continuous_const_smul M (γ i)] :
has_continuous_const_smul M (Π (i : ι), γ i)
theorem is_compact.smul {α : Type u_1} {β : Type u_2} [has_smul α β] [topological_space β] [has_continuous_const_smul α β] (a : α) {s : set β} (hs : is_compact s) :
theorem is_compact.vadd {α : Type u_1} {β : Type u_2} [has_vadd α β] [topological_space β] [has_continuous_const_vadd α β] (a : α) {s : set β} (hs : is_compact s) :
@[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 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 (nhds (c a)) filter.tendsto f l (nhds 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 (nhds (c +ᵥ a)) filter.tendsto f l (nhds 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 dense.smul {α : Type u_2} {G : Type u_4} [topological_space α] [group G] [mul_action G α] [has_continuous_const_smul G α] (c : G) {s : set α} (hs : dense s) :
dense (c s)
theorem dense.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 α} (hs : dense s) :
dense (c +ᵥ 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 (nhds (c a)) filter.tendsto f l (nhds 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 has_compact_mul_support.comp_smul {α : Type u_2} {G₀ : Type u_4} [topological_space α] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_const_smul G₀ α] {β : Type u_1} [has_one β] {f : α β} (h : has_compact_mul_support f) {c : G₀} (hc : c 0) :
has_compact_mul_support (λ (x : α), f (c x))
theorem has_compact_support.comp_smul {α : Type u_2} {G₀ : Type u_4} [topological_space α] [group_with_zero G₀] [mul_action G₀ α] [has_continuous_const_smul G₀ α] {β : Type u_1} [has_zero β] {f : α β} (h : has_compact_support f) {c : G₀} (hc : c 0) :
has_compact_support (λ (x : α), f (c x))
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 (nhds (c a)) filter.tendsto f l (nhds 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_smul Γ 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 of this typeclass
@[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 of this typeclass
@[protected, instance]

A finite group action is always properly discontinuous.

@[protected, instance]

A finite group action is always properly discontinuous.

The quotient map by a group action is open, i.e. the quotient by a group action is an open quotient.

The quotient map by a group action is open, i.e. the quotient by a group action is an open quotient.

@[protected, instance]

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

@[protected, instance]

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

The quotient of a second countable space by an additive group action is second countable.

The quotient of a second countable space by a group action is second countable.

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 nhds x) (hc : c 0) :
c s nhds (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 nhds (c x) s nhds 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 nhds 0 s nhds 0