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 mapx ↦ γ • xis continuous onT;properly_discontinuous_smul: says that the scalar multiplication(•) : Γ → T → Tis properly discontinuous, that is, for any pair of compact setsK, LinT, only finitely manyγ:ΓmoveKto have nontrivial intersection withL.homeomorph.smul: scalar multiplication by an element of a groupΓacting onTis a homeomorphism ofT.
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)
[topological_space T]
[has_smul Γ 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.
Note that both has_continuous_const_smul α α and has_continuous_const_smul αᵐᵒᵖ α are
weaker versions of has_continuous_mul α.
Instances of this typeclass
- has_continuous_smul.has_continuous_const_smul
- is_scalar_tower.has_continuous_const_smul
- smul_comm_class.has_continuous_const_smul
- has_uniform_continuous_const_smul.to_has_continuous_const_smul
- has_isometric_smul.to_has_continuous_const_smul
- has_continuous_const_smul.op
- mul_opposite.has_continuous_const_smul
- order_dual.has_continuous_const_smul
- order_dual.has_continuous_const_smul'
- prod.has_continuous_const_smul
- pi.has_continuous_const_smul
- units.has_continuous_const_smul
- add_monoid.has_continuous_const_smul_nat
- conj_act.units_has_continuous_const_smul
- add_group.has_continuous_const_smul_int
- quotient_group.has_continuous_const_smul
- continuous_linear_map.has_continuous_const_smul
- division_ring.has_continuous_const_smul_rat
- continuous_multilinear_map.has_continuous_const_smul
@[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.
Note that both has_continuous_const_vadd α α and has_continuous_const_vadd αᵐᵒᵖ α are
weaker versions of has_continuous_add α.
Instances of this typeclass
- has_continuous_vadd.has_continuous_const_vadd
- vadd_assoc_class.has_continuous_const_vadd
- vadd_comm_class.has_continuous_const_vadd
- has_uniform_continuous_const_vadd.to_has_continuous_const_vadd
- has_isometric_vadd.to_has_continuous_const_vadd
- has_continuous_const_vadd.op
- add_opposite.has_continuous_const_vadd
- order_dual.has_continuous_const_vadd
- order_dual.has_continuous_const_vadd'
- prod.has_continuous_const_vadd
- pi.has_continuous_const_vadd
- add_units.has_continuous_const_vadd
- quotient_add_group.has_continuous_const_vadd
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]
def
has_continuous_const_smul.op
{M : Type u_1}
{α : Type u_2}
[topological_space α]
[has_smul M α]
[has_continuous_const_smul M α]
[has_smul Mᵐᵒᵖ α]
[is_central_scalar M α] :
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}
[topological_space α]
[has_vadd M α]
[has_continuous_const_vadd M α]
[has_vadd Mᵃᵒᵖ α]
[is_central_vadd M α] :
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}
[topological_space α]
[has_vadd M α]
[has_continuous_const_vadd M α] :
@[protected, instance]
def
mul_opposite.has_continuous_const_smul
{M : Type u_1}
{α : Type u_2}
[topological_space α]
[has_smul M α]
[has_continuous_const_smul M α] :
@[protected, instance]
def
order_dual.has_continuous_const_vadd
{M : Type u_1}
{α : Type u_2}
[topological_space α]
[has_vadd M α]
[has_continuous_const_vadd M α] :
@[protected, instance]
def
order_dual.has_continuous_const_smul
{M : Type u_1}
{α : Type u_2}
[topological_space α]
[has_smul M α]
[has_continuous_const_smul M α] :
@[protected, instance]
def
order_dual.has_continuous_const_smul'
{M : Type u_1}
{α : Type u_2}
[topological_space α]
[has_smul M α]
[has_continuous_const_smul M α] :
@[protected, instance]
def
order_dual.has_continuous_const_vadd'
{M : Type u_1}
{α : Type u_2}
[topological_space α]
[has_vadd M α]
[has_continuous_const_vadd M α] :
@[protected, instance]
def
prod.has_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 β]
[has_smul M β]
[has_continuous_const_smul 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 β] :
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_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) :
is_compact (a • 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) :
is_compact (a +ᵥ s)
@[protected, instance]
def
add_units.has_continuous_const_vadd
{M : Type u_1}
{α : Type u_2}
[topological_space α]
[add_monoid M]
[add_action M α]
[has_continuous_const_vadd M α] :
@[protected, instance]
def
units.has_continuous_const_smul
{M : Type u_1}
{α : Type u_2}
[topological_space α]
[monoid M]
[mul_action M α]
[has_continuous_const_smul M α] :
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 : α) :
c • closure (mul_action.orbit M x) ⊆ closure (mul_action.orbit 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 : α) :
c +ᵥ closure (add_action.orbit M x) ⊆ closure (add_action.orbit 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
- homeomorph.vadd γ = {to_equiv := add_action.to_perm γ, continuous_to_fun := _, continuous_inv_fun := _}
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
- homeomorph.smul γ = {to_equiv := mul_action.to_perm γ, continuous_to_fun := _, continuous_inv_fun := _}
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) :
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 α) :
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) :
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) :
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
- homeomorph.smul_of_ne_zero c hc = homeomorph.smul (units.mk0 c hc)
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) :
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) :
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
- finite_disjoint_inter_image : ∀ {K L : set T}, is_compact K → is_compact L → {γ : Γ | has_smul.smul γ '' K ∩ L ≠ ∅}.finite
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
- finite_disjoint_inter_image : ∀ {K L : set T}, is_compact K → is_compact L → {γ : Γ | has_vadd.vadd γ '' K ∩ L ≠ ∅}.finite
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}
[topological_space T]
[add_action Γ 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}
[topological_space T]
[mul_action Γ 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}
[topological_space T]
[add_action Γ T]
[has_continuous_const_vadd Γ 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}
[topological_space T]
[mul_action Γ T]
[has_continuous_const_smul Γ T] :
The quotient map by a group action is open, i.e. the quotient by a group action is an open quotient.
@[protected, instance]
def
t2_space_of_properly_discontinuous_smul_of_t2_space
{Γ : Type u_4}
[group Γ]
{T : Type u_5}
[topological_space T]
[mul_action Γ T]
[t2_space T]
[locally_compact_space T]
[has_continuous_const_smul Γ T]
[properly_discontinuous_smul Γ T] :
t2_space (quotient (mul_action.orbit_rel Γ T))
The quotient by a discontinuous group action of a locally compact t2 space is t2.
@[protected, instance]
def
t2_space_of_properly_discontinuous_vadd_of_t2_space
{Γ : Type u_4}
[add_group Γ]
{T : Type u_5}
[topological_space T]
[add_action Γ T]
[t2_space T]
[locally_compact_space T]
[has_continuous_const_vadd Γ T]
[properly_discontinuous_vadd Γ T] :
t2_space (quotient (add_action.orbit_rel Γ T))
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}
[topological_space T]
[add_action Γ T]
[topological_space.second_countable_topology T]
[has_continuous_const_vadd Γ 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}
[topological_space T]
[mul_action Γ T]
[topological_space.second_countable_topology T]
[has_continuous_const_smul Γ 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₀]
[mul_action G₀ α]
[topological_space α]
[has_continuous_const_smul G₀ α]
{c : G₀}
{s : set α}
{x : α}
(hs : s ∈ nhds x)
(hc : c ≠ 0) :
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) :
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) :