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

• uniformContinuous_const_vadd : ∀ (c : M), UniformContinuous ((fun x x_1 => x +ᵥ x_1) c)

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

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

• uniformContinuous_const_smul : ∀ (c : M), UniformContinuous ((fun x x_1 => x • x_1) c)

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

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

Equations

• AddMonoid.uniformContinuousConstSMul_nat = AddMonoid.uniformContinuousConstSMul_nat.proof_1

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

Equations

• AddGroup.uniformContinuousConstSMul_int = AddGroup.uniformContinuousConstSMul_int.proof_1

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

• Ring.uniformContinuousConstSMul = Ring.uniformContinuousConstSMul.proof_1

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

• Ring.uniformContinuousConstSMul_op = Ring.uniformContinuousConstSMul_op.proof_1

theorem UniformContinuousConstVAdd.to_continuousConstVAdd.proof_1 (M : Type u_1) (X : Type u_2) [UniformSpace X] [VAdd M X] [UniformContinuousConstVAdd M X] : ContinuousConstVAdd M X

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

Equations

• UniformContinuousConstVAdd.to_continuousConstVAdd = UniformContinuousConstVAdd.to_continuousConstVAdd.proof_1

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

Equations

• UniformContinuousConstSMul.to_continuousConstSMul = UniformContinuousConstSMul.to_continuousConstSMul.proof_1

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 UniformContinuousConstVAdd.op.proof_1 {M : Type u_1} {X : Type u_2} [UniformSpace X] [VAdd M X] [VAdd Mᵃᵒᵖ X] [IsCentralVAdd M X] [UniformContinuousConstVAdd M X] : UniformContinuousConstVAdd 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

• @UniformContinuousConstVAdd.op = @UniformContinuousConstVAdd.op.proof_1

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

• @UniformContinuousConstSMul.op = @UniformContinuousConstSMul.op.proof_1

theorem AddOpposite.uniformContinuousConstVAdd.proof_1 {M : Type u_1} {X : Type u_2} [UniformSpace X] [VAdd M X] [UniformContinuousConstVAdd M X] : UniformContinuousConstVAdd M Xᵃᵒᵖ

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

Equations

• @AddOpposite.uniformContinuousConstVAdd = @AddOpposite.uniformContinuousConstVAdd.proof_1

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

Equations

• @MulOpposite.uniformContinuousConstSMul = @MulOpposite.uniformContinuousConstSMul.proof_1

theorem UniformAddGroup.to_uniformContinuousConstVAdd.proof_1 {G : Type u_1} [AddGroup G] [UniformSpace G] [UniformAddGroup G] : UniformContinuousConstVAdd G G

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

Equations

• @UniformAddGroup.to_uniformContinuousConstVAdd = @UniformAddGroup.to_uniformContinuousConstVAdd.proof_1

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

Equations

• @UniformGroup.to_uniformContinuousConstSMul = @UniformGroup.to_uniformContinuousConstSMul.proof_1

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 => UniformSpace.Completion.map ((fun x x_1 => x +ᵥ x_1) c) }

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 => UniformSpace.Completion.map ((fun x x_1 => x • x_1) c) }

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 => 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 => c • x) x

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

Equations

• One or more equations did not get rendered due to their size.

theorem UniformSpace.Completion.instUniformContinuousConstVAddCompletionUniformSpaceInstVAddCompletion.proof_1 (M : Type u_1) (X : Type u_2) [UniformSpace X] [VAdd M X] : UniformContinuousConstVAdd M (UniformSpace.Completion X)

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

Equations

• One or more equations did not get rendered due to their size.

theorem UniformSpace.Completion.instVAddAssocClass.proof_1 (M : Type u_1) (N : Type u_2) (X : Type u_3) [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)

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

• UniformSpace.Completion.instVAddAssocClass = UniformSpace.Completion.instVAddAssocClass.proof_1

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

• UniformSpace.Completion.instIsScalarTower = UniformSpace.Completion.instIsScalarTower.proof_1

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

• UniformSpace.Completion.instVAddCommClassCompletionInstVAddCompletionInstVAddCompletion = UniformSpace.Completion.instVAddCommClassCompletionInstVAddCompletionInstVAddCompletion.proof_1

theorem UniformSpace.Completion.instVAddCommClassCompletionInstVAddCompletionInstVAddCompletion.proof_1 (M : Type u_1) (N : Type u_2) (X : Type u_3) [UniformSpace X] [VAdd M X] [VAdd N X] [VAddCommClass M N X] [UniformContinuousConstVAdd M X] [UniformContinuousConstVAdd N X] : VAddCommClass M N (UniformSpace.Completion X)

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

• UniformSpace.Completion.instSMulCommClassCompletionInstSMulCompletionInstSMulCompletion = UniformSpace.Completion.instSMulCommClassCompletionInstSMulCompletionInstSMulCompletion.proof_1

theorem UniformSpace.Completion.instIsCentralVAddCompletionInstVAddCompletionAddOpposite.proof_1 (M : Type u_1) (X : Type u_2) [UniformSpace X] [VAdd M X] [VAdd Mᵃᵒᵖ X] [IsCentralVAdd M X] : IsCentralVAdd M (UniformSpace.Completion X)

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

• UniformSpace.Completion.instIsCentralVAddCompletionInstVAddCompletionAddOpposite = UniformSpace.Completion.instIsCentralVAddCompletionInstVAddCompletionAddOpposite.proof_1

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

• UniformSpace.Completion.instIsCentralScalarCompletionInstSMulCompletionMulOpposite = UniformSpace.Completion.instIsCentralScalarCompletionInstSMulCompletionMulOpposite.proof_1

@[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

• One or more equations did not get rendered due to their size.

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

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)

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 (_ : ∀ (a : UniformSpace.Completion X), 1 • a = a) (_ : ∀ (x y : M) (a : UniformSpace.Completion X), (x * y) • a = x • y • a)