# mathlib3documentation

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 #

• has_continuous_const_smul Γ T : typeclass saying that the map x ↦ γ • x is continuous on T;
• properly_discontinuous_smul: 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.
• homeomorph.smul: scalar multiplication by an element of a group Γ acting on T is a homeomorphism of T.

## Main results #

• is_open_map_quotient_mk_mul : The quotient map by a group action is open.
• t2_space_of_properly_discontinuous_smul_of_t2_space : The quotient by a discontinuous group action of a locally compact t2 space is t2.

## Tags #

Hausdorff, discrete group, properly discontinuous, quotient space

@[class]
structure has_continuous_const_smul (Γ : Type u_1) (T : Type u_2) [ 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
@[class]
structure has_continuous_const_vadd (Γ : Type u_1) (T : Type u_2) [ T] :
Prop

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.

Note that both has_continuous_const_vadd α α and has_continuous_const_vadd αᵐᵒᵖ α are weaker versions of has_continuous_add α.

Instances of this typeclass
theorem filter.tendsto.const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [ α] {f : β α} {l : filter β} {a : α} (hf : (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} [ α] {f : β α} {l : filter β} {a : α} (hf : (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} [ α] {g : β α} {b : β} {s : set β} (hg : 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} [ α] {g : β α} {b : β} {s : set β} (hg : 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} [ α] {g : β α} {b : β} (hg : 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} [ α] {g : β α} {b : β} (hg : 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} [ α] {g : β α} {s : set β} (hg : 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} [ α] {g : β α} {s : set β} (hg : 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} [ α] {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} [ α] {g : β α} (hg : continuous g) (c : M) :
continuous (λ (x : β), c g x)
@[protected, instance]
def has_continuous_const_smul.op {M : Type u_1} {α : Type u_2} [ α] [ α] [ α] :

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

@[protected, instance]
def has_continuous_const_vadd.op {M : Type u_1} {α : Type u_2} [ α] [ α] [ α] :

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

@[protected, instance]
def add_opposite.has_continuous_const_vadd {M : Type u_1} {α : Type u_2} [ α]  :
@[protected, instance]
def mul_opposite.has_continuous_const_smul {M : Type u_1} {α : Type u_2} [ α]  :
@[protected, instance]
def order_dual.has_continuous_const_vadd {M : Type u_1} {α : Type u_2} [ α]  :
@[protected, instance]
def order_dual.has_continuous_const_smul {M : Type u_1} {α : Type u_2} [ α]  :
@[protected, instance]
def order_dual.has_continuous_const_smul' {M : Type u_1} {α : Type u_2} [ α]  :
@[protected, instance]
def order_dual.has_continuous_const_vadd' {M : Type u_1} {α : Type u_2} [ α]  :
@[protected, instance]
def prod.has_continuous_const_smul {M : Type u_1} {α : Type u_2} {β : Type u_3} [ α] [ β]  :
× β)
@[protected, instance]
def prod.has_continuous_const_vadd {M : Type u_1} {α : Type u_2} {β : Type u_3} [ α] [ β]  :
× β)
@[protected, instance]
def pi.has_continuous_const_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_const_smul {M : Type u_1} {ι : Type u_2} {γ : ι Type u_3} [Π (i : ι), topological_space (γ i)] [Π (i : ι), (γ i)] [ (i : ι), (γ i)] :
(Π (i : ι), γ i)
theorem is_compact.smul {α : Type u_1} {β : Type u_2} [ β] (a : α) {s : set β} (hs : is_compact s) :
theorem is_compact.vadd {α : Type u_1} {β : Type u_2} [ β] (a : α) {s : set β} (hs : is_compact s) :
@[protected, instance]
@[protected, instance]
def units.has_continuous_const_smul {M : Type u_1} {α : Type u_2} [monoid M] [ α]  :
theorem smul_closure_subset {M : Type u_1} {α : Type u_2} [monoid M] [ α] (c : M) (s : set α) :
c closure (c s)
theorem vadd_closure_subset {M : Type u_1} {α : Type u_2} [add_monoid M] [ α] (c : M) (s : set α) :
theorem smul_closure_orbit_subset {M : Type u_1} {α : Type u_2} [monoid M] [ α] (c : M) (x : α) :
theorem vadd_closure_orbit_subset {M : Type u_1} {α : Type u_2} [add_monoid M] [ α] (c : M) (x : α) :
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 (nhds (c a)) (nhds a)
theorem tendsto_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [add_group G] [ α] {f : β α} {l : filter β} {a : α} (c : G) :
filter.tendsto (λ (x : β), c +ᵥ f x) l (nhds (c +ᵥ a)) (nhds 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_within_at_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [add_group G] [ α] {f : β α} {b : β} {s : set β} (c : G) :
continuous_within_at (λ (x : β), c +ᵥ f x) s b b
theorem continuous_on_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [add_group G] [ α] {f : β α} {s : set β} (c : G) :
continuous_on (λ (x : β), c +ᵥ f x) s
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_at_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [add_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)
theorem continuous_const_vadd_iff {α : Type u_2} {β : Type u_3} {G : Type u_4} [add_group G] [ α] {f : β α} (c : G) :
continuous (λ (x : β), c +ᵥ f x)
def homeomorph.vadd {α : Type u_2} {G : Type u_4} [add_group 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} [group 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} [group G] [ α] (c : G) :
is_open_map (λ (x : α), c x)
theorem is_open_map_vadd {α : Type u_2} {G : Type u_4} [add_group G] [ α] (c : G) :
is_open_map (λ (x : α), c +ᵥ x)
theorem is_open.vadd {α : Type u_2} {G : Type u_4} [add_group G] [ α] {s : set α} (hs : is_open s) (c : G) :
theorem is_open.smul {α : Type u_2} {G : Type u_4} [group 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} [add_group G] [ α] (c : G) :
is_closed_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)
theorem is_closed.vadd {α : Type u_2} {G : Type u_4} [add_group G] [ α] {s : set α} (hs : is_closed s) (c : G) :
theorem is_closed.smul {α : Type u_2} {G : Type u_4} [group G] [ α] {s : set α} (hs : is_closed s) (c : G) :
theorem closure_vadd {α : Type u_2} {G : Type u_4} [add_group G] [ α] (c : G) (s : set α) :
closure (c +ᵥ s) = c +ᵥ
theorem closure_smul {α : Type u_2} {G : Type u_4} [group G] [ α] (c : G) (s : set α) :
closure (c s) = c
theorem dense.smul {α : Type u_2} {G : Type u_4} [group G] [ α] (c : G) {s : set α} (hs : dense s) :
dense (c s)
theorem dense.vadd {α : Type u_2} {G : Type u_4} [add_group G] [ α] (c : G) {s : set α} (hs : dense s) :
dense (c +ᵥ s)
theorem interior_vadd {α : Type u_2} {G : Type u_4} [add_group G] [ α] (c : G) (s : set α) :
interior (c +ᵥ s) = c +ᵥ
theorem interior_smul {α : Type u_2} {G : Type u_4} [group G] [ α] (c : G) (s : set α) :
interior (c s) = c
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 (nhds (c a)) (nhds 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)
@[protected]
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_open.smul₀ {α : Type u_2} {G₀ : Type u_4} [group_with_zero 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} [group_with_zero G₀] [ α] {c : G₀} (hc : c 0) (s : set α) :
interior (c s) = c
theorem closure_smul₀ {G₀ : Type u_4} [group_with_zero G₀] {E : Type u_1} [has_zero E] [ E] [t1_space E] (c : G₀) (s : set E) :
closure (c s) = c
theorem is_closed_map_smul_of_ne_zero {α : 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 is_closed.smul_of_ne_zero {α : Type u_2} {G₀ : Type u_4} [group_with_zero G₀] [ α] {c : G₀} {s : set α} (hs : is_closed s) (hc : c 0) :
theorem is_closed_map_smul₀ {𝕜 : Type u_1} {M : Type u_2} [t1_space M] [ 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} [t1_space M] [ M] (c : 𝕜) {s : set M} (hs : is_closed s) :
theorem has_compact_mul_support.comp_smul {α : Type u_2} {G₀ : Type u_4} [group_with_zero 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} [group_with_zero 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] [ α] {f : β α} {l : filter β} {a : α} {c : M} (hc : is_unit c) :
filter.tendsto (λ (x : β), c f x) l (nhds (c a)) (nhds 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)
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)
@[class]
structure properly_discontinuous_smul (Γ : Type u_4) (T : Type u_5) [ 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) [ 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]
def finite.to_properly_discontinuous_vadd {Γ : Type u_4} [add_group Γ] {T : Type u_5} [ T] [finite Γ] :

A finite group action is always properly discontinuous.

@[protected, instance]
def finite.to_properly_discontinuous_smul {Γ : Type u_4} [group Γ] {T : Type u_5} [ T] [finite Γ] :

A finite group action is always properly discontinuous.

theorem is_open_map_quotient_mk_add {Γ : Type u_4} [add_group Γ] {T : Type u_5} [ T]  :

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

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

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.

theorem has_continuous_const_vadd.second_countable_topology {Γ : Type u_4} [add_group Γ] {T : Type u_5} [ T]  :

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

theorem has_continuous_const_smul.second_countable_topology {Γ : Type u_4} [group Γ] {T : Type u_5} [ T]  :

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₀] [ α] {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₀] [ α] {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 α] [ α] {s : set α} {c : G₀} (hc : c 0) :
c s nhds 0 s nhds 0