Multiplicative action on the completion of a uniform space #

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

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) [uniform_space X] [has_vadd M X] :

Prop

uniform_continuous_const_vadd : ∀ (c : M), uniform_continuous (has_vadd.vadd c)

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) [uniform_space X] [has_smul M X] :

Prop

uniform_continuous_const_smul : ∀ (c : M), uniform_continuous (has_smul.smul c)

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 action is central, then its right action is uniform continuous when its left action is.

source

@[protected, instance]

def has_uniform_continuous_const_vadd.op {M : Type v} {X : Type x} [uniform_space X] [has_vadd M X] [has_vadd Mᵃᵒᵖ X] [is_central_vadd M X] [has_uniform_continuous_const_vadd M X] :

has_uniform_continuous_const_vadd Mᵃᵒᵖ X

If an additive action 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

uniform_space.completion.has_smul M X = {smul := λ (c : M), uniform_space.completion.map (has_smul.smul c)}

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

uniform_space.completion.has_vadd M X = {vadd := λ (c : M), uniform_space.completion.map (has_vadd.vadd c)}

source

theorem uniform_space.completion.vadd_def (M : Type v) (X : Type x) [uniform_space X] [has_vadd M X] (c : M) (x : uniform_space.completion X) :

c +ᵥ x = uniform_space.completion.map (has_vadd.vadd c) x

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.vadd_assoc_class (M : Type v) (N : Type w) (X : Type x) [uniform_space X] [has_vadd M X] [has_vadd N X] [has_vadd M N] [has_uniform_continuous_const_vadd M X] [has_uniform_continuous_const_vadd N X] [vadd_assoc_class M N X] :

vadd_assoc_class 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.vadd_comm_class (M : Type v) (N : Type w) (X : Type x) [uniform_space X] [has_vadd M X] [has_vadd N X] [vadd_comm_class M N X] [has_uniform_continuous_const_vadd M X] [has_uniform_continuous_const_vadd N X] :

vadd_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

@[protected, instance]

def uniform_space.completion.is_central_vadd (M : Type v) (X : Type x) [uniform_space X] [has_vadd M X] [has_vadd Mᵃᵒᵖ X] [is_central_vadd M X] :

is_central_vadd 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

uniform_space.completion.add_action M X = {to_has_vadd := {vadd := has_vadd.vadd (uniform_space.completion.has_vadd M X)}, zero_vadd := _, add_vadd := _}

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

uniform_space.completion.mul_action M X = {to_has_smul := {smul := has_smul.smul (uniform_space.completion.has_smul M X)}, one_smul := _, mul_smul := _}