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 #

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

source

@[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

source

@[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

source

@[class]

structure properly_discontinuous_smul (Γ : Type u_1) (T : Type u_2) [topological_space T] [has_scalar Γ T] :

Prop

finite_disjoint_inter_image : ∀ {K L : set T}, is_compact K → is_compact L → {γ : Γ | has_scalar.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

fintype.properly_discontinuous_smul

source

@[class]

structure properly_discontinuous_vadd (Γ : Type u_1) (T : Type u_2) [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

fintype.properly_discontinuous_vadd

source

@[protected, instance]

def fintype.properly_discontinuous_vadd {Γ : Type u_1} [add_group Γ] {T : Type u_2} [topological_space T] [add_action Γ T] [fintype Γ] :

properly_discontinuous_vadd Γ T

source

@[protected, instance]

def fintype.properly_discontinuous_smul {Γ : Type u_1} [group Γ] {T : Type u_2} [topological_space T] [mul_action Γ T] [fintype Γ] :

properly_discontinuous_smul Γ T

A finite group action is always properly discontinuous

source

def homeomorph.smul {T : Type u_1} [topological_space T] {Γ : Type u_2} [group Γ] [mul_action Γ T] [has_continuous_const_smul Γ T] (γ : Γ) :

T ≃ₜ T

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_hom Γ T) γ, continuous_to_fun := _, continuous_inv_fun := _}

source

def homeomorph.vadd {T : Type u_1} [topological_space T] {Γ : Type u_2} [add_group Γ] [add_action Γ T] [has_continuous_const_vadd Γ T] (γ : Γ) :

T ≃ₜ T

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_hom T Γ) γ, continuous_to_fun := _, continuous_inv_fun := _}

source

theorem is_open_map_quotient_mk_add {Γ : Type u_1} [add_group Γ] {T : Type u_2} [topological_space T] [add_action Γ T] [has_continuous_const_vadd Γ T] :

is_open_map quotient.mk

source

theorem is_open_map_quotient_mk_mul {Γ : Type u_1} [group Γ] {T : Type u_2} [topological_space T] [mul_action Γ T] [has_continuous_const_smul Γ T] :

is_open_map quotient.mk

The quotient map by a group action is open.

source

@[protected, instance]

def t2_space_of_properly_discontinuous_smul_of_t2_space {Γ : Type u_1} [group Γ] {T : Type u_2} [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.

source

@[protected, instance]

def t2_space_of_properly_discontinuous_vadd_of_t2_space {Γ : Type u_1} [add_group Γ] {T : Type u_2} [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))