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

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

Instances

theorem UniformContinuousConstVAdd.uniformContinuous_const_vadd {M : Type v} {X : Type x} :

∀ {inst : UniformSpace X} {inst_1 : VAdd M X} [self : UniformContinuousConstVAdd M X] (c : M), UniformContinuous fun (x : X) => c +ᵥ x

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

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

Instances

theorem UniformContinuousConstSMul.uniformContinuous_const_smul {M : Type v} {X : Type x} :

∀ {inst : UniformSpace X} {inst_1 : SMul M X} [self : UniformContinuousConstSMul M X] (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 UniformContinuousConstVAdd.to_continuousConstVAdd (M : Type v) (X : Type x) [UniformSpace X] [VAdd M X] [UniformContinuousConstVAdd M X] :

ContinuousConstVAdd M X

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

⋯ = ⋯

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

⋯ = ⋯

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.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 }

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 }

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

UniformContinuousConstVAdd M (UniformSpace.Completion X)

Equations

⋯ = ⋯

instance UniformSpace.Completion.instUniformContinuousConstSMul (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.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.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.instIsCentralVAdd (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.instIsCentralScalar (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

theorem UniformSpace.Completion.instAddActionOfUniformContinuousConstVAdd.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.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 ⋯ ⋯

theorem UniformSpace.Completion.instAddActionOfUniformContinuousConstVAdd.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.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 ⋯ ⋯