Mathlib.Topology.Algebra.IsUniformGroup.Defs

IsUniformGroup structure

(α : Type*) [UniformSpace α] [Group α]

Full source

/-- A uniform group is a group in which multiplication and inversion are uniformly continuous. -/
class IsUniformGroup (α : Type*) [UniformSpace α] [Group α] : Prop where
  uniformContinuous_div : UniformContinuous fun p : α × α => p.1 / p.2

Uniform Group

Informal description

A uniform group is a group $\alpha$ equipped with a uniform space structure such that the group multiplication operation $(x, y) \mapsto x * y$ and the inversion operation $x \mapsto x^{-1}$ are uniformly continuous with respect to the uniformity on $\alpha$.

IsUniformAddGroup structure

(α : Type*) [UniformSpace α] [AddGroup α]

Full source

/-- A uniform additive group is an additive group in which addition
  and negation are uniformly continuous. -/
class IsUniformAddGroup (α : Type*) [UniformSpace α] [AddGroup α] : Prop where
  uniformContinuous_sub : UniformContinuous fun p : α × α => p.1 - p.2

Additive Uniform Group

Informal description

An additive uniform group is an additive group $\alpha$ equipped with a uniform space structure such that the addition operation $+ : \alpha \times \alpha \to \alpha$ and the negation operation $- : \alpha \to \alpha$ are uniformly continuous.

IsUniformGroup.mk' theorem

 {α} [UniformSpace α] [Group α] (h₁ : UniformContinuous fun p : α × α => p.1 * p.2)
  (h₂ : UniformContinuous fun p : α => p⁻¹) : IsUniformGroup α

Full source

@[to_additive]
theorem IsUniformGroup.mk' {α} [UniformSpace α] [Group α]
    (h₁ : UniformContinuous fun p : α × α => p.1 * p.2) (h₂ : UniformContinuous fun p : α => p⁻¹) :
    IsUniformGroup α :=
  ⟨by simpa only [div_eq_mul_inv] using
    h₁.comp (uniformContinuous_fst.prodMk (h₂.comp uniformContinuous_snd))⟩

Uniform Group Criterion via Uniform Continuity of Multiplication and Inversion

Informal description

Let $\alpha$ be a group equipped with a uniform space structure. If the multiplication map $(x, y) \mapsto x \cdot y$ and the inversion map $x \mapsto x^{-1}$ are uniformly continuous, then $\alpha$ is a uniform group.

uniformContinuous_div theorem

: UniformContinuous fun p : α × α => p.1 / p.2

Full source

@[to_additive]
theorem uniformContinuous_div : UniformContinuous fun p : α × α => p.1 / p.2 :=
  IsUniformGroup.uniformContinuous_div

Uniform Continuity of Division in Uniform Groups

Informal description

For a uniform group $\alpha$, the division operation $(x, y) \mapsto x / y$ is uniformly continuous with respect to the product uniformity on $\alpha \times \alpha$.

UniformContinuous.div theorem

 [UniformSpace β] {f : β → α} {g : β → α} (hf : UniformContinuous f) (hg : UniformContinuous g) :
  UniformContinuous fun x => f x / g x

Full source

@[to_additive]
theorem UniformContinuous.div [UniformSpace β] {f : β → α} {g : β → α} (hf : UniformContinuous f)
    (hg : UniformContinuous g) : UniformContinuous fun x => f x / g x :=
  uniformContinuous_div.comp (hf.prodMk hg)

Uniform Continuity of Pointwise Division in Uniform Groups

Informal description

Let $\alpha$ be a uniform group and $\beta$ be a uniform space. For any two uniformly continuous functions $f, g \colon \beta \to \alpha$, the function $x \mapsto f(x) / g(x)$ is uniformly continuous.

UniformContinuous.inv theorem

[UniformSpace β] {f : β → α} (hf : UniformContinuous f) : UniformContinuous fun x => (f x)⁻¹

Full source

@[to_additive]
theorem UniformContinuous.inv [UniformSpace β] {f : β → α} (hf : UniformContinuous f) :
    UniformContinuous fun x => (f x)⁻¹ := by
  have : UniformContinuous fun x => 1 / f x := uniformContinuous_const.div hf
  simp_all

Uniform Continuity of Inversion in Uniform Groups

Informal description

Let $\alpha$ be a uniform group and $\beta$ be a uniform space. For any uniformly continuous function $f \colon \beta \to \alpha$, the function $x \mapsto (f(x))^{-1}$ is uniformly continuous.

uniformContinuous_inv theorem

: UniformContinuous fun x : α => x⁻¹

Full source

@[to_additive]
theorem uniformContinuous_inv : UniformContinuous fun x : α => x⁻¹ :=
  uniformContinuous_id.inv

Uniform continuity of inversion in a uniform group

Informal description

In a uniform group $\alpha$, the inversion operation $x \mapsto x^{-1}$ is uniformly continuous.

UniformContinuous.mul theorem

 [UniformSpace β] {f : β → α} {g : β → α} (hf : UniformContinuous f) (hg : UniformContinuous g) :
  UniformContinuous fun x => f x * g x

Full source

@[to_additive]
theorem UniformContinuous.mul [UniformSpace β] {f : β → α} {g : β → α} (hf : UniformContinuous f)
    (hg : UniformContinuous g) : UniformContinuous fun x => f x * g x := by
  have : UniformContinuous fun x => f x / (g x)⁻¹ := hf.div hg.inv
  simp_all

Uniform Continuity of Pointwise Multiplication in Uniform Groups

Informal description

Let $\alpha$ be a uniform group and $\beta$ be a uniform space. For any two uniformly continuous functions $f, g \colon \beta \to \alpha$, the function $x \mapsto f(x) \cdot g(x)$ is uniformly continuous.

uniformContinuous_mul theorem

: UniformContinuous fun p : α × α => p.1 * p.2

Full source

@[to_additive]
theorem uniformContinuous_mul : UniformContinuous fun p : α × α => p.1 * p.2 :=
  uniformContinuous_fst.mul uniformContinuous_snd

Uniform continuity of multiplication in a uniform group

Informal description

In a uniform group $\alpha$, the multiplication operation $(x, y) \mapsto x \cdot y$ is uniformly continuous with respect to the product uniformity on $\alpha \times \alpha$.

UniformContinuous.mul_const theorem

[UniformSpace β] {f : β → α} (hf : UniformContinuous f) (a : α) : UniformContinuous fun x ↦ f x * a

Full source

@[to_additive]
theorem UniformContinuous.mul_const [UniformSpace β] {f : β → α} (hf : UniformContinuous f)
    (a : α) : UniformContinuous fun x ↦ f x * a :=
  hf.mul uniformContinuous_const

Uniform Continuity of Right Multiplication by a Constant in Uniform Groups

Informal description

Let $\alpha$ be a uniform group and $\beta$ be a uniform space. For any uniformly continuous function $f \colon \beta \to \alpha$ and any fixed element $a \in \alpha$, the function $x \mapsto f(x) \cdot a$ is uniformly continuous.

UniformContinuous.const_mul theorem

[UniformSpace β] {f : β → α} (hf : UniformContinuous f) (a : α) : UniformContinuous fun x ↦ a * f x

Full source

@[to_additive]
theorem UniformContinuous.const_mul [UniformSpace β] {f : β → α} (hf : UniformContinuous f)
    (a : α) : UniformContinuous fun x ↦ a * f x :=
  uniformContinuous_const.mul hf

Uniform continuity of left multiplication by a constant in a uniform group

Informal description

Let $\alpha$ be a uniform group and $\beta$ be a uniform space. For any uniformly continuous function $f \colon \beta \to \alpha$ and any fixed element $a \in \alpha$, the function $x \mapsto a \cdot f(x)$ is uniformly continuous.

uniformContinuous_mul_left theorem

(a : α) : UniformContinuous fun b : α => a * b

Full source

@[to_additive]
theorem uniformContinuous_mul_left (a : α) : UniformContinuous fun b : α => a * b :=
  uniformContinuous_id.const_mul _

Uniform continuity of left multiplication in a uniform group

Informal description

Let $\alpha$ be a uniform group. For any fixed element $a \in \alpha$, the left multiplication map $b \mapsto a * b$ is uniformly continuous.

uniformContinuous_mul_right theorem

(a : α) : UniformContinuous fun b : α => b * a

Full source

@[to_additive]
theorem uniformContinuous_mul_right (a : α) : UniformContinuous fun b : α => b * a :=
  uniformContinuous_id.mul_const _

Uniform Continuity of Right Multiplication in a Uniform Group

Informal description

For any element $a$ in a uniform group $\alpha$, the right multiplication function $b \mapsto b \cdot a$ is uniformly continuous.

UniformContinuous.div_const theorem

[UniformSpace β] {f : β → α} (hf : UniformContinuous f) (a : α) : UniformContinuous fun x ↦ f x / a

Full source

@[to_additive]
theorem UniformContinuous.div_const [UniformSpace β] {f : β → α} (hf : UniformContinuous f)
    (a : α) : UniformContinuous fun x ↦ f x / a :=
  hf.div uniformContinuous_const

Uniform Continuity of Right Division by a Constant in Uniform Groups

Informal description

Let $\alpha$ be a uniform group and $\beta$ be a uniform space. For any uniformly continuous function $f \colon \beta \to \alpha$ and any fixed element $a \in \alpha$, the function $x \mapsto f(x) / a$ is uniformly continuous.

uniformContinuous_div_const theorem

(a : α) : UniformContinuous fun b : α => b / a

Full source

@[to_additive]
theorem uniformContinuous_div_const (a : α) : UniformContinuous fun b : α => b / a :=
  uniformContinuous_id.div_const _

Uniform Continuity of Right Division by a Constant in Uniform Groups

Informal description

For any element $a$ in a uniform group $\alpha$, the right division function $b \mapsto b / a$ is uniformly continuous.

UniformContinuous.pow_const theorem

[UniformSpace β] {f : β → α} (hf : UniformContinuous f) : ∀ n : ℕ, UniformContinuous fun x => f x ^ n

Full source

@[to_additive UniformContinuous.const_nsmul]
theorem UniformContinuous.pow_const [UniformSpace β] {f : β → α} (hf : UniformContinuous f) :
    ∀ n : ℕ, UniformContinuous fun x => f x ^ n
  | 0 => by
    simp_rw [pow_zero]
    exact uniformContinuous_const
  | n + 1 => by
    simp_rw [pow_succ']
    exact hf.mul (hf.pow_const n)

Uniform continuity of power functions in uniform groups

Informal description

Let $\alpha$ be a uniform group and $\beta$ be a uniform space. For any uniformly continuous function $f \colon \beta \to \alpha$ and any natural number $n$, the function $x \mapsto (f(x))^n$ is uniformly continuous.

uniformContinuous_pow_const theorem

(n : ℕ) : UniformContinuous fun x : α => x ^ n

Full source

@[to_additive uniformContinuous_const_nsmul]
theorem uniformContinuous_pow_const (n : ℕ) : UniformContinuous fun x : α => x ^ n :=
  uniformContinuous_id.pow_const n

Uniform continuity of power functions in uniform groups

Informal description

For any natural number $n$, the function $x \mapsto x^n$ is uniformly continuous on a uniform group $\alpha$.

UniformContinuous.zpow_const theorem

[UniformSpace β] {f : β → α} (hf : UniformContinuous f) : ∀ n : ℤ, UniformContinuous fun x => f x ^ n

Full source

@[to_additive UniformContinuous.const_zsmul]
theorem UniformContinuous.zpow_const [UniformSpace β] {f : β → α} (hf : UniformContinuous f) :
    ∀ n : ℤ, UniformContinuous fun x => f x ^ n
  | (n : ℕ) => by
    simp_rw [zpow_natCast]
    exact hf.pow_const _
  | Int.negSucc n => by
    simp_rw [zpow_negSucc]
    exact (hf.pow_const _).inv

Uniform continuity of integer power functions in uniform groups

Informal description

Let $\alpha$ be a uniform group and $\beta$ be a uniform space. For any uniformly continuous function $f \colon \beta \to \alpha$ and any integer $n$, the function $x \mapsto (f(x))^n$ is uniformly continuous.

uniformContinuous_zpow_const theorem

(n : ℤ) : UniformContinuous fun x : α => x ^ n

Full source

@[to_additive uniformContinuous_const_zsmul]
theorem uniformContinuous_zpow_const (n : ℤ) : UniformContinuous fun x : α => x ^ n :=
  uniformContinuous_id.zpow_const n

Uniform continuity of integer power functions in uniform groups

Informal description

For any integer $n$, the function $x \mapsto x^n$ is uniformly continuous on a uniform group $\alpha$.

IsUniformGroup.to_topologicalGroup instance

: IsTopologicalGroup α

Full source

@[to_additive]
instance (priority := 10) IsUniformGroup.to_topologicalGroup : IsTopologicalGroup α where
  continuous_mul := uniformContinuous_mul.continuous
  continuous_inv := uniformContinuous_inv.continuous

Uniform Groups are Topological Groups

Informal description

Every uniform group $\alpha$ is also a topological group. That is, the group operations (multiplication and inversion) are continuous with respect to the topology induced by the uniform structure on $\alpha$.

Prod.instIsUniformGroup instance

[UniformSpace β] [Group β] [IsUniformGroup β] : IsUniformGroup (α × β)

Full source

@[to_additive]
instance Prod.instIsUniformGroup [UniformSpace β] [Group β] [IsUniformGroup β] :
    IsUniformGroup (α × β) :=
  ⟨((uniformContinuous_fst.comp uniformContinuous_fst).div
          (uniformContinuous_fst.comp uniformContinuous_snd)).prodMk
      ((uniformContinuous_snd.comp uniformContinuous_fst).div
        (uniformContinuous_snd.comp uniformContinuous_snd))⟩

Product of Uniform Groups is a Uniform Group

Informal description

For any uniform groups $\alpha$ and $\beta$, the product group $\alpha \times \beta$ equipped with the product uniform space structure is also a uniform group. This means that the group operations (multiplication and inversion) on $\alpha \times \beta$ are uniformly continuous with respect to the product uniformity.

uniformity_translate_mul theorem

(a : α) : ((𝓤 α).map fun x : α × α => (x.1 * a, x.2 * a)) = 𝓤 α

Full source

@[to_additive]
theorem uniformity_translate_mul (a : α) : ((𝓤 α).map fun x : α × α => (x.1 * a, x.2 * a)) = 𝓤 α :=
  le_antisymm (uniformContinuous_id.mul uniformContinuous_const)
    (calc
      𝓤 α =
          ((𝓤 α).map fun x : α × α => (x.1 * a⁻¹, x.2 * a⁻¹)).map fun x : α × α =>
            (x.1 * a, x.2 * a) := by simp [Filter.map_map, Function.comp_def]
      _ ≤ (𝓤 α).map fun x : α × α => (x.1 * a, x.2 * a) :=
        Filter.map_mono (uniformContinuous_id.mul uniformContinuous_const)
      )

Invariance of Uniformity under Right Multiplication: $\mathfrak{U}(\alpha) = \{(x \cdot a, y \cdot a) \mid (x, y) \in \mathfrak{U}(\alpha)\}$

Informal description

For any element $a$ in a uniform group $\alpha$, the image of the uniformity filter $\mathfrak{U}(\alpha)$ under the map $(x, y) \mapsto (x \cdot a, y \cdot a)$ is equal to $\mathfrak{U}(\alpha)$ itself.

MulOpposite.instIsUniformGroup instance

: IsUniformGroup αᵐᵒᵖ

Full source

@[to_additive]
instance : IsUniformGroup αᵐᵒᵖ :=
  ⟨uniformContinuous_op.comp
      ((uniformContinuous_unop.comp uniformContinuous_snd).inv.mul <|
        uniformContinuous_unop.comp uniformContinuous_fst)⟩

Uniform Group Structure on the Multiplicative Opposite

Informal description

The multiplicative opposite $\alpha^{\mathrm{op}}$ of a uniform group $\alpha$ is also a uniform group, where the group operations (multiplication and inversion) are uniformly continuous with respect to the inherited uniform structure.

isUniformGroup_sInf theorem

{us : Set (UniformSpace β)} (h : ∀ u ∈ us, @IsUniformGroup β u _) : @IsUniformGroup β (sInf us) _

Full source

@[to_additive]
theorem isUniformGroup_sInf {us : Set (UniformSpace β)} (h : ∀ u ∈ us, @IsUniformGroup β u _) :
    @IsUniformGroup β (sInf us) _ :=
  @IsUniformGroup.mk β (_) _ <|
    uniformContinuous_sInf_rng.mpr fun u hu =>
      uniformContinuous_sInf_dom₂ hu hu (@IsUniformGroup.uniformContinuous_div β u _ (h u hu))

Infimum of Uniform Group Structures is Uniform Group

Informal description

Let $\beta$ be a group equipped with a set of uniform space structures $\{u_i\}_{i \in I}$ such that for each $u_i$, the group operations are uniformly continuous (i.e., $(\beta, u_i)$ is a uniform group). Then the infimum uniform space structure $\bigsqcap u_i$ on $\beta$ also makes $\beta$ a uniform group.

isUniformGroup_iInf theorem

 {ι : Sort*} {us' : ι → UniformSpace β} (h' : ∀ i, @IsUniformGroup β (us' i) _) : @IsUniformGroup β (⨅ i, us' i) _

Full source

@[to_additive]
theorem isUniformGroup_iInf {ι : Sort*} {us' : ι → UniformSpace β}
    (h' : ∀ i, @IsUniformGroup β (us' i) _) : @IsUniformGroup β (⨅ i, us' i) _ := by
  rw [← sInf_range]
  exact isUniformGroup_sInf (Set.forall_mem_range.mpr h')

Uniform Group Structure Preserved Under Infimum of Uniformities

Informal description

Let $\beta$ be a group and $\{u_i\}_{i \in \iota}$ be a family of uniform space structures on $\beta$ such that for each $i \in \iota$, the group operations are uniformly continuous with respect to $u_i$. Then the group operations are also uniformly continuous with respect to the infimum uniform space structure $\bigsqcap_{i \in \iota} u_i$ on $\beta$.

isUniformGroup_inf theorem

 {u₁ u₂ : UniformSpace β} (h₁ : @IsUniformGroup β u₁ _) (h₂ : @IsUniformGroup β u₂ _) : @IsUniformGroup β (u₁ ⊓ u₂) _

Full source

@[to_additive]
theorem isUniformGroup_inf {u₁ u₂ : UniformSpace β} (h₁ : @IsUniformGroup β u₁ _)
    (h₂ : @IsUniformGroup β u₂ _) : @IsUniformGroup β (u₁ ⊓ u₂) _ := by
  rw [inf_eq_iInf]
  refine isUniformGroup_iInf fun b => ?_
  cases b <;> assumption

Uniform Group Structure Preserved Under Infimum of Two Uniformities

Informal description

Let $\beta$ be a group equipped with two uniform space structures $u_1$ and $u_2$ such that the group operations (multiplication and inversion) are uniformly continuous with respect to both $u_1$ and $u_2$. Then the group operations are also uniformly continuous with respect to the infimum uniform space structure $u_1 \sqcap u_2$ on $\beta$.

uniformity_eq_comap_nhds_one theorem

: 𝓤 α = comap (fun x : α × α => x.2 / x.1) (𝓝 (1 : α))

Full source

@[to_additive]
theorem uniformity_eq_comap_nhds_one : 𝓤 α = comap (fun x : α × α => x.2 / x.1) (𝓝 (1 : α)) := by
  rw [nhds_eq_comap_uniformity, Filter.comap_comap]
  refine le_antisymm (Filter.map_le_iff_le_comap.1 ?_) ?_
  · intro s hs
    rcases mem_uniformity_of_uniformContinuous_invariant uniformContinuous_div hs with ⟨t, ht, hts⟩
    refine mem_map.2 (mem_of_superset ht ?_)
    rintro ⟨a, b⟩
    simpa [subset_def] using hts a b a
  · intro s hs
    rcases mem_uniformity_of_uniformContinuous_invariant uniformContinuous_mul hs with ⟨t, ht, hts⟩
    refine ⟨_, ht, ?_⟩
    rintro ⟨a, b⟩
    simpa [subset_def] using hts 1 (b / a) a

Uniformity as Preimage of Identity Neighborhood via Division

Informal description

For a uniform group $\alpha$, the uniformity $\mathfrak{U}(\alpha)$ is equal to the preimage of the neighborhood filter of the identity element $1 \in \alpha$ under the map $(x, y) \mapsto y / x$.

uniformity_eq_comap_nhds_one_swapped theorem

: 𝓤 α = comap (fun x : α × α => x.1 / x.2) (𝓝 (1 : α))

Full source

@[to_additive]
theorem uniformity_eq_comap_nhds_one_swapped :
    𝓤 α = comap (fun x : α × α => x.1 / x.2) (𝓝 (1 : α)) := by
  rw [← comap_swap_uniformity, uniformity_eq_comap_nhds_one, comap_comap]
  rfl

Uniformity as Preimage of Identity Neighborhood via Swapped Division

Informal description

For a uniform group $\alpha$, the uniformity $\mathfrak{U}(\alpha)$ is equal to the preimage of the neighborhood filter of the identity element $1 \in \alpha$ under the map $(x, y) \mapsto x / y$.

IsUniformGroup.ext theorem

 {G : Type*} [Group G] {u v : UniformSpace G} (hu : @IsUniformGroup G u _) (hv : @IsUniformGroup G v _)
  (h : @nhds _ u.toTopologicalSpace 1 = @nhds _ v.toTopologicalSpace 1) : u = v

Full source

@[to_additive]
theorem IsUniformGroup.ext {G : Type*} [Group G] {u v : UniformSpace G} (hu : @IsUniformGroup G u _)
    (hv : @IsUniformGroup G v _)
    (h : @nhds _ u.toTopologicalSpace 1 = @nhds _ v.toTopologicalSpace 1) : u = v :=
  UniformSpace.ext <| by
    rw [@uniformity_eq_comap_nhds_one _ u _ hu, @uniformity_eq_comap_nhds_one _ v _ hv, h]

Equality of Uniform Group Structures via Identity Neighborhoods

Informal description

Let $G$ be a group equipped with two uniform space structures $u$ and $v$ such that both $(G, u)$ and $(G, v)$ are uniform groups. If the neighborhood filters of the identity element $1 \in G$ coincide in the topologies induced by $u$ and $v$, then the uniform structures $u$ and $v$ are equal.

IsUniformGroup.ext_iff theorem

 {G : Type*} [Group G] {u v : UniformSpace G} (hu : @IsUniformGroup G u _) (hv : @IsUniformGroup G v _) :
  u = v ↔ @nhds _ u.toTopologicalSpace 1 = @nhds _ v.toTopologicalSpace 1

Full source

@[to_additive]
theorem IsUniformGroup.ext_iff {G : Type*} [Group G] {u v : UniformSpace G}
    (hu : @IsUniformGroup G u _) (hv : @IsUniformGroup G v _) :
    u = v ↔ @nhds _ u.toTopologicalSpace 1 = @nhds _ v.toTopologicalSpace 1 :=
  ⟨fun h => h ▸ rfl, hu.ext hv⟩

Equivalence of Uniform Group Structures via Identity Neighborhoods

Informal description

Let $G$ be a group equipped with two uniform space structures $u$ and $v$ such that both $(G, u)$ and $(G, v)$ are uniform groups. Then $u = v$ if and only if the neighborhood filters of the identity element $1 \in G$ coincide in the topologies induced by $u$ and $v$.

IsUniformGroup.uniformity_countably_generated theorem

[(𝓝 (1 : α)).IsCountablyGenerated] : (𝓤 α).IsCountablyGenerated

Full source

@[to_additive]
theorem IsUniformGroup.uniformity_countably_generated [(𝓝 (1 : α)).IsCountablyGenerated] :
    (𝓤 α).IsCountablyGenerated := by
  rw [uniformity_eq_comap_nhds_one]
  exact Filter.comap.isCountablyGenerated _ _

Countable Generation of Uniformity in Uniform Groups with Countably Generated Identity Neighborhood

Informal description

Let $\alpha$ be a uniform group. If the neighborhood filter of the identity element $1 \in \alpha$ is countably generated, then the uniformity filter $\mathfrak{U}(\alpha)$ is also countably generated.

uniformity_eq_comap_inv_mul_nhds_one theorem

: 𝓤 α = comap (fun x : α × α => x.1⁻¹ * x.2) (𝓝 (1 : α))

Full source

@[to_additive]
theorem uniformity_eq_comap_inv_mul_nhds_one :
    𝓤 α = comap (fun x : α × α => x.1⁻¹ * x.2) (𝓝 (1 : α)) := by
  rw [← comap_uniformity_mulOpposite, uniformity_eq_comap_nhds_one, ← op_one, ← comap_unop_nhds,
    comap_comap, comap_comap]
  simp [Function.comp_def]

Uniformity as Preimage of Identity Neighborhood via Left Multiplication by Inverse

Informal description

For a uniform group $\alpha$, the uniformity $\mathfrak{U}(\alpha)$ is equal to the preimage of the neighborhood filter of the identity element $1 \in \alpha$ under the map $(x, y) \mapsto x^{-1} y$.

uniformity_eq_comap_inv_mul_nhds_one_swapped theorem

: 𝓤 α = comap (fun x : α × α => x.2⁻¹ * x.1) (𝓝 (1 : α))

Full source

@[to_additive]
theorem uniformity_eq_comap_inv_mul_nhds_one_swapped :
    𝓤 α = comap (fun x : α × α => x.2⁻¹ * x.1) (𝓝 (1 : α)) := by
  rw [← comap_swap_uniformity, uniformity_eq_comap_inv_mul_nhds_one, comap_comap]
  rfl

Uniformity as Preimage of Identity Neighborhood via Right Multiplication by Inverse

Informal description

For a uniform group $\alpha$, the uniformity $\mathfrak{U}(\alpha)$ is equal to the preimage of the neighborhood filter of the identity element $1 \in \alpha$ under the map $(x, y) \mapsto y^{-1} x$.

Filter.HasBasis.uniformity_of_nhds_one theorem

 {ι} {p : ι → Prop} {U : ι → Set α} (h : (𝓝 (1 : α)).HasBasis p U) :
  (𝓤 α).HasBasis p fun i => {x : α × α | x.2 / x.1 ∈ U i}

Full source

@[to_additive]
theorem Filter.HasBasis.uniformity_of_nhds_one {ι} {p : ι → Prop} {U : ι → Set α}
    (h : (𝓝 (1 : α)).HasBasis p U) :
    (𝓤 α).HasBasis p fun i => { x : α × α | x.2 / x.1 ∈ U i } := by
  rw [uniformity_eq_comap_nhds_one]
  exact h.comap _

Uniformity Basis via Division in Uniform Groups

Informal description

Let $\alpha$ be a uniform group with identity element $1$, and let $\mathfrak{U}(\alpha)$ be its uniformity filter. Suppose the neighborhood filter $\mathfrak{N}(1)$ of $1$ has a basis $\{U_i\}_{i \in \iota}$ indexed by a type $\iota$ with a predicate $p : \iota \to \mathrm{Prop}$. Then the uniformity $\mathfrak{U}(\alpha)$ has a basis consisting of sets $\{(x,y) \in \alpha \times \alpha \mid y / x \in U_i\}$ for each $i \in \iota$ satisfying $p(i)$.

Filter.HasBasis.uniformity_of_nhds_one_inv_mul theorem

 {ι} {p : ι → Prop} {U : ι → Set α} (h : (𝓝 (1 : α)).HasBasis p U) :
  (𝓤 α).HasBasis p fun i => {x : α × α | x.1⁻¹ * x.2 ∈ U i}

Full source

@[to_additive]
theorem Filter.HasBasis.uniformity_of_nhds_one_inv_mul {ι} {p : ι → Prop} {U : ι → Set α}
    (h : (𝓝 (1 : α)).HasBasis p U) :
    (𝓤 α).HasBasis p fun i => { x : α × α | x.1⁻¹ * x.2 ∈ U i } := by
  rw [uniformity_eq_comap_inv_mul_nhds_one]
  exact h.comap _

Uniformity Basis via Left Multiplication by Inverse in Uniform Groups

Informal description

Let $\alpha$ be a uniform group with identity element $1$, and let $\mathfrak{N}(1)$ be the neighborhood filter of $1$. Suppose $\mathfrak{N}(1)$ has a basis $\{U_i\}_{i \in \iota}$ indexed by a type $\iota$ with a predicate $p : \iota \to \mathrm{Prop}$. Then the uniformity $\mathfrak{U}(\alpha)$ has a basis consisting of sets $\{(x,y) \in \alpha \times \alpha \mid x^{-1} y \in U_i\}$ for each $i \in \iota$ satisfying $p(i)$.

Filter.HasBasis.uniformity_of_nhds_one_swapped theorem

 {ι} {p : ι → Prop} {U : ι → Set α} (h : (𝓝 (1 : α)).HasBasis p U) :
  (𝓤 α).HasBasis p fun i => {x : α × α | x.1 / x.2 ∈ U i}

Full source

@[to_additive]
theorem Filter.HasBasis.uniformity_of_nhds_one_swapped {ι} {p : ι → Prop} {U : ι → Set α}
    (h : (𝓝 (1 : α)).HasBasis p U) :
    (𝓤 α).HasBasis p fun i => { x : α × α | x.1 / x.2 ∈ U i } := by
  rw [uniformity_eq_comap_nhds_one_swapped]
  exact h.comap _

Uniformity Basis via Swapped Division in Uniform Groups

Informal description

Let $\alpha$ be a uniform group with identity element $1$, and let $\mathfrak{N}(1)$ be the neighborhood filter of $1$. Suppose $\mathfrak{N}(1)$ has a basis $\{U_i\}_{i \in \iota}$ indexed by a type $\iota$ with a predicate $p : \iota \to \mathrm{Prop}$. Then the uniformity $\mathfrak{U}(\alpha)$ has a basis consisting of sets $\{(x,y) \in \alpha \times \alpha \mid x / y \in U_i\}$ for each $i \in \iota$ satisfying $p(i)$.

Filter.HasBasis.uniformity_of_nhds_one_inv_mul_swapped theorem

 {ι} {p : ι → Prop} {U : ι → Set α} (h : (𝓝 (1 : α)).HasBasis p U) :
  (𝓤 α).HasBasis p fun i => {x : α × α | x.2⁻¹ * x.1 ∈ U i}

Full source

@[to_additive]
theorem Filter.HasBasis.uniformity_of_nhds_one_inv_mul_swapped {ι} {p : ι → Prop} {U : ι → Set α}
    (h : (𝓝 (1 : α)).HasBasis p U) :
    (𝓤 α).HasBasis p fun i => { x : α × α | x.2⁻¹ * x.1 ∈ U i } := by
  rw [uniformity_eq_comap_inv_mul_nhds_one_swapped]
  exact h.comap _

Uniformity Basis via Right Multiplication by Inverse in Uniform Groups

Informal description

Let $\alpha$ be a uniform group with identity element $1$, and let $\mathfrak{N}(1)$ be the neighborhood filter of $1$. Suppose $\mathfrak{N}(1)$ has a basis $\{U_i\}_{i \in \iota}$ indexed by a type $\iota$ with a predicate $p : \iota \to \mathrm{Prop}$. Then the uniformity $\mathfrak{U}(\alpha)$ has a basis consisting of sets $\{(x,y) \in \alpha \times \alpha \mid y^{-1} x \in U_i\}$ for each $i \in \iota$ satisfying $p(i)$.

uniformContinuous_of_tendsto_one theorem

 {hom : Type*} [UniformSpace β] [Group β] [IsUniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β] {f : hom}
  (h : Tendsto f (𝓝 1) (𝓝 1)) : UniformContinuous f

Full source

@[to_additive]
theorem uniformContinuous_of_tendsto_one {hom : Type*} [UniformSpace β] [Group β] [IsUniformGroup β]
    [FunLike hom α β] [MonoidHomClass hom α β] {f : hom} (h : Tendsto f (𝓝 1) (𝓝 1)) :
    UniformContinuous f := by
  have :
    ((fun x : β × β => x.2 / x.1) ∘ fun x : α × α => (f x.1, f x.2)) = fun x : α × α =>
      f (x.2 / x.1) := by ext; simp only [Function.comp_apply, map_div]
  rw [UniformContinuous, uniformity_eq_comap_nhds_one α, uniformity_eq_comap_nhds_one β,
    tendsto_comap_iff, this]
  exact Tendsto.comp h tendsto_comap

Uniform Continuity of Monoid Homomorphisms via Tendency to Identity

Informal description

Let $\alpha$ and $\beta$ be uniform groups, and let $f \colon \alpha \to \beta$ be a monoid homomorphism. If $f$ tends to the identity element $1$ at the identity element $1$ (i.e., $\lim_{x \to 1} f(x) = 1$), then $f$ is uniformly continuous.

uniformContinuous_of_continuousAt_one theorem

 {hom : Type*} [UniformSpace β] [Group β] [IsUniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β] (f : hom)
  (hf : ContinuousAt f 1) : UniformContinuous f

Full source

/-- A group homomorphism (a bundled morphism of a type that implements `MonoidHomClass`) between
two uniform groups is uniformly continuous provided that it is continuous at one. See also
`continuous_of_continuousAt_one`. -/
@[to_additive "An additive group homomorphism (a bundled morphism of a type that implements
`AddMonoidHomClass`) between two uniform additive groups is uniformly continuous provided that it
is continuous at zero. See also `continuous_of_continuousAt_zero`."]
theorem uniformContinuous_of_continuousAt_one {hom : Type*} [UniformSpace β] [Group β]
    [IsUniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β]
    (f : hom) (hf : ContinuousAt f 1) :
    UniformContinuous f :=
  uniformContinuous_of_tendsto_one (by simpa using hf.tendsto)

Uniform Continuity of Monoid Homomorphisms via Continuity at Identity

Informal description

Let $\alpha$ and $\beta$ be uniform groups, and let $f \colon \alpha \to \beta$ be a monoid homomorphism. If $f$ is continuous at the identity element $1$ of $\alpha$, then $f$ is uniformly continuous.

MonoidHom.uniformContinuous_of_continuousAt_one theorem

[UniformSpace β] [Group β] [IsUniformGroup β] (f : α →* β) (hf : ContinuousAt f 1) : UniformContinuous f

Full source

@[to_additive]
theorem MonoidHom.uniformContinuous_of_continuousAt_one [UniformSpace β] [Group β]
    [IsUniformGroup β] (f : α →* β) (hf : ContinuousAt f 1) : UniformContinuous f :=
  _root_.uniformContinuous_of_continuousAt_one f hf

Uniform Continuity of Monoid Homomorphisms via Continuity at Identity

Informal description

Let $\alpha$ and $\beta$ be uniform groups, and let $f \colon \alpha \to \beta$ be a monoid homomorphism. If $f$ is continuous at the identity element $1$ of $\alpha$, then $f$ is uniformly continuous.

IsUniformGroup.uniformContinuous_iff_isOpen_ker theorem

 {hom : Type*} [UniformSpace β] [DiscreteTopology β] [Group β] [IsUniformGroup β] [FunLike hom α β]
  [MonoidHomClass hom α β] {f : hom} : UniformContinuous f ↔ IsOpen ((f : α →* β).ker : Set α)

Full source

/-- A homomorphism from a uniform group to a discrete uniform group is continuous if and only if
its kernel is open. -/
@[to_additive "A homomorphism from a uniform additive group to a discrete uniform additive group is
continuous if and only if its kernel is open."]
theorem IsUniformGroup.uniformContinuous_iff_isOpen_ker {hom : Type*} [UniformSpace β]
    [DiscreteTopology β] [Group β] [IsUniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β]
    {f : hom} :
    UniformContinuousUniformContinuous f ↔ IsOpen ((f : α →* β).ker : Set α) := by
  refine ⟨fun hf => ?_, fun hf => ?_⟩
  · apply (isOpen_discrete ({1} : Set β)).preimage hf.continuous
  · apply uniformContinuous_of_continuousAt_one
    rw [ContinuousAt, nhds_discrete β, map_one, tendsto_pure]
    exact hf.mem_nhds (map_one f)

Uniform Continuity Criterion for Homomorphisms to Discrete Groups via Open Kernel

Informal description

Let $\alpha$ be a uniform group and $\beta$ a discrete uniform group. A group homomorphism $f \colon \alpha \to \beta$ is uniformly continuous if and only if its kernel $\ker f$ is an open subset of $\alpha$.

uniformContinuous_monoidHom_of_continuous theorem

 {hom : Type*} [UniformSpace β] [Group β] [IsUniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β] {f : hom}
  (h : Continuous f) : UniformContinuous f

Full source

@[to_additive]
theorem uniformContinuous_monoidHom_of_continuous {hom : Type*} [UniformSpace β] [Group β]
    [IsUniformGroup β] [FunLike hom α β] [MonoidHomClass hom α β] {f : hom} (h : Continuous f) :
    UniformContinuous f :=
  uniformContinuous_of_tendsto_one <|
    suffices Tendsto f (𝓝 1) (𝓝 (f 1)) by rwa [map_one] at this
    h.tendsto 1

Uniform Continuity of Continuous Monoid Homomorphisms Between Uniform Groups

Informal description

Let $\alpha$ and $\beta$ be uniform groups, and let $f \colon \alpha \to \beta$ be a monoid homomorphism. If $f$ is continuous, then $f$ is uniformly continuous.

IsTopologicalGroup.toUniformSpace definition

: UniformSpace G

Full source

/-- The right uniformity on a topological group (as opposed to the left uniformity).

Warning: in general the right and left uniformities do not coincide and so one does not obtain a
`IsUniformGroup` structure. Two important special cases where they _do_ coincide are for
commutative groups (see `comm_topologicalGroup_is_uniform`) and for compact groups (see
`topologicalGroup_is_uniform_of_compactSpace`). -/
@[to_additive "The right uniformity on a topological additive group (as opposed to the left
uniformity).

Warning: in general the right and left uniformities do not coincide and so one does not obtain a
`IsUniformAddGroup` structure. Two important special cases where they _do_ coincide are for
commutative additive groups (see `comm_topologicalAddGroup_is_uniform`) and for compact
additive groups (see `topologicalAddGroup_is_uniform_of_compactSpace`)."]
def IsTopologicalGroup.toUniformSpace : UniformSpace G where
  uniformity := comap (fun p : G × G => p.2 / p.1) (𝓝 1)
  symm :=
    have : Tendsto (fun p : G × G ↦ (p.2 / p.1)⁻¹) (comap (fun p : G × G ↦ p.2 / p.1) (𝓝 1))
      (𝓝 1⁻¹) := tendsto_id.inv.comp tendsto_comap
    by simpa [tendsto_comap_iff]
  comp := Tendsto.le_comap fun U H ↦ by
    rcases exists_nhds_one_split H with ⟨V, V_nhds, V_mul⟩
    refine mem_map.2 (mem_of_superset (mem_lift' <| preimage_mem_comap V_nhds) ?_)
    rintro ⟨x, y⟩ ⟨z, hz₁, hz₂⟩
    simpa using V_mul _ hz₂ _ hz₁
  nhds_eq_comap_uniformity _ := by simp only [comap_comap, Function.comp_def, nhds_translation_div]

Right uniformity on a topological group

Informal description

The right uniformity on a topological group $G$ is defined as the uniformity induced by the filter $\text{comap} (p \mapsto p_2 / p_1) (\mathcal{N}(1))$, where $\mathcal{N}(1)$ is the neighborhood filter of the identity element $1$ in $G$. This uniformity satisfies the symmetry and composition properties required for a uniform space structure. The topology induced by this uniformity coincides with the original topology of the group.

uniformity_eq_comap_nhds_one' theorem

: 𝓤 G = comap (fun p : G × G => p.2 / p.1) (𝓝 (1 : G))

Full source

@[to_additive]
theorem uniformity_eq_comap_nhds_one' : 𝓤 G = comap (fun p : G × G => p.2 / p.1) (𝓝 (1 : G)) :=
  rfl

Uniformity as Pullback of Identity Neighborhoods in a Topological Group

Informal description

For a topological group $G$ with identity element $1$, the uniformity $\mathfrak{U}(G)$ is equal to the filter obtained by pulling back the neighborhood filter $\mathcal{N}(1)$ along the map $(x, y) \mapsto y / x$ from $G \times G$ to $G$.

isUniformGroup_of_commGroup theorem

: IsUniformGroup G

Full source

@[to_additive]
theorem isUniformGroup_of_commGroup : IsUniformGroup G := by
  constructor
  simp only [UniformContinuous, uniformity_prod_eq_prod, uniformity_eq_comap_nhds_one',
    tendsto_comap_iff, tendsto_map'_iff, prod_comap_comap_eq, Function.comp_def,
    div_div_div_comm _ (Prod.snd (Prod.snd _)), ← nhds_prod_eq, Prod.mk_one_one]
  exact (continuous_div'.tendsto' 1 1 (div_one 1)).comp tendsto_comap

Commutative Topological Groups are Uniform Groups

Informal description

Every commutative topological group $G$ is a uniform group, meaning that the group operations (multiplication and inversion) are uniformly continuous with respect to the canonical uniformity induced by the topology on $G$.

IsUniformGroup.toUniformSpace_eq theorem

{G : Type*} [u : UniformSpace G] [Group G] [IsUniformGroup G] : IsTopologicalGroup.toUniformSpace G = u

Full source

@[to_additive]
theorem IsUniformGroup.toUniformSpace_eq {G : Type*} [u : UniformSpace G] [Group G]
    [IsUniformGroup G] : IsTopologicalGroup.toUniformSpace G = u := by
  ext : 1
  rw [uniformity_eq_comap_nhds_one' G, uniformity_eq_comap_nhds_one G]

Equality of Canonical and Given Uniformities in a Uniform Group

Informal description

For any group $G$ equipped with a uniform space structure $u$ that makes it a uniform group, the canonical uniformity induced by the topological group structure on $G$ coincides with $u$.

tendsto_div_comap_self theorem

 (de : IsDenseInducing e) (x₀ : α) :
  Tendsto (fun t : β × β => t.2 / t.1) ((comap fun p : β × β => (e p.1, e p.2)) <| 𝓝 (x₀, x₀)) (𝓝 1)

Full source

@[to_additive]
theorem tendsto_div_comap_self (de : IsDenseInducing e) (x₀ : α) :
    Tendsto (fun t : β × β => t.2 / t.1) ((comap fun p : β × β => (e p.1, e p.2)) <| 𝓝 (x₀, x₀))
      (𝓝 1) := by
  have comm : ((fun x : α × α => x.2 / x.1) ∘ fun t : β × β => (e t.1, e t.2)) =
      e ∘ fun t : β × β => t.2 / t.1 := by
    ext t
    simp
  have lim : Tendsto (fun x : α × α => x.2 / x.1) (𝓝 (x₀, x₀)) (𝓝 (e 1)) := by
    simpa using (continuous_div'.comp (@continuous_swap α α _ _)).tendsto (x₀, x₀)
  simpa using de.tendsto_comap_nhds_nhds lim comm

Limit of Division under Dense Inducing Maps: $(y, x) \mapsto y / x \to 1$ as $(x, y) \to (x_0, x_0)$

Informal description

Let $e \colon \alpha \to \beta$ be a dense inducing map between topological groups. For any point $x_0 \in \alpha$, the function $(y, x) \mapsto y / x$ tends to the identity element $1$ as $(x, y)$ tends to $(x_0, x_0)$ in the topology induced by $e$ on $\beta \times \beta$.

Mathlib.Topology.Algebra.IsUniformGroup.Defs

Main declarations

Main results