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] [UniformAddGroup X] : UniformContinuousConstSMul ℕ X

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem uniformContinuousConstSMul_of_continuousConstSMul (R : Type u) (M : Type v) [Monoid R] [AddCommGroup M] [DistribMulAction R M] [UniformSpace M] [UniformAddGroup M] [ContinuousConstSMul R M] : UniformContinuousConstSMul R M

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] [UniformSpace R] [UniformAddGroup R] [ContinuousMul R] : UniformContinuousConstSMul R R

The action of Semiring.toModule is uniformly continuous.

Equations

• ⋯ = ⋯

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

The action of Semiring.toOppositeModule is uniformly continuous.

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 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 UniformInducing.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 : UniformInducing f) (hsmul : ∀ (c : M) (x : X), f (c +ᵥ x) = c +ᵥ f x) : UniformContinuousConstVAdd M X

theorem UniformInducing.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 : UniformInducing f) (hsmul : ∀ (c : M) (x : X), f (c • x) = c • f x) : UniformContinuousConstSMul M X

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.

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• UniformSpace.Completion.instVAddCompletion M X = { vadd := fun (c : M) => UniformSpace.Completion.map fun (x : X) => c +ᵥ x }

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

Equations

• UniformSpace.Completion.instSMulCompletion M X = { smul := fun (c : M) => UniformSpace.Completion.map fun (x : X) => c • x }

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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 (UniformSpace.Completion X)

Equations

• ⋯ = ⋯

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 (UniformSpace.Completion X)

Equations

• ⋯ = ⋯

instance UniformSpace.Completion.instVAddCommClassCompletionInstVAddCompletionInstVAddCompletion (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 (UniformSpace.Completion X)

Equations

• ⋯ = ⋯

instance UniformSpace.Completion.instSMulCommClassCompletionInstSMulCompletionInstSMulCompletion (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 (UniformSpace.Completion X)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

theorem UniformSpace.Completion.coe_vadd {M : Type v} {X : Type x} [UniformSpace X] [VAdd M X] [UniformContinuousConstVAdd M X] (c : M) (x : X) : ↑X (c +ᵥ x) = c +ᵥ ↑X 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) : ↑X (c • x) = c • ↑X x

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

Equations

• UniformSpace.Completion.instAddActionCompletion M X = AddAction.mk ⋯ ⋯

theorem UniformSpace.Completion.instAddActionCompletion.proof_2 (M : Type u_2) (X : Type u_1) [UniformSpace X] [AddMonoid M] [AddAction M X] [UniformContinuousConstVAdd M X] (x : M) (y : M) (a : UniformSpace.Completion X) : x + y +ᵥ a = x +ᵥ (y +ᵥ a)

theorem UniformSpace.Completion.instAddActionCompletion.proof_1 (M : Type u_2) (X : Type u_1) [UniformSpace X] [AddMonoid M] [AddAction M X] [UniformContinuousConstVAdd M X] (a : UniformSpace.Completion X) : 0 +ᵥ a = a

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

Equations

• UniformSpace.Completion.instMulActionCompletion M X = MulAction.mk ⋯ ⋯