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
uniform_space.completion.distrib_mul_action
uniform_space.completion.mul_action_with_zero
uniform_space.completion.module
TODO: Generalise the results here from the concrete completion
to any abstract_completion
.
- 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.
- 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
- has_uniform_continuous_const_smul.op
- uniform_space.completion.normed_space.to_has_uniform_continuous_const_smul
- add_monoid.has_uniform_continuous_const_smul_nat
- add_group.has_uniform_continuous_const_smul_int
- ring.has_uniform_continuous_const_smul
- ring.has_uniform_continuous_const_op_smul
- mul_opposite.has_uniform_continuous_const_smul
- uniform_group.to_has_uniform_continuous_const_smul
- uniform_space.completion.has_uniform_continuous_const_smul
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
The action of semiring.to_module
is uniformly continuous.
The action of semiring.to_opposite_module
is uniformly continuous.
If a scalar is central, then its right action is uniform continuous when its left action is.
Equations
- uniform_space.completion.has_smul M X = {smul := λ (c : M), uniform_space.completion.map (has_smul.smul c)}
Equations
- uniform_space.completion.has_vadd M X = {vadd := λ (c : M), uniform_space.completion.map (has_vadd.vadd c)}
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 := _}
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 := _}