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.

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.

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.

    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

      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

      The action of Semiring.toModule is uniformly continuous.

      Equations
      • =

      The action of Semiring.toOppositeModule is uniformly continuous.

      Equations
      • =
      @[instance 100]
      Equations
      • =
      @[instance 100]
      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 : YX} (hf : UniformContinuous f) (c : M) :
      theorem UniformContinuous.const_smul {M : Type v} {X : Type x} {Y : Type y} [UniformSpace X] [UniformSpace Y] [SMul M X] [UniformContinuousConstSMul M X] {f : YX} (hf : UniformContinuous f) (c : M) :
      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 : XY} (hf : IsUniformInducing f) (hsmul : ∀ (c : M) (x : X), f (c +ᵥ x) = c +ᵥ f x) :
      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 : XY} (hf : IsUniformInducing f) (hsmul : ∀ (c : M) (x : X), f (c x) = c f 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 : XY} (hf : IsUniformInducing f) (hsmul : ∀ (c : M) (x : X), f (c x) = c f x) :

      Alias of IsUniformInducing.uniformContinuousConstSMul.

      @[instance 100]

      If an additive action is central, then its right action is uniform continuous when its left action is.

      Equations
      • =
      @[instance 100]

      If a scalar action is central, then its right action is uniform continuous when its left action is.

      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.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
      noncomputable instance UniformSpace.Completion.instVAdd (M : Type v) (X : Type x) [UniformSpace X] [VAdd M X] :
      Equations
      noncomputable instance UniformSpace.Completion.instSMul (M : Type v) (X : Type x) [UniformSpace X] [SMul M X] :
      Equations
      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
      @[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