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) [UniformSpace X] [VAdd M X] : Prop

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

• uniformContinuous_const_vadd (c : M) : UniformContinuous fun (x : X) => c +ᵥ x

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

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

• uniformContinuous_const_smul (c : M) : UniformContinuous fun (x : X) => c • x

instance AddMonoid.uniformContinuousConstSMul_nat (X : Type x) [UniformSpace X] [AddGroup X] [IsUniformAddGroup X] : UniformContinuousConstSMul ℕ X

instance AddGroup.uniformContinuousConstSMul_int (X : Type x) [UniformSpace X] [AddGroup X] [IsUniformAddGroup X] : UniformContinuousConstSMul ℤ X

theorem uniformContinuousConstSMul_of_continuousConstSMul (R : Type u) (M : Type v) [AddGroup M] [DistribSMul R M] [UniformSpace M] [IsUniformAddGroup M] [ContinuousConstSMul R M] : UniformContinuousConstSMul R M

A DistribSMul 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] [UniformSpace R] [IsUniformAddGroup R] [ContinuousMul R] : UniformContinuousConstSMul R R

The action of Semiring.toModule is uniformly continuous.

instance Ring.uniformContinuousConstSMul_op (R : Type u) [Ring R] [UniformSpace R] [IsUniformAddGroup R] [ContinuousMul R] : UniformContinuousConstSMul Rᵐᵒᵖ R

The action of Semiring.toOppositeModule is uniformly continuous.

@[instance 100]

instance UniformContinuousConstSMul.to_continuousConstSMul (M : Type v) (X : Type x) [UniformSpace X] [SMul M X] [UniformContinuousConstSMul M X] : ContinuousConstSMul M X

@[instance 100]

instance UniformContinuousConstVAdd.to_continuousConstVAdd (M : Type v) (X : Type x) [UniformSpace X] [VAdd M X] [UniformContinuousConstVAdd M X] : ContinuousConstVAdd M X

theorem UniformContinuous.const_smul {M : Type v} {X : Type x} {Y : Type y} [UniformSpace X] [UniformSpace Y] [SMul M X] [UniformContinuousConstSMul M X] {f : Y → X} (hf : UniformContinuous f) (c : M) : UniformContinuous (c • f)

theorem UniformContinuous.const_vadd {M : Type v} {X : Type x} {Y : Type y} [UniformSpace X] [UniformSpace Y] [VAdd M X] [UniformContinuousConstVAdd M X] {f : Y → X} (hf : UniformContinuous f) (c : M) : UniformContinuous (c +ᵥ f)

theorem IsUniformInducing.uniformContinuousConstSMul {M : Type v} {X : Type x} {Y : Type y} [UniformSpace X] [UniformSpace Y] [SMul M X] [SMul M Y] [UniformContinuousConstSMul M Y] {f : X → Y} (hf : IsUniformInducing f) (hsmul : ∀ (c : M) (x : X), f (c • x) = c • f x) : UniformContinuousConstSMul M X

theorem IsUniformInducing.uniformContinuousConstVAdd {M : Type v} {X : Type x} {Y : Type y} [UniformSpace X] [UniformSpace Y] [VAdd M X] [VAdd M Y] [UniformContinuousConstVAdd M Y] {f : X → Y} (hf : IsUniformInducing f) (hvadd : ∀ (c : M) (x : X), f (c +ᵥ x) = c +ᵥ f x) : UniformContinuousConstVAdd M X

@[instance 100]

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

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

@[instance 100]

instance UniformContinuousConstVAdd.op {M : Type v} {X : Type x} [UniformSpace X] [VAdd M X] [VAdd Mᵃᵒᵖ X] [IsCentralVAdd M X] [UniformContinuousConstVAdd M X] : UniformContinuousConstVAdd Mᵃᵒᵖ X

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

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

instance AddOpposite.uniformContinuousConstVAdd {M : Type v} {X : Type x} [UniformSpace X] [VAdd M X] [UniformContinuousConstVAdd M X] : UniformContinuousConstVAdd M Xᵃᵒᵖ

instance IsUniformGroup.to_uniformContinuousConstSMul {G : Type u} [Group G] [UniformSpace G] [IsUniformGroup G] : UniformContinuousConstSMul G G

instance IsUniformAddGroup.to_uniformContinuousConstVAdd {G : Type u} [AddGroup G] [UniformSpace G] [IsUniformAddGroup G] : UniformContinuousConstVAdd G G

theorem UniformContinuous.const_mul' {R : Type u_1} {β : Type u_2} [Ring R] [UniformSpace R] [UniformSpace β] [UniformContinuousConstSMul R R] {f : β → R} (hf : UniformContinuous f) (a : R) : UniformContinuous fun (x : β) => a * f x

theorem UniformContinuous.mul_const' {R : Type u_1} {β : Type u_2} [Ring R] [UniformSpace R] [UniformSpace β] [UniformContinuousConstSMul Rᵐᵒᵖ R] {f : β → R} (hf : UniformContinuous f) (a : R) : UniformContinuous fun (x : β) => f x * a

theorem uniformContinuous_mul_left' {R : Type u_1} [Ring R] [UniformSpace R] [UniformContinuousConstSMul R R] (a : R) : UniformContinuous fun (b : R) => a * b

theorem uniformContinuous_mul_right' {R : Type u_1} [Ring R] [UniformSpace R] [UniformContinuousConstSMul Rᵐᵒᵖ R] (a : R) : UniformContinuous fun (b : R) => b * a

theorem UniformContinuous.div_const' {R : Type u_3} {β : Type u_4} [DivisionRing R] [UniformSpace R] [UniformContinuousConstSMul Rᵐᵒᵖ R] [UniformSpace β] {f : β → R} (hf : UniformContinuous f) (a : R) : UniformContinuous fun (x : β) => f x / a

theorem uniformContinuous_div_const' {R : Type u_3} [DivisionRing R] [UniformSpace R] [UniformContinuousConstSMul Rᵐᵒᵖ R] (a : R) : UniformContinuous fun (b : R) => b / a

theorem IsUnit.smul_uniformity {M : Type v} {X : Type x} [UniformSpace X] [Monoid M] [MulAction M X] [UniformContinuousConstSMul M X] {c : M} (hc : IsUnit c) : c • uniformity X = uniformity X

theorem IsAddUnit.vadd_uniformity {M : Type v} {X : Type x} [UniformSpace X] [AddMonoid M] [AddAction M X] [UniformContinuousConstVAdd M X] {c : M} (hc : IsAddUnit c) : c +ᵥ uniformity X = uniformity X

@[simp]

theorem smul_uniformity {M : Type v} {X : Type x} [UniformSpace X] [Group M] [MulAction M X] [UniformContinuousConstSMul M X] (c : M) : c • uniformity X = uniformity X

@[simp]

theorem vadd_uniformity {M : Type v} {X : Type x} [UniformSpace X] [AddGroup M] [AddAction M X] [UniformContinuousConstVAdd M X] (c : M) : c +ᵥ uniformity X = uniformity X

theorem smul_uniformity₀ {M : Type v} {X : Type x} [UniformSpace X] [GroupWithZero M] [MulAction M X] [UniformContinuousConstSMul M X] {c : M} (hc : c ≠ 0) : c • uniformity X = uniformity X

@[implicit_reducible]

noncomputable instance UniformSpace.Completion.instSMul (M : Type v) (X : Type x) [UniformSpace X] [SMul M X] : SMul M (Completion X)

@[implicit_reducible]

noncomputable instance UniformSpace.Completion.instVAdd (M : Type v) (X : Type x) [UniformSpace X] [VAdd M X] : VAdd M (Completion X)

theorem UniformSpace.Completion.smul_def (M : Type v) (X : Type x) [UniformSpace X] [SMul M X] (c : M) (x : Completion X) : c • x = Completion.map (fun (x : X) => c • x) x

theorem UniformSpace.Completion.vadd_def (M : Type v) (X : Type x) [UniformSpace X] [VAdd M X] (c : M) (x : Completion X) : c +ᵥ x = Completion.map (fun (x : X) => c +ᵥ x) x

instance UniformSpace.Completion.instUniformContinuousConstSMul (M : Type v) (X : Type x) [UniformSpace X] [SMul M X] : UniformContinuousConstSMul M (Completion X)

instance UniformSpace.Completion.instUniformContinuousConstVAdd (M : Type v) (X : Type x) [UniformSpace X] [VAdd M X] : UniformContinuousConstVAdd M (Completion X)

instance UniformSpace.Completion.instIsScalarTower (M : Type v) (N : Type w) (X : Type x) [UniformSpace X] [SMul M X] [SMul N X] [SMul M N] [UniformContinuousConstSMul M X] [UniformContinuousConstSMul N X] [IsScalarTower M N X] : IsScalarTower M N (Completion X)

instance UniformSpace.Completion.instVAddAssocClass (M : Type v) (N : Type w) (X : Type x) [UniformSpace X] [VAdd M X] [VAdd N X] [VAdd M N] [UniformContinuousConstVAdd M X] [UniformContinuousConstVAdd N X] [VAddAssocClass M N X] : VAddAssocClass M N (Completion X)

instance UniformSpace.Completion.instSMulCommClassOfUniformContinuousConstSMul (M : Type v) (N : Type w) (X : Type x) [UniformSpace X] [SMul M X] [SMul N X] [SMulCommClass M N X] [UniformContinuousConstSMul M X] [UniformContinuousConstSMul N X] : SMulCommClass M N (Completion X)

instance UniformSpace.Completion.instVAddCommClassOfUniformContinuousConstVAdd (M : Type v) (N : Type w) (X : Type x) [UniformSpace X] [VAdd M X] [VAdd N X] [VAddCommClass M N X] [UniformContinuousConstVAdd M X] [UniformContinuousConstVAdd N X] : VAddCommClass M N (Completion X)

instance UniformSpace.Completion.instIsCentralScalar (M : Type v) (X : Type x) [UniformSpace X] [SMul M X] [SMul Mᵐᵒᵖ X] [IsCentralScalar M X] : IsCentralScalar M (Completion X)

instance UniformSpace.Completion.instIsCentralVAdd (M : Type v) (X : Type x) [UniformSpace X] [VAdd M X] [VAdd Mᵃᵒᵖ X] [IsCentralVAdd M X] : IsCentralVAdd M (Completion X)

@[simp]

theorem UniformSpace.Completion.coe_smul {M : Type v} {X : Type x} [UniformSpace X] [SMul M X] [UniformContinuousConstSMul M X] (c : M) (x : X) : ↑(c • x) = c • ↑x

@[simp]

theorem UniformSpace.Completion.coe_vadd {M : Type v} {X : Type x} [UniformSpace X] [VAdd M X] [UniformContinuousConstVAdd M X] (c : M) (x : X) : ↑(c +ᵥ x) = c +ᵥ ↑x

@[implicit_reducible]

noncomputable instance UniformSpace.Completion.instMulActionOfUniformContinuousConstSMul (M : Type v) (X : Type x) [UniformSpace X] [Monoid M] [MulAction M X] [UniformContinuousConstSMul M X] : MulAction M (Completion X)

@[implicit_reducible]

noncomputable instance UniformSpace.Completion.instAddActionOfUniformContinuousConstVAdd (M : Type v) (X : Type x) [UniformSpace X] [AddMonoid M] [AddAction M X] [UniformContinuousConstVAdd M X] : AddAction M (Completion X)