mathlib documentation

topology.algebra.uniform_mul_action

Multiplicative action on the completion of a uniform space #

In this file we define typeclasses has_uniform_continuous_const_vadd and has_uniform_continuous_const_smul and prove that a multiplicative action on X with uniformly continuous (•) c can be extended to a multiplicative action on uniform_space.completion X.

In later files once the additive group structure is set up, we provide

TODO: Generalise the results here from the concrete completion to any abstract_completion.

source
@[class]
structure has_uniform_continuous_const_vadd (M : Type v) (X : Type x) [_inst_1 _inst_3 : uniform_space X] [has_vadd M X] :
Prop

An additive action such that for all c, the map λ x, c +ᵥ x is uniformly continuous.

Instances of this typeclass
source
@[class]
structure has_uniform_continuous_const_smul (M : Type v) (X : Type x) [_inst_1 _inst_3 : uniform_space X] [has_smul M X] :
Prop

A multiplicative action such that for all c, the map λ x, c • x is uniformly continuous.

Instances of this typeclass
source
@[protected, instance]
def add_monoid.has_uniform_continuous_const_smul_nat (X : Type x) [uniform_space X] [add_group X] [uniform_add_group X] :
has_uniform_continuous_const_smul ℕ X
source
@[protected, instance]
def add_group.has_uniform_continuous_const_smul_int (X : Type x) [uniform_space X] [add_group X] [uniform_add_group X] :
has_uniform_continuous_const_smul ℤ X
source
theorem has_uniform_continuous_const_smul_of_continuous_const_smul (R : Type u) (M : Type v) [monoid R] [add_comm_group M] [distrib_mul_action R M] [uniform_space M] [uniform_add_group M] [has_continuous_const_smul R M] :
has_uniform_continuous_const_smul R M

A distrib_mul_action that is continuous on a uniform group is uniformly continuous. This can't be an instance due to it forming a loop with has_uniform_continuous_const_smul.to_has_continuous_const_smul

source
@[protected, instance]
def ring.has_uniform_continuous_const_smul (R : Type u) [ring R] [uniform_space R] [uniform_add_group R] [has_continuous_mul R] :
has_uniform_continuous_const_smul R R

The action of semiring.to_module is uniformly continuous.

source
@[protected, instance]
def ring.has_uniform_continuous_const_op_smul (R : Type u) [ring R] [uniform_space R] [uniform_add_group R] [has_continuous_mul R] :
has_uniform_continuous_const_smul Rᵐᵒᵖ R

The action of semiring.to_opposite_module is uniformly continuous.

source
@[protected, instance]
def has_uniform_continuous_const_vadd.to_has_continuous_const_vadd (M : Type v) (X : Type x) [uniform_space X] [has_vadd M X] [has_uniform_continuous_const_vadd M X] :
has_continuous_const_vadd M X
source
@[protected, instance]
def has_uniform_continuous_const_smul.to_has_continuous_const_smul (M : Type v) (X : Type x) [uniform_space X] [has_smul M X] [has_uniform_continuous_const_smul M X] :
has_continuous_const_smul M X
source
theorem uniform_continuous.const_smul {M : Type v} {X : Type x} {Y : Type y} [uniform_space X] [uniform_space Y] [has_smul M X] [has_uniform_continuous_const_smul M X] {f : Y → X} (hf : uniform_continuous f) (c : M) :
uniform_continuous (c • f)
source
theorem uniform_continuous.const_vadd {M : Type v} {X : Type x} {Y : Type y} [uniform_space X] [uniform_space Y] [has_vadd M X] [has_uniform_continuous_const_vadd M X] {f : Y → X} (hf : uniform_continuous f) (c : M) :
uniform_continuous (c +ᵥ f)
source
@[protected, instance]
def has_uniform_continuous_const_smul.op {M : Type v} {X : Type x} [uniform_space X] [has_smul M X] [has_smul Mᵐᵒᵖ X] [is_central_scalar M X] [has_uniform_continuous_const_smul M X] :
has_uniform_continuous_const_smul Mᵐᵒᵖ X

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

source
@[protected, instance]
def mul_opposite.has_uniform_continuous_const_smul {M : Type v} {X : Type x} [uniform_space X] [has_smul M X] [has_uniform_continuous_const_smul M X] :
has_uniform_continuous_const_smul M Xᵐᵒᵖ
source
@[protected, instance]
def add_opposite.has_uniform_continuous_const_vadd {M : Type v} {X : Type x} [uniform_space X] [has_vadd M X] [has_uniform_continuous_const_vadd M X] :
has_uniform_continuous_const_vadd M Xᵃᵒᵖ
source
@[protected, instance]
def uniform_group.to_has_uniform_continuous_const_smul {G : Type u} [group G] [uniform_space G] [uniform_group G] :
has_uniform_continuous_const_smul G G
source
@[protected, instance]
def uniform_add_group.to_has_uniform_continuous_const_vadd {G : Type u} [add_group G] [uniform_space G] [uniform_add_group G] :
has_uniform_continuous_const_vadd G G
source
@[protected, instance]
noncomputable def uniform_space.completion.has_smul (M : Type v) (X : Type x) [uniform_space X] [has_smul M X] :
has_smul M (uniform_space.completion X)
Equations
source
@[protected, instance]
noncomputable def uniform_space.completion.has_vadd (M : Type v) (X : Type x) [uniform_space X] [has_vadd M X] :
has_vadd M (uniform_space.completion X)
Equations
source
theorem uniform_space.completion.smul_def (M : Type v) (X : Type x) [uniform_space X] [has_smul M X] (c : M) (x : uniform_space.completion X) :
c • x = uniform_space.completion.map (has_smul.smul c) x
source
@[protected, instance]
def uniform_space.completion.has_uniform_continuous_const_vadd (M : Type v) (X : Type x) [uniform_space X] [has_vadd M X] :
has_uniform_continuous_const_vadd M (uniform_space.completion X)
source
@[protected, instance]
def uniform_space.completion.has_uniform_continuous_const_smul (M : Type v) (X : Type x) [uniform_space X] [has_smul M X] :
has_uniform_continuous_const_smul M (uniform_space.completion X)
source
@[protected, instance]
def uniform_space.completion.is_scalar_tower (M : Type v) (N : Type w) (X : Type x) [uniform_space X] [has_smul M X] [has_smul N X] [has_smul M N] [has_uniform_continuous_const_smul M X] [has_uniform_continuous_const_smul N X] [is_scalar_tower M N X] :
is_scalar_tower M N (uniform_space.completion X)
source
@[protected, instance]
def uniform_space.completion.smul_comm_class (M : Type v) (N : Type w) (X : Type x) [uniform_space X] [has_smul M X] [has_smul N X] [smul_comm_class M N X] [has_uniform_continuous_const_smul M X] [has_uniform_continuous_const_smul N X] :
smul_comm_class M N (uniform_space.completion X)
source
@[protected, instance]
def uniform_space.completion.is_central_scalar (M : Type v) (X : Type x) [uniform_space X] [has_smul M X] [has_smul Mᵐᵒᵖ X] [is_central_scalar M X] :
is_central_scalar M (uniform_space.completion X)
source
@[simp, norm_cast]
theorem uniform_space.completion.coe_smul {M : Type v} {X : Type x} [uniform_space X] [has_smul M X] [has_uniform_continuous_const_smul M X] (c : M) (x : X) :
↑(c • x) = c • ↑x
source
@[simp, norm_cast]
theorem uniform_space.completion.coe_vadd {M : Type v} {X : Type x} [uniform_space X] [has_vadd M X] [has_uniform_continuous_const_vadd M X] (c : M) (x : X) :
↑(c +ᵥ x) = c +ᵥ ↑x
source
@[protected, instance]
noncomputable def uniform_space.completion.add_action (M : Type v) (X : Type x) [uniform_space X] [add_monoid M] [add_action M X] [has_uniform_continuous_const_vadd M X] :
add_action M (uniform_space.completion X)
Equations
source
@[protected, instance]
noncomputable def uniform_space.completion.mul_action (M : Type v) (X : Type x) [uniform_space X] [monoid M] [mul_action M X] [has_uniform_continuous_const_smul M X] :
mul_action M (uniform_space.completion X)
Equations