doc-next-gen

Mathlib.Topology.Algebra.UniformMulAction

Module docstring

{"# 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. "}

UniformContinuousConstVAdd structure
[VAdd M X]
Full source 
/-- An additive action such that for all `c`, the map `fun x ↦ c +ᵥ x` is uniformly continuous. -/
class UniformContinuousConstVAdd [VAdd M X] : Prop where
  uniformContinuous_const_vadd : ∀ c : M, UniformContinuous (c +ᵥ · : X → X)
Uniformly continuous additive action
Informal description
The structure `UniformContinuousConstVAdd` represents an additive action of a type `M` on a uniform space `X` such that for every element `c` in `M`, the function `x ↦ c +ᵥ x` is uniformly continuous. This ensures that the additive action respects the uniform structure of `X`.
UniformContinuousConstSMul structure
[SMul M X]
Full source 
/-- A multiplicative action such that for all `c`,
the map `fun x ↦ c • x` is uniformly continuous. -/
@[to_additive]
class UniformContinuousConstSMul [SMul M X] : Prop where
  uniformContinuous_const_smul : ∀ c : M, UniformContinuous (c • · : X → X)
Uniformly continuous scalar multiplication
Informal description
A structure representing a multiplicative action where for each element \( c \) in the acting type \( M \), the scalar multiplication map \( x \mapsto c \cdot x \) is uniformly continuous on the uniform space \( X \).
AddMonoid.uniformContinuousConstSMul_nat instance
[AddGroup X] [IsUniformAddGroup X] : UniformContinuousConstSMul ℕ X
Full source 
instance AddMonoid.uniformContinuousConstSMul_nat [AddGroup X] [IsUniformAddGroup X] :
    UniformContinuousConstSMul ℕ X :=
  ⟨uniformContinuous_const_nsmul⟩
Uniform Continuity of Natural Number Scalar Multiplication on Uniform Additive Groups
Informal description
For any additive group $X$ with a uniform additive group structure, the natural scalar multiplication by natural numbers on $X$ is uniformly continuous.
AddGroup.uniformContinuousConstSMul_int instance
[AddGroup X] [IsUniformAddGroup X] : UniformContinuousConstSMul ℤ X
Full source 
instance AddGroup.uniformContinuousConstSMul_int [AddGroup X] [IsUniformAddGroup X] :
    UniformContinuousConstSMul ℤ X :=
  ⟨uniformContinuous_const_zsmul⟩
Uniform Continuity of Integer Scalar Multiplication on Uniform Additive Groups
Informal description
For any additive group $X$ with a uniform additive group structure, the scalar multiplication by integers on $X$ is uniformly continuous.
uniformContinuousConstSMul_of_continuousConstSMul theorem
[Monoid R] [AddGroup M] [DistribMulAction R M] [UniformSpace M] [IsUniformAddGroup M] [ContinuousConstSMul R M] : UniformContinuousConstSMul R M
Full source 
/-- 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` -/
theorem uniformContinuousConstSMul_of_continuousConstSMul [Monoid R] [AddGroup M]
    [DistribMulAction R M] [UniformSpace M] [IsUniformAddGroup M] [ContinuousConstSMul R M] :
    UniformContinuousConstSMul R M :=
  ⟨fun r =>
    uniformContinuous_of_continuousAt_zero (DistribMulAction.toAddMonoidHom M r)
      (Continuous.continuousAt (continuous_const_smul r))⟩
Uniform Continuity of Continuous Scalar Multiplication on Uniform Additive Groups
Informal description
Let $R$ be a monoid, $M$ be an additive group with a uniform space structure such that $M$ is a uniform additive group, and suppose there is a distributive multiplicative action of $R$ on $M$. If the scalar multiplication by any element of $R$ is continuous on $M$, then the scalar multiplication is uniformly continuous on $M$.
Ring.uniformContinuousConstSMul instance
[Ring R] [UniformSpace R] [IsUniformAddGroup R] [ContinuousMul R] : UniformContinuousConstSMul R R
Full source 
/-- The action of `Semiring.toModule` is uniformly continuous. -/
instance Ring.uniformContinuousConstSMul [Ring R] [UniformSpace R] [IsUniformAddGroup R]
    [ContinuousMul R] : UniformContinuousConstSMul R R :=
  uniformContinuousConstSMul_of_continuousConstSMul _ _
Uniform Continuity of Scalar Multiplication on Uniform Rings
Informal description
For any ring $R$ equipped with a uniform space structure such that $R$ is a uniform additive group and multiplication is continuous, the scalar multiplication by any element of $R$ on itself is uniformly continuous.
Ring.uniformContinuousConstSMul_op instance
[Ring R] [UniformSpace R] [IsUniformAddGroup R] [ContinuousMul R] : UniformContinuousConstSMul Rᵐᵒᵖ R
Full source 
/-- The action of `Semiring.toOppositeModule` is uniformly continuous. -/
instance Ring.uniformContinuousConstSMul_op [Ring R] [UniformSpace R] [IsUniformAddGroup R]
    [ContinuousMul R] : UniformContinuousConstSMul Rᵐᵒᵖ R :=
  uniformContinuousConstSMul_of_continuousConstSMul _ _
Uniform Continuity of Scalar Multiplication by Opposite Ring Elements
Informal description
For any ring $R$ equipped with a uniform space structure such that $R$ is a uniform additive group and multiplication is continuous, the scalar multiplication by any element of the opposite ring $R^\mathrm{op}$ on $R$ is uniformly continuous.
UniformContinuousConstSMul.to_continuousConstSMul instance
[UniformContinuousConstSMul M X] : ContinuousConstSMul M X
Full source 
@[to_additive]
instance (priority := 100) UniformContinuousConstSMul.to_continuousConstSMul
    [UniformContinuousConstSMul M X] : ContinuousConstSMul M X :=
  ⟨fun c => (uniformContinuous_const_smul c).continuous⟩
Uniformly Continuous Scalar Multiplication Implies Continuous Scalar Multiplication
Informal description
For any types $M$ and $X$ with a scalar multiplication operation $M \times X \to X$ where for each $c \in M$, the map $x \mapsto c \cdot x$ is uniformly continuous, the scalar multiplication is also continuous for each fixed $c \in M$.
UniformContinuous.const_smul theorem
[UniformContinuousConstSMul M X] {f : Y → X} (hf : UniformContinuous f) (c : M) : UniformContinuous (c • f)
Full source 
@[to_additive]
theorem UniformContinuous.const_smul [UniformContinuousConstSMul M X] {f : Y → X}
    (hf : UniformContinuous f) (c : M) : UniformContinuous (c • f) :=
  (uniformContinuous_const_smul c).comp hf
Uniform Continuity of Scalar Multiplication of a Function
Informal description
Let $M$ and $X$ be types with a scalar multiplication operation $M \times X \to X$ such that for each $c \in M$, the map $x \mapsto c \cdot x$ is uniformly continuous. If $f : Y \to X$ is a uniformly continuous function, then for any $c \in M$, the function $x \mapsto c \cdot f(x)$ is also uniformly continuous.
IsUniformInducing.uniformContinuousConstSMul theorem
[SMul M Y] [UniformContinuousConstSMul M Y] {f : X → Y} (hf : IsUniformInducing f) (hsmul : ∀ (c : M) x, f (c • x) = c • f x) : UniformContinuousConstSMul M X
Full source 
@[to_additive]
lemma IsUniformInducing.uniformContinuousConstSMul [SMul M Y] [UniformContinuousConstSMul M Y]
    {f : X → Y} (hf : IsUniformInducing f) (hsmul : ∀ (c : M) x, f (c • x) = c • f x) :
    UniformContinuousConstSMul M X where
  uniformContinuous_const_smul c := by
    simpa only [hf.uniformContinuous_iff, Function.comp_def, hsmul]
      using hf.uniformContinuous.const_smul c
Uniform Continuity of Induced Scalar Multiplication via Uniformly Inducing Map
Informal description
Let $M$ and $Y$ be types with a scalar multiplication operation $M \times Y \to Y$ such that for each $c \in M$, the map $y \mapsto c \cdot y$ is uniformly continuous. Given a uniformly inducing map $f : X \to Y$ that preserves scalar multiplication (i.e., $f(c \cdot x) = c \cdot f(x)$ for all $c \in M$ and $x \in X$), then the scalar multiplication on $X$ is also uniformly continuous for each fixed $c \in M$.
UniformContinuousConstSMul.op instance
[SMul Mᵐᵒᵖ X] [IsCentralScalar M X] [UniformContinuousConstSMul M X] : UniformContinuousConstSMul Mᵐᵒᵖ X
Full source 
/-- If a scalar action is central, then its right action is uniform continuous when its left action
is. -/
@[to_additive "If an additive action is central, then its right action is uniform
continuous when its left action is."]
instance (priority := 100) UniformContinuousConstSMul.op [SMul Mᵐᵒᵖ X] [IsCentralScalar M X]
    [UniformContinuousConstSMul M X] : UniformContinuousConstSMul Mᵐᵒᵖ X :=
  ⟨MulOpposite.rec' fun c ↦ by simpa only [op_smul_eq_smul] using uniformContinuous_const_smul c⟩
Uniform Continuity of Right Scalar Multiplication in Central Actions
Informal description
For a type $X$ with a scalar multiplication action by $M$ where each left multiplication map $x \mapsto c \cdot x$ is uniformly continuous, and assuming the action is central (i.e., left and right actions coincide), then each right multiplication map $x \mapsto x \cdot c$ is also uniformly continuous.
MulOpposite.uniformContinuousConstSMul instance
[UniformContinuousConstSMul M X] : UniformContinuousConstSMul M Xᵐᵒᵖ
Full source 
@[to_additive]
instance MulOpposite.uniformContinuousConstSMul [UniformContinuousConstSMul M X] :
    UniformContinuousConstSMul M Xᵐᵒᵖ :=
  ⟨fun c =>
    MulOpposite.uniformContinuous_op.comp <| MulOpposite.uniformContinuous_unop.const_smul c⟩
Uniformly Continuous Scalar Multiplication on Opposite Types
Informal description
For any type $X$ with a scalar multiplication action by $M$ where each left multiplication map $x \mapsto c \cdot x$ is uniformly continuous, the opposite type $X^\text{op}$ also has a uniformly continuous scalar multiplication action by $M$.
IsUniformGroup.to_uniformContinuousConstSMul instance
{G : Type u} [Group G] [UniformSpace G] [IsUniformGroup G] : UniformContinuousConstSMul G G
Full source 
@[to_additive]
instance IsUniformGroup.to_uniformContinuousConstSMul {G : Type u} [Group G] [UniformSpace G]
    [IsUniformGroup G] : UniformContinuousConstSMul G G :=
  ⟨fun _ => uniformContinuous_const.mul uniformContinuous_id⟩
Uniformly Continuous Group Action on Itself
Informal description
For any group $G$ equipped with a uniform space structure where the group operations are uniformly continuous, the scalar multiplication action of $G$ on itself is uniformly continuous.
UniformContinuous.const_mul' theorem
[UniformContinuousConstSMul R R] {f : β → R} (hf : UniformContinuous f) (a : R) : UniformContinuous fun x ↦ a * f x
Full source 
theorem UniformContinuous.const_mul' [UniformContinuousConstSMul R R] {f : β → R}
    (hf : UniformContinuous f) (a : R) : UniformContinuous fun x ↦ a * f x :=
  hf.const_smul a
Uniform Continuity of Left Multiplication by a Scalar
Informal description
Let $R$ be a type with a scalar multiplication operation $R \times R \to R$ such that for each $c \in R$, the map $x \mapsto c \cdot x$ is uniformly continuous. If $f : \beta \to R$ is a uniformly continuous function, then for any $a \in R$, the function $x \mapsto a \cdot f(x)$ is also uniformly continuous.
UniformContinuous.mul_const' theorem
[UniformContinuousConstSMul Rᵐᵒᵖ R] {f : β → R} (hf : UniformContinuous f) (a : R) : UniformContinuous fun x ↦ f x * a
Full source 
theorem UniformContinuous.mul_const' [UniformContinuousConstSMul Rᵐᵒᵖ R] {f : β → R}
    (hf : UniformContinuous f) (a : R) : UniformContinuous fun x ↦ f x * a :=
  hf.const_smul (MulOpposite.op a)
Uniform Continuity of Right Multiplication by a Scalar
Informal description
Let $R$ be a type with a scalar multiplication operation $R^{\text{op}} \times R \to R$ such that for each $c \in R^{\text{op}}$, the map $x \mapsto x \cdot c$ is uniformly continuous. If $f : \beta \to R$ is a uniformly continuous function, then for any $a \in R$, the function $x \mapsto f(x) \cdot a$ is also uniformly continuous.
uniformContinuous_mul_left' theorem
[UniformContinuousConstSMul R R] (a : R) : UniformContinuous fun b : R => a * b
Full source 
theorem uniformContinuous_mul_left' [UniformContinuousConstSMul R R] (a : R) :
    UniformContinuous fun b : R => a * b :=
  uniformContinuous_id.const_mul' _
Uniform Continuity of Left Multiplication by a Fixed Scalar
Informal description
Let $R$ be a uniform space with a scalar multiplication operation $R \times R \to R$ such that for each $c \in R$, the map $x \mapsto c \cdot x$ is uniformly continuous. Then for any fixed element $a \in R$, the left multiplication map $b \mapsto a \cdot b$ is uniformly continuous on $R$.
uniformContinuous_mul_right' theorem
[UniformContinuousConstSMul Rᵐᵒᵖ R] (a : R) : UniformContinuous fun b : R => b * a
Full source 
theorem uniformContinuous_mul_right' [UniformContinuousConstSMul Rᵐᵒᵖ R] (a : R) :
    UniformContinuous fun b : R => b * a :=
  uniformContinuous_id.mul_const' _
Uniform Continuity of Right Multiplication by a Fixed Scalar
Informal description
Let $R$ be a type with a scalar multiplication operation $R^{\text{op}} \times R \to R$ such that for each $c \in R^{\text{op}}$, the map $x \mapsto x \cdot c$ is uniformly continuous. Then for any fixed element $a \in R$, the right multiplication map $b \mapsto b \cdot a$ is uniformly continuous on $R$.
UniformContinuous.div_const' theorem
{R β : Type*} [DivisionRing R] [UniformSpace R] [UniformContinuousConstSMul Rᵐᵒᵖ R] [UniformSpace β] {f : β → R} (hf : UniformContinuous f) (a : R) : UniformContinuous fun x ↦ f x / a
Full source 
theorem UniformContinuous.div_const' {R β : Type*} [DivisionRing R] [UniformSpace R]
    [UniformContinuousConstSMul Rᵐᵒᵖ R] [UniformSpace β] {f : β → R}
    (hf : UniformContinuous f) (a : R) :
    UniformContinuous fun x ↦ f x / a := by
  simpa [div_eq_mul_inv] using hf.mul_const' a⁻¹
Uniform Continuity of Division by a Scalar
Informal description
Let $R$ be a division ring equipped with a uniform space structure, and suppose that for each $c \in R^{\text{op}}$, the right multiplication map $x \mapsto x \cdot c$ is uniformly continuous. Let $\beta$ be a uniform space and $f : \beta \to R$ be a uniformly continuous function. Then for any fixed element $a \in R$, the function $x \mapsto f(x) / a$ is uniformly continuous.
uniformContinuous_div_const' theorem
{R : Type*} [DivisionRing R] [UniformSpace R] [UniformContinuousConstSMul Rᵐᵒᵖ R] (a : R) : UniformContinuous fun b : R => b / a
Full source 
theorem uniformContinuous_div_const' {R : Type*} [DivisionRing R] [UniformSpace R]
    [UniformContinuousConstSMul Rᵐᵒᵖ R] (a : R) :
    UniformContinuous fun b : R => b / a :=
  uniformContinuous_id.div_const' _
Uniform Continuity of Division by a Fixed Scalar in a Division Ring
Informal description
Let $R$ be a division ring equipped with a uniform space structure, and suppose that for each $c \in R^{\text{op}}$, the right multiplication map $x \mapsto x \cdot c$ is uniformly continuous. Then for any fixed element $a \in R$, the division map $b \mapsto b / a$ is uniformly continuous on $R$.
UniformSpace.Completion.instSMul instance
: SMul M (Completion X)
Full source 
@[to_additive]
noncomputable instance : SMul M (Completion X) :=
  ⟨fun c => Completion.map (c • ·)⟩
Scalar Multiplication on the Completion of a Uniform Space
Informal description
For any uniform space $X$ with a scalar multiplication action by $M$ where the action is uniformly continuous, the completion of $X$ inherits a scalar multiplication action by $M$.
UniformSpace.Completion.smul_def theorem
(c : M) (x : Completion X) : c • x = Completion.map (c • ·) x
Full source 
@[to_additive]
theorem smul_def (c : M) (x : Completion X) : c • x = Completion.map (c • ·) x :=
  rfl
Definition of Scalar Multiplication in Completion via Mapping
Informal description
For any scalar $c$ in $M$ and any element $x$ in the completion of a uniform space $X$, the scalar multiplication $c \cdot x$ is equal to the completion of the map $\lambda y, c \cdot y$ applied to $x$.
UniformSpace.Completion.instUniformContinuousConstSMul instance
: UniformContinuousConstSMul M (Completion X)
Full source 
@[to_additive]
instance : UniformContinuousConstSMul M (Completion X) :=
  ⟨fun _ => uniformContinuous_map⟩
Uniformly Continuous Scalar Multiplication on the Completion of a Uniform Space
Informal description
For any uniform space $X$ with a scalar multiplication action by $M$ where the action is uniformly continuous, the completion of $X$ inherits a uniformly continuous scalar multiplication action by $M$.
UniformSpace.Completion.instIsScalarTower instance
[SMul N X] [SMul M N] [UniformContinuousConstSMul M X] [UniformContinuousConstSMul N X] [IsScalarTower M N X] : IsScalarTower M N (Completion X)
Full source 
@[to_additive]
instance instIsScalarTower [SMul N X] [SMul M N] [UniformContinuousConstSMul M X]
    [UniformContinuousConstSMul N X] [IsScalarTower M N X] : IsScalarTower M N (Completion X) :=
  ⟨fun m n x => by
    have : _ = (_ : Completion X → Completion X) :=
      map_comp (uniformContinuous_const_smul m) (uniformContinuous_const_smul n)
    refine Eq.trans ?_ (congr_fun this.symm x)
    exact congr_arg (fun f => Completion.map f x) (funext (smul_assoc _ _))⟩
Scalar Tower Property on Completion of Uniform Space
Informal description
For any uniform space $X$ with scalar multiplication actions by $M$ and $N$ that are both uniformly continuous, and given that $M$ acts on $X$ through $N$ (i.e., the scalar multiplication satisfies the tower property $m \cdot (n \cdot x) = (m \cdot n) \cdot x$ for all $m \in M$, $n \in N$, and $x \in X$), the completion of $X$ inherits the scalar tower property for $M$ and $N$.
UniformSpace.Completion.instSMulCommClassOfUniformContinuousConstSMul instance
[SMul N X] [SMulCommClass M N X] [UniformContinuousConstSMul M X] [UniformContinuousConstSMul N X] : SMulCommClass M N (Completion X)
Full source 
@[to_additive]
instance [SMul N X] [SMulCommClass M N X] [UniformContinuousConstSMul M X]
    [UniformContinuousConstSMul N X] : SMulCommClass M N (Completion X) :=
  ⟨fun m n x => by
    have hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x := rfl
    have hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x := rfl
    rw [hmn, hnm, map_comp, map_comp]
    · exact congr_arg (fun f => Completion.map f x) (funext (smul_comm _ _))
    repeat' exact uniformContinuous_const_smul _⟩
Commuting Scalar Actions on the Completion of a Uniform Space
Informal description
For any uniform space $X$ with scalar multiplication actions by $M$ and $N$ that are both uniformly continuous, and given that the actions of $M$ and $N$ commute on $X$, the completion of $X$ inherits a commuting scalar multiplication structure by $M$ and $N$.
UniformSpace.Completion.instIsCentralScalar instance
[SMul Mᵐᵒᵖ X] [IsCentralScalar M X] : IsCentralScalar M (Completion X)
Full source 
@[to_additive]
instance [SMul Mᵐᵒᵖ X] [IsCentralScalar M X] : IsCentralScalar M (Completion X) :=
  ⟨fun c a => (congr_arg fun f => Completion.map f a) <| funext (op_smul_eq_smul c)⟩
Central Scalar Property on Completion of Uniform Space
Informal description
For any uniform space $X$ with a scalar multiplication action by $M$ where the action is uniformly continuous, and given that $M$ has a central scalar property on $X$, the completion of $X$ inherits the central scalar property for $M$.
UniformSpace.Completion.coe_smul theorem
(c : M) (x : X) : (↑(c • x) : Completion X) = c • (x : Completion X)
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_smul (c : M) (x : X) : (↑(c • x) : Completion X) = c • (x : Completion X) :=
  (map_coe (uniformContinuous_const_smul c) x).symm
Compatibility of Scalar Multiplication with Completion Embedding
Informal description
For any element $c \in M$ and any point $x \in X$, the image of the scalar multiplication $c \cdot x$ under the canonical embedding into the completion of $X$ is equal to the scalar multiplication of $c$ with the image of $x$ in the completion, i.e., $\iota(c \cdot x) = c \cdot \iota(x)$, where $\iota: X \to \overline{X}$ is the completion map.
UniformSpace.Completion.instMulActionOfUniformContinuousConstSMul instance
[Monoid M] [MulAction M X] [UniformContinuousConstSMul M X] : MulAction M (Completion X)
Full source 
@[to_additive]
noncomputable instance [Monoid M] [MulAction M X] [UniformContinuousConstSMul M X] :
    MulAction M (Completion X) where
  smul := (· • ·)
  one_smul := ext' (continuous_const_smul _) continuous_id fun a => by rw [← coe_smul, one_smul]
  mul_smul x y :=
    ext' (continuous_const_smul _) ((continuous_const_smul _).const_smul _) fun a => by
      simp only [← coe_smul, mul_smul]
Multiplicative Action on the Completion of a Uniform Space
Informal description
For any monoid $M$ acting on a uniform space $X$ with uniformly continuous scalar multiplication, the completion of $X$ inherits a multiplicative action by $M$.