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 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

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

@[deprecated IsUniformInducing.uniformContinuousConstSMul]

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

Alias of IsUniformInducing.uniformContinuousConstSMul.

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

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

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

Equations

• UniformSpace.Completion.instVAdd M X = { vadd := fun (c : M) => UniformSpace.Completion.map fun (x : X) => c +ᵥ 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

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

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

Equations

• ⋯ = ⋯

instance UniformSpace.Completion.instUniformContinuousConstVAdd (M : Type v) (X : Type x) [UniformSpace X] [VAdd M X] : UniformContinuousConstVAdd M (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.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.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 (UniformSpace.Completion X)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

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

Equations

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

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

Equations

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