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

TODO: Generalise the results here from the concrete Completion to any AbstractCompletion.

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

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

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

    Instances
      source
      instance AddMonoid.uniformContinuousConstSMul_nat (X : Type x) [UniformSpace X] [AddGroup X] [UniformAddGroup X] :
      UniformContinuousConstSMul ℕ X
      Equations
      source
      instance AddGroup.uniformContinuousConstSMul_int (X : Type x) [UniformSpace X] [AddGroup X] [UniformAddGroup X] :
      UniformContinuousConstSMul ℤ X
      Equations
      source
      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

      source
      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
      source
      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
      source
      instance UniformContinuousConstVAdd.to_continuousConstVAdd (M : Type v) (X : Type x) [UniformSpace X] [VAdd M X] [UniformContinuousConstVAdd M X] :
      ContinuousConstVAdd M X
      Equations
      source
      instance UniformContinuousConstSMul.to_continuousConstSMul (M : Type v) (X : Type x) [UniformSpace X] [SMul M X] [UniformContinuousConstSMul M X] :
      ContinuousConstSMul M X
      Equations
      source
      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)
      source
      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)
      source
      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
      source
      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
      source
      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
      source
      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
      source
      instance AddOpposite.uniformContinuousConstVAdd {M : Type v} {X : Type x} [UniformSpace X] [VAdd M X] [UniformContinuousConstVAdd M X] :
      UniformContinuousConstVAdd M Xᵃᵒᵖ
      Equations
      source
      instance MulOpposite.uniformContinuousConstSMul {M : Type v} {X : Type x} [UniformSpace X] [SMul M X] [UniformContinuousConstSMul M X] :
      UniformContinuousConstSMul M Xᵐᵒᵖ
      Equations
      source
      instance UniformAddGroup.to_uniformContinuousConstVAdd {G : Type u} [AddGroup G] [UniformSpace G] [UniformAddGroup G] :
      UniformContinuousConstVAdd G G
      Equations
      source
      instance UniformGroup.to_uniformContinuousConstSMul {G : Type u} [Group G] [UniformSpace G] [UniformGroup G] :
      UniformContinuousConstSMul G G
      Equations
      source
      noncomputable instance UniformSpace.Completion.instVAddCompletion (M : Type v) (X : Type x) [UniformSpace X] [VAdd M X] :
      VAdd M (UniformSpace.Completion X)
      Equations
      source
      noncomputable instance UniformSpace.Completion.instSMulCompletion (M : Type v) (X : Type x) [UniformSpace X] [SMul M X] :
      SMul M (UniformSpace.Completion X)
      Equations
      source
      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
      source
      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
      source
      instance UniformSpace.Completion.instUniformContinuousConstVAddCompletionUniformSpaceInstVAddCompletion (M : Type v) (X : Type x) [UniformSpace X] [VAdd M X] :
      UniformContinuousConstVAdd M (UniformSpace.Completion X)
      Equations
      source
      instance UniformSpace.Completion.instUniformContinuousConstSMulCompletionUniformSpaceInstSMulCompletion (M : Type v) (X : Type x) [UniformSpace X] [SMul M X] :
      UniformContinuousConstSMul M (UniformSpace.Completion X)
      Equations
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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
      source
      @[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
      source
      @[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
      source
      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.
      source
      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)
      source
      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
      source
      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