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

      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 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 : XY} (hf : UniformInducing f) (hsmul : ∀ (c : M) (x : X), f (c +ᵥ x) = c +ᵥ f 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 : XY} (hf : UniformInducing f) (hsmul : ∀ (c : M) (x : X), f (c x) = c f x) :
      @[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
      • =
      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