# Documentation

Mathlib.Topology.Algebra.UniformMulAction

# Multiplicative action on the completion of a uniform space #

In this file we define typeclasses UniformContinuousConstVAdd and UniformContinuousConstSMul and prove that a multiplicative action on X with uniformly continuous (•) c can be extended to a multiplicative action on UniformSpace.Completion X.

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

• UniformSpace.Completion.DistribMulAction
• UniformSpace.Completion.MulActionWithZero
• UniformSpace.Completion.Module

TODO: Generalise the results here from the concrete Completion to any AbstractCompletion.

class UniformContinuousConstVAdd (M : Type v) (X : Type x) [] [VAdd M X] :

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

Instances
class UniformContinuousConstSMul (M : Type v) (X : Type x) [] [SMul M X] :

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

Instances
theorem uniformContinuousConstSMul_of_continuousConstSMul (R : Type u) (M : Type v) [] [] [] [] [] [] :

A DistribMulAction that is continuous on a uniform group is uniformly continuous. This can't be an instance due to it forming a loop with UniformContinuousConstSMul.to_continuousConstSMul

instance Ring.uniformContinuousConstSMul (R : Type u) [Ring R] [] [] [] :

The action of Semiring.toModule is uniformly continuous.

instance Ring.uniformContinuousConstSMul_op (R : Type u) [Ring R] [] [] [] :

The action of Semiring.toOppositeModule is uniformly continuous.

theorem UniformContinuous.const_vadd {M : Type v} {X : Type x} {Y : Type y} [] [] [VAdd M X] {f : YX} (hf : ) (c : M) :
theorem UniformContinuous.const_smul {M : Type v} {X : Type x} {Y : Type y} [] [] [SMul M X] {f : YX} (hf : ) (c : M) :
theorem UniformContinuousConstVAdd.op.proof_1 {M : Type u_1} {X : Type u_2} [] [VAdd M X] [VAdd Mᵃᵒᵖ X] [] :
instance UniformContinuousConstVAdd.op {M : Type v} {X : Type x} [] [VAdd M X] [VAdd Mᵃᵒᵖ X] [] :

If an additive action is central, then its right action is uniform continuous when its left action is.

instance UniformContinuousConstSMul.op {M : Type v} {X : Type x} [] [SMul M X] [SMul Mᵐᵒᵖ X] [] :

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

instance MulOpposite.uniformContinuousConstSMul {M : Type v} {X : Type x} [] [SMul M X] :
noncomputable instance UniformSpace.Completion.instVAddCompletion (M : Type v) (X : Type x) [] [VAdd M X] :
noncomputable instance UniformSpace.Completion.instSMulCompletion (M : Type v) (X : Type x) [] [SMul M X] :
theorem UniformSpace.Completion.vadd_def (M : Type v) (X : Type x) [] [VAdd M X] (c : M) (x : ) :
c +ᵥ x = UniformSpace.Completion.map (fun x => c +ᵥ x) x
theorem UniformSpace.Completion.smul_def (M : Type v) (X : Type x) [] [SMul M X] (c : M) (x : ) :
c x = UniformSpace.Completion.map (fun x => c x) x
theorem UniformSpace.Completion.instVAddAssocClass.proof_1 (M : Type u_1) (N : Type u_2) (X : Type u_3) [] [VAdd M X] [VAdd N X] [VAdd M N] [] :
instance UniformSpace.Completion.instVAddAssocClass (M : Type v) (N : Type w) (X : Type x) [] [VAdd M X] [VAdd N X] [VAdd M N] [] :
instance UniformSpace.Completion.instIsScalarTower (M : Type v) (N : Type w) (X : Type x) [] [SMul M X] [SMul N X] [SMul M N] [] :
@[simp]
theorem UniformSpace.Completion.coe_vadd {M : Type v} {X : Type x} [] [VAdd M X] (c : M) (x : X) :
X (c +ᵥ x) = c +ᵥ X x
@[simp]
theorem UniformSpace.Completion.coe_smul {M : Type v} {X : Type x} [] [SMul M X] (c : M) (x : X) :
X (c x) = c X x
noncomputable instance UniformSpace.Completion.instAddActionCompletion (M : Type v) (X : Type x) [] [] [] :
theorem UniformSpace.Completion.instAddActionCompletion.proof_1 (M : Type u_2) (X : Type u_1) [] [] [] (a : ) :
0 +ᵥ a = a
theorem UniformSpace.Completion.instAddActionCompletion.proof_2 (M : Type u_2) (X : Type u_1) [] [] [] (x : M) (y : M) (a : ) :
x + y +ᵥ a = x +ᵥ (y +ᵥ a)
noncomputable instance UniformSpace.Completion.instMulActionCompletion (M : Type v) (X : Type x) [] [] [] :