Mathlib.Topology.Algebra.IsUniformGroup.Basic

Pi.instIsUniformGroup instance

 {ι : Type*} {G : ι → Type*} [∀ i, UniformSpace (G i)] [∀ i, Group (G i)] [∀ i, IsUniformGroup (G i)] :
  IsUniformGroup (∀ i, G i)

Full source

@[to_additive]
instance Pi.instIsUniformGroup {ι : Type*} {G : ι → Type*} [∀ i, UniformSpace (G i)]
    [∀ i, Group (G i)] [∀ i, IsUniformGroup (G i)] : IsUniformGroup (∀ i, G i) where
  uniformContinuous_div := uniformContinuous_pi.mpr fun i ↦
    (uniformContinuous_proj G i).comp uniformContinuous_fst |>.div <|
      (uniformContinuous_proj G i).comp uniformContinuous_snd

Uniform Group Structure on Product of Uniform Groups

Informal description

For any family of uniform groups $\{G_i\}_{i \in \iota}$ (i.e., each $G_i$ is a group equipped with a uniform space structure such that multiplication and inversion are uniformly continuous), the product group $\prod_{i \in \iota} G_i$ is also a uniform group with the product uniform space structure and pointwise group operations.

isUniformEmbedding_translate_mul theorem

(a : α) : IsUniformEmbedding fun x : α => x * a

Full source

@[to_additive]
theorem isUniformEmbedding_translate_mul (a : α) : IsUniformEmbedding fun x : α => x * a :=
  { comap_uniformity := by
      nth_rw 1 [← uniformity_translate_mul a, comap_map]
      rintro ⟨p₁, p₂⟩ ⟨q₁, q₂⟩
      simp only [Prod.mk.injEq, mul_left_inj, imp_self]
    injective := mul_left_injective a }

Right Multiplication is a Uniform Embedding in a Uniform Group

Informal description

For any element $a$ in a uniform group $\alpha$, the right multiplication map $x \mapsto x \cdot a$ is a uniform embedding. That is, it is injective, uniformly continuous, and the uniformity on $\alpha$ is induced by the map from the uniformity on $\alpha$.

IsUniformGroup.cauchy_iff_tendsto theorem

(𝓕 : Filter G) : Cauchy 𝓕 ↔ NeBot 𝓕 ∧ Tendsto (fun p ↦ p.1 / p.2) (𝓕 ×ˢ 𝓕) (𝓝 1)

Full source

@[to_additive]
lemma cauchy_iff_tendsto (𝓕 : Filter G) :
    CauchyCauchy 𝓕 ↔ NeBot 𝓕 ∧ Tendsto (fun p ↦ p.1 / p.2) (𝓕 ×ˢ 𝓕) (𝓝 1) := by
  simp [Cauchy, uniformity_eq_comap_nhds_one_swapped, ← tendsto_iff_comap]

Characterization of Cauchy Filters in Uniform Groups via Division

Informal description

A filter $\mathcal{F}$ on a uniform group $G$ is Cauchy if and only if $\mathcal{F}$ is non-trivial and the map $(x, y) \mapsto x / y$ tends to the identity element $1$ along the product filter $\mathcal{F} \times \mathcal{F}$.

IsUniformGroup.cauchy_iff_tendsto_swapped theorem

(𝓕 : Filter G) : Cauchy 𝓕 ↔ NeBot 𝓕 ∧ Tendsto (fun p ↦ p.2 / p.1) (𝓕 ×ˢ 𝓕) (𝓝 1)

Full source

@[to_additive]
lemma cauchy_iff_tendsto_swapped (𝓕 : Filter G) :
    CauchyCauchy 𝓕 ↔ NeBot 𝓕 ∧ Tendsto (fun p ↦ p.2 / p.1) (𝓕 ×ˢ 𝓕) (𝓝 1) := by
  simp [Cauchy, uniformity_eq_comap_nhds_one, ← tendsto_iff_comap]

Characterization of Cauchy Filters in Uniform Groups via Division

Informal description

For a filter $\mathcal{F}$ on a uniform group $G$, $\mathcal{F}$ is a Cauchy filter if and only if $\mathcal{F}$ is non-trivial and the function $(x,y) \mapsto y / x$ tends to the identity element $1$ along the product filter $\mathcal{F} \times \mathcal{F}$.

IsUniformGroup.cauchy_map_iff_tendsto theorem

 (𝓕 : Filter ι) (f : ι → G) : Cauchy (map f 𝓕) ↔ NeBot 𝓕 ∧ Tendsto (fun p ↦ f p.1 / f p.2) (𝓕 ×ˢ 𝓕) (𝓝 1)

Full source

@[to_additive]
lemma cauchy_map_iff_tendsto (𝓕 : Filter ι) (f : ι → G) :
    CauchyCauchy (map f 𝓕) ↔ NeBot 𝓕 ∧ Tendsto (fun p ↦ f p.1 / f p.2) (𝓕 ×ˢ 𝓕) (𝓝 1) := by
  simp [cauchy_map_iff, uniformity_eq_comap_nhds_one_swapped, Function.comp_def]

Cauchy Criterion for Mapped Filters in Uniform Groups via Division

Informal description

Let $G$ be a uniform group and $\iota$ be an index type. For any filter $\mathcal{F}$ on $\iota$ and any function $f \colon \iota \to G$, the filter $\text{map } f \mathcal{F}$ is Cauchy if and only if $\mathcal{F}$ is non-trivial and the function $(p_1, p_2) \mapsto f(p_1) / f(p_2)$ tends to the identity element $1$ along the filter $\mathcal{F} \times \mathcal{F}$.

IsUniformGroup.cauchy_map_iff_tendsto_swapped theorem

 (𝓕 : Filter ι) (f : ι → G) : Cauchy (map f 𝓕) ↔ NeBot 𝓕 ∧ Tendsto (fun p ↦ f p.2 / f p.1) (𝓕 ×ˢ 𝓕) (𝓝 1)

Full source

@[to_additive]
lemma cauchy_map_iff_tendsto_swapped (𝓕 : Filter ι) (f : ι → G) :
    CauchyCauchy (map f 𝓕) ↔ NeBot 𝓕 ∧ Tendsto (fun p ↦ f p.2 / f p.1) (𝓕 ×ˢ 𝓕) (𝓝 1) := by
  simp [cauchy_map_iff, uniformity_eq_comap_nhds_one, Function.comp_def]

Cauchy Criterion for Uniform Groups via Swapped Division

Informal description

Let $G$ be a group equipped with a uniform space structure making it a uniform group, and let $\iota$ be an index type. For any filter $\mathcal{F}$ on $\iota$ and any function $f \colon \iota \to G$, the filter $\text{map } f \mathcal{F}$ is a Cauchy filter if and only if $\mathcal{F}$ is non-trivial and the function $(p_1, p_2) \mapsto f(p_2) / f(p_1)$ tends to the identity element $1$ along the filter $\mathcal{F} \times \mathcal{F}$.

IsUniformInducing.isUniformGroup theorem

 {γ : Type*} [Group γ] [UniformSpace γ] [IsUniformGroup γ] [UniformSpace β] {F : Type*} [FunLike F β γ]
  [MonoidHomClass F β γ] (f : F) (hf : IsUniformInducing f) : IsUniformGroup β

Full source

@[to_additive]
lemma IsUniformInducing.isUniformGroup {γ : Type*} [Group γ] [UniformSpace γ] [IsUniformGroup γ]
    [UniformSpace β] {F : Type*} [FunLike F β γ] [MonoidHomClass F β γ]
    (f : F) (hf : IsUniformInducing f) :
    IsUniformGroup β where
  uniformContinuous_div := by
    simp_rw [hf.uniformContinuous_iff, Function.comp_def, map_div]
    exact uniformContinuous_div.comp (hf.uniformContinuous.prodMap hf.uniformContinuous)

Uniform Group Structure Induced by a Uniform Inducing Monoid Homomorphism

Informal description

Let $\gamma$ be a group equipped with a uniform space structure making it a uniform group, and let $\beta$ be another uniform space. Given a monoid homomorphism $f \colon \beta \to \gamma$ that is uniform inducing, the group $\beta$ inherits a uniform group structure from $\gamma$ via $f$.

IsUniformGroup.comap theorem

 {γ : Type*} [Group γ] {u : UniformSpace γ} [IsUniformGroup γ] {F : Type*} [FunLike F β γ] [MonoidHomClass F β γ]
  (f : F) : @IsUniformGroup β (u.comap f) _

Full source

@[to_additive]
protected theorem IsUniformGroup.comap {γ : Type*} [Group γ] {u : UniformSpace γ} [IsUniformGroup γ]
    {F : Type*} [FunLike F β γ] [MonoidHomClass F β γ] (f : F) : @IsUniformGroup β (u.comap f) _ :=
  letI : UniformSpace β := u.comap f; IsUniformInducing.isUniformGroup f ⟨rfl⟩

Pullback Uniform Group Structure via Monoid Homomorphism

Informal description

Let $\gamma$ be a group equipped with a uniform space structure that makes it a uniform group, and let $F$ be a type of homomorphisms from $\beta$ to $\gamma$ that preserve the monoid structure. Given a homomorphism $f \colon \beta \to \gamma$ in $F$, the group $\beta$ equipped with the pullback uniform space structure induced by $f$ is a uniform group.

Subgroup.isUniformGroup instance

(S : Subgroup α) : IsUniformGroup S

Full source

@[to_additive]
instance isUniformGroup (S : Subgroup α) : IsUniformGroup S := .comap S.subtype

Uniform Group Structure on Subgroups

Informal description

For any subgroup $S$ of a uniform group $\alpha$, the subgroup $S$ inherits a uniform group structure from $\alpha$.

CauchySeq.mul theorem

{ι : Type*} [Preorder ι] {u v : ι → α} (hu : CauchySeq u) (hv : CauchySeq v) : CauchySeq (u * v)

Full source

@[to_additive]
theorem CauchySeq.mul {ι : Type*} [Preorder ι] {u v : ι → α} (hu : CauchySeq u)
    (hv : CauchySeq v) : CauchySeq (u * v) :=
  uniformContinuous_mul.comp_cauchySeq (hu.prodMk hv)

Product of Cauchy Sequences in a Uniform Group is Cauchy

Informal description

Let $\alpha$ be a uniform group and $\iota$ a preorder. For any two Cauchy sequences $u, v \colon \iota \to \alpha$, the pointwise product sequence $n \mapsto u(n) \cdot v(n)$ is also a Cauchy sequence.

CauchySeq.mul_const theorem

{ι : Type*} [Preorder ι] {u : ι → α} {x : α} (hu : CauchySeq u) : CauchySeq fun n => u n * x

Full source

@[to_additive]
theorem CauchySeq.mul_const {ι : Type*} [Preorder ι] {u : ι → α} {x : α} (hu : CauchySeq u) :
    CauchySeq fun n => u n * x :=
  (uniformContinuous_id.mul uniformContinuous_const).comp_cauchySeq hu

Right Multiplication Preserves Cauchy Sequences in Uniform Groups

Informal description

Let $\alpha$ be a uniform group and $\iota$ be a preorder. For any Cauchy sequence $u \colon \iota \to \alpha$ and any fixed element $x \in \alpha$, the sequence defined by $n \mapsto u_n \cdot x$ is also a Cauchy sequence.

CauchySeq.const_mul theorem

{ι : Type*} [Preorder ι] {u : ι → α} {x : α} (hu : CauchySeq u) : CauchySeq fun n => x * u n

Full source

@[to_additive]
theorem CauchySeq.const_mul {ι : Type*} [Preorder ι] {u : ι → α} {x : α} (hu : CauchySeq u) :
    CauchySeq fun n => x * u n :=
  (uniformContinuous_const.mul uniformContinuous_id).comp_cauchySeq hu

Left Multiplication by a Constant Preserves Cauchy Sequences in Uniform Groups

Informal description

Let $\alpha$ be a uniform group, $\iota$ a preorder, and $u \colon \iota \to \alpha$ a Cauchy sequence. For any fixed element $x \in \alpha$, the sequence $n \mapsto x \cdot u(n)$ is also a Cauchy sequence.

CauchySeq.inv theorem

{ι : Type*} [Preorder ι] {u : ι → α} (h : CauchySeq u) : CauchySeq u⁻¹

Full source

@[to_additive]
theorem CauchySeq.inv {ι : Type*} [Preorder ι] {u : ι → α} (h : CauchySeq u) :
    CauchySeq u⁻¹ :=
  uniformContinuous_inv.comp_cauchySeq h

Inversion Preserves Cauchy Sequences in Uniform Groups

Informal description

Let $\alpha$ be a uniform group, $\iota$ a preorder, and $u \colon \iota \to \alpha$ a Cauchy sequence. Then the sequence of inverses $u^{-1} \colon \iota \to \alpha$ defined by $n \mapsto (u(n))^{-1}$ is also a Cauchy sequence.

totallyBounded_iff_subset_finite_iUnion_nhds_one theorem

{s : Set α} : TotallyBounded s ↔ ∀ U ∈ 𝓝 (1 : α), ∃ t : Set α, t.Finite ∧ s ⊆ ⋃ y ∈ t, y • U

Full source

@[to_additive]
theorem totallyBounded_iff_subset_finite_iUnion_nhds_one {s : Set α} :
    TotallyBoundedTotallyBounded s ↔ ∀ U ∈ 𝓝 (1 : α), ∃ t : Set α, t.Finite ∧ s ⊆ ⋃ y ∈ t, y • U :=
  (𝓝 (1 : α)).basis_sets.uniformity_of_nhds_one_inv_mul_swapped.totallyBounded_iff.trans <| by
    simp [← preimage_smul_inv, preimage]

Characterization of totally bounded sets via finite covers by translates of identity neighborhoods

Informal description

A subset $s$ of a uniform group $\alpha$ is totally bounded if and only if for every neighborhood $U$ of the identity element $1 \in \alpha$, there exists a finite subset $t \subseteq \alpha$ such that $s$ is contained in the union of the left translates $y \cdot U$ for all $y \in t$.

totallyBounded_inv theorem

{s : Set α} (hs : TotallyBounded s) : TotallyBounded (s⁻¹)

Full source

@[to_additive]
theorem totallyBounded_inv {s : Set α} (hs : TotallyBounded s) : TotallyBounded (s⁻¹) := by
  convert TotallyBounded.image hs uniformContinuous_inv
  aesop

Inversion Preserves Total Boundedness in Uniform Groups

Informal description

Let $\alpha$ be a uniform group and $s \subseteq \alpha$ a totally bounded subset. Then the set of inverses $s^{-1} = \{x^{-1} \mid x \in s\}$ is also totally bounded.

TendstoUniformlyOnFilter.mul theorem

 (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') :
  TendstoUniformlyOnFilter (f * f') (g * g') l l'

Full source

@[to_additive]
theorem TendstoUniformlyOnFilter.mul (hf : TendstoUniformlyOnFilter f g l l')
    (hf' : TendstoUniformlyOnFilter f' g' l l') : TendstoUniformlyOnFilter (f * f') (g * g') l l' :=
  fun u hu =>
  ((uniformContinuous_mul.comp_tendstoUniformlyOnFilter (hf.prodMk hf')) u hu).diag_of_prod_left

Uniform Convergence of Pointwise Multiplication on a Filter

Informal description

Let $\alpha$ be a topological space and $\beta$ be a uniform group. Given two families of functions $f_n, f'_n \colon \alpha \to \beta$ indexed by $n \in \iota$ that converge uniformly on a filter $l'$ to functions $g, g' \colon \alpha \to \beta$ respectively, with respect to a filter $l$ on $\iota$, then the family of pointwise multiplication functions $(f_n \cdot f'_n)$ converges uniformly on $l'$ to $g \cdot g'$ with respect to $l$.

TendstoUniformlyOnFilter.div theorem

 (hf : TendstoUniformlyOnFilter f g l l') (hf' : TendstoUniformlyOnFilter f' g' l l') :
  TendstoUniformlyOnFilter (f / f') (g / g') l l'

Full source

@[to_additive]
theorem TendstoUniformlyOnFilter.div (hf : TendstoUniformlyOnFilter f g l l')
    (hf' : TendstoUniformlyOnFilter f' g' l l') : TendstoUniformlyOnFilter (f / f') (g / g') l l' :=
  fun u hu =>
  ((uniformContinuous_div.comp_tendstoUniformlyOnFilter (hf.prodMk hf')) u hu).diag_of_prod_left

Uniform Convergence of Pointwise Division on a Filter

Informal description

Let $\alpha$ be a topological space and $\beta$ be a uniform group. Given two families of functions $f_n, f'_n \colon \alpha \to \beta$ indexed by $n \in \iota$ that converge uniformly on a filter $l'$ to functions $g, g' \colon \alpha \to \beta$ respectively, with respect to a filter $l$ on $\iota$, then the family of pointwise division functions $(f_n / f'_n)$ converges uniformly on $l'$ to $g / g'$ with respect to $l$.

TendstoUniformlyOn.mul theorem

(hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) : TendstoUniformlyOn (f * f') (g * g') l s

Full source

@[to_additive]
theorem TendstoUniformlyOn.mul (hf : TendstoUniformlyOn f g l s)
    (hf' : TendstoUniformlyOn f' g' l s) : TendstoUniformlyOn (f * f') (g * g') l s := fun u hu =>
  ((uniformContinuous_mul.comp_tendstoUniformlyOn (hf.prodMk hf')) u hu).diag_of_prod

Uniform Convergence of Pointwise Multiplication on a Set

Informal description

Let $\alpha$ be a topological space and $\beta$ be a uniform group. Given two families of functions $f_n, f'_n \colon \alpha \to \beta$ indexed by $n \in \iota$ that converge uniformly on a set $s \subseteq \alpha$ to functions $g, g' \colon \alpha \to \beta$ respectively with respect to a filter $l$ on $\iota$, then the family of pointwise products $(f_n \cdot f'_n)$ converges uniformly on $s$ to $g \cdot g'$ with respect to $l$.

TendstoUniformlyOn.div theorem

(hf : TendstoUniformlyOn f g l s) (hf' : TendstoUniformlyOn f' g' l s) : TendstoUniformlyOn (f / f') (g / g') l s

Full source

@[to_additive]
theorem TendstoUniformlyOn.div (hf : TendstoUniformlyOn f g l s)
    (hf' : TendstoUniformlyOn f' g' l s) : TendstoUniformlyOn (f / f') (g / g') l s := fun u hu =>
  ((uniformContinuous_div.comp_tendstoUniformlyOn (hf.prodMk hf')) u hu).diag_of_prod

Uniform Convergence of Pointwise Division on a Set

Informal description

Let $\alpha$ be a topological space and $\beta$ be a uniform group. Given two families of functions $f_n, f'_n \colon \alpha \to \beta$ indexed by $n \in \iota$ that converge uniformly on a set $s \subseteq \alpha$ to functions $g, g' \colon \alpha \to \beta$ respectively with respect to a filter $l$ on $\iota$, then the family of pointwise divisions $(f_n / f'_n)$ converges uniformly on $s$ to $g / g'$ with respect to $l$.

TendstoUniformly.mul theorem

(hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) : TendstoUniformly (f * f') (g * g') l

Full source

@[to_additive]
theorem TendstoUniformly.mul (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) :
    TendstoUniformly (f * f') (g * g') l := fun u hu =>
  ((uniformContinuous_mul.comp_tendstoUniformly (hf.prodMk hf')) u hu).diag_of_prod

Uniform convergence is preserved under pointwise multiplication in uniform groups

Informal description

Let $\alpha$ be a topological space and $\beta$ be a uniform group. Given two families of functions $f_n, f'_n \colon \alpha \to \beta$ indexed by $n \in \iota$ that converge uniformly to functions $g, g' \colon \alpha \to \beta$ respectively with respect to a filter $l$ on $\iota$, then the family of pointwise products $(f_n \cdot f'_n)$ converges uniformly to $g \cdot g'$ with respect to $l$.

TendstoUniformly.div theorem

(hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) : TendstoUniformly (f / f') (g / g') l

Full source

@[to_additive]
theorem TendstoUniformly.div (hf : TendstoUniformly f g l) (hf' : TendstoUniformly f' g' l) :
    TendstoUniformly (f / f') (g / g') l := fun u hu =>
  ((uniformContinuous_div.comp_tendstoUniformly (hf.prodMk hf')) u hu).diag_of_prod

Uniform convergence is preserved under pointwise division in uniform groups

Informal description

Let $\alpha$ be a topological space, $\beta$ be a uniform group, and $f, f', g, g' \colon \alpha \to \beta$ be functions. If $f$ converges uniformly to $g$ and $f'$ converges uniformly to $g'$ with respect to a filter $l$ on the index set, then the pointwise division $f / f'$ converges uniformly to $g / g'$ with respect to the same filter $l$.

UniformCauchySeqOn.mul theorem

(hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) : UniformCauchySeqOn (f * f') l s

Full source

@[to_additive]
theorem UniformCauchySeqOn.mul (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) :
    UniformCauchySeqOn (f * f') l s := fun u hu => by
  simpa using (uniformContinuous_mul.comp_uniformCauchySeqOn (hf.prod' hf')) u hu

Uniform Cauchy property of pointwise product sequences on a common set

Informal description

Let $\alpha$ be a type, $\beta$ be a uniform group, and $f, f' \colon \alpha \to \beta$ be sequences of functions indexed by a common set. If both $f$ and $f'$ are uniformly Cauchy on a subset $s \subseteq \alpha$ with respect to a filter $l$ on the index set, then the pointwise product sequence $(f \cdot f')$ defined by $x \mapsto f(x) \cdot f'(x)$ is also uniformly Cauchy on $s$ with respect to $l$.

UniformCauchySeqOn.div theorem

(hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) : UniformCauchySeqOn (f / f') l s

Full source

@[to_additive]
theorem UniformCauchySeqOn.div (hf : UniformCauchySeqOn f l s) (hf' : UniformCauchySeqOn f' l s) :
    UniformCauchySeqOn (f / f') l s := fun u hu => by
  simpa using (uniformContinuous_div.comp_uniformCauchySeqOn (hf.prod' hf')) u hu

Uniform Cauchy Property of Pointwise Division Sequences on a Common Set

Informal description

Let $\alpha$ be a type, $\beta$ be a uniform group, $f, f' \colon \alpha \to \beta$ be sequences of functions, $l$ a filter on the index set, and $s \subseteq \alpha$. If both $f$ and $f'$ are uniformly Cauchy on $s$ with respect to $l$, then the pointwise division sequence $(f / f')$ defined by $x \mapsto f(x) / f'(x)$ is also uniformly Cauchy on $s$ with respect to $l$.

topologicalGroup_is_uniform_of_compactSpace theorem

[CompactSpace G] : IsUniformGroup G

Full source

@[to_additive]
theorem topologicalGroup_is_uniform_of_compactSpace [CompactSpace G] : IsUniformGroup G :=
  ⟨by
    apply CompactSpace.uniformContinuous_of_continuous
    exact continuous_div'⟩

Compact topological groups are uniform groups

Informal description

For any compact topological group $G$, the group operations (multiplication and inversion) are uniformly continuous with respect to the right uniformity on $G$. In other words, every compact topological group is a uniform group.

Subgroup.isClosed_of_discrete instance

[T2Space G] {H : Subgroup G} [DiscreteTopology H] : IsClosed (H : Set G)

Full source

@[to_additive]
instance Subgroup.isClosed_of_discrete [T2Space G] {H : Subgroup G} [DiscreteTopology H] :
    IsClosed (H : Set G) := by
  obtain ⟨V, V_in, VH⟩ : ∃ (V : Set G), V ∈ 𝓝 (1 : G) ∧ V ∩ (H : Set G) = {1} :=
    nhds_inter_eq_singleton_of_mem_discrete H.one_mem
  have : (fun p : G × G => p.2 / p.1) ⁻¹' V(fun p : G × G => p.2 / p.1) ⁻¹' V ∈ 𝓤 G := preimage_mem_comap V_in
  apply isClosed_of_spaced_out this
  intro h h_in h' h'_in
  contrapose!
  simp only [Set.mem_preimage, not_not]
  rintro (hyp : h' / h ∈ V)
  have : h' / h ∈ ({1} : Set G) := VH ▸ Set.mem_inter hyp (H.div_mem h'_in h_in)
  exact (eq_of_div_eq_one this).symm

Closedness of Discrete Subgroups in Hausdorff Topological Groups

Informal description

For any Hausdorff topological group $G$ and any subgroup $H$ of $G$ with the discrete topology, $H$ is a closed subset of $G$.

Subgroup.tendsto_coe_cofinite_of_discrete theorem

[T2Space G] (H : Subgroup G) [DiscreteTopology H] : Tendsto ((↑) : H → G) cofinite (cocompact _)

Full source

@[to_additive]
lemma Subgroup.tendsto_coe_cofinite_of_discrete [T2Space G] (H : Subgroup G) [DiscreteTopology H] :
    Tendsto ((↑) : H → G) cofinite (cocompact _) :=
  IsClosed.tendsto_coe_cofinite_of_discreteTopology inferInstance inferInstance

Cofinite-to-Cocompact Tendency for Discrete Subgroups in Hausdorff Topological Groups

Informal description

Let $G$ be a Hausdorff topological group and $H$ a subgroup of $G$ endowed with the discrete topology. Then the inclusion map $H \hookrightarrow G$ tends to the cocompact filter on $G$ along the cofinite filter on $H$. In other words, for any compact subset $K \subseteq G$, the set $\{h \in H \mid h \notin K\}$ is finite.

MonoidHom.tendsto_coe_cofinite_of_discrete theorem

 [T2Space G] {H : Type*} [Group H] {f : H →* G} (hf : Function.Injective f) (hf' : DiscreteTopology f.range) :
  Tendsto f cofinite (cocompact _)

Full source

@[to_additive]
lemma MonoidHom.tendsto_coe_cofinite_of_discrete [T2Space G] {H : Type*} [Group H] {f : H →* G}
    (hf : Function.Injective f) (hf' : DiscreteTopology f.range) :
    Tendsto f cofinite (cocompact _) := by
  replace hf : Function.Injective f.rangeRestrict := by simpa
  exact f.range.tendsto_coe_cofinite_of_discrete.comp hf.tendsto_cofinite

Cofinite-to-Cocompact Tendency for Discrete-Range Injective Group Homomorphisms in Hausdorff Topological Groups

Informal description

Let $G$ be a Hausdorff topological group and $H$ a group. Given an injective group homomorphism $f \colon H \to G$ such that the range of $f$ is a discrete subgroup of $G$, the function $f$ tends to the cocompact filter on $G$ along the cofinite filter on $H$. In other words, for any compact subset $K \subseteq G$, the set $\{h \in H \mid f(h) \notin K\}$ is finite.

IsTopologicalGroup.tendstoUniformly_iff theorem

 (F : ι → α → G) (f : α → G) (p : Filter ι) (hu : IsTopologicalGroup.toUniformSpace G = u) :
  TendstoUniformly F f p ↔ ∀ u ∈ 𝓝 (1 : G), ∀ᶠ i in p, ∀ a, F i a / f a ∈ u

Full source

@[to_additive]
theorem tendstoUniformly_iff (F : ι → α → G) (f : α → G) (p : Filter ι)
    (hu : IsTopologicalGroup.toUniformSpace G = u) :
    TendstoUniformlyTendstoUniformly F f p ↔ ∀ u ∈ 𝓝 (1 : G), ∀ᶠ i in p, ∀ a, F i a / f a ∈ u :=
  hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩,
    fun h _ ⟨u, hu, hv⟩ => mem_of_superset (h u hu) fun _ hi a => hv (hi a)⟩

Uniform Convergence Criterion for Functions into a Topological Group

Informal description

Let $G$ be a topological group with the right uniformity $u$. A family of functions $F_i : \alpha \to G$ indexed by $\iota$ converges uniformly to a function $f : \alpha \to G$ with respect to a filter $p$ on $\iota$ if and only if for every neighborhood $u$ of the identity element $1$ in $G$, there exists an event $N \in p$ such that for all $i \in N$ and all $a \in \alpha$, the quotient $F_i(a) / f(a)$ belongs to $u$.

IsTopologicalGroup.tendstoUniformlyOn_iff theorem

 (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α) (hu : IsTopologicalGroup.toUniformSpace G = u) :
  TendstoUniformlyOn F f p s ↔ ∀ u ∈ 𝓝 (1 : G), ∀ᶠ i in p, ∀ a ∈ s, F i a / f a ∈ u

Full source

@[to_additive]
theorem tendstoUniformlyOn_iff (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α)
    (hu : IsTopologicalGroup.toUniformSpace G = u) :
    TendstoUniformlyOnTendstoUniformlyOn F f p s ↔ ∀ u ∈ 𝓝 (1 : G), ∀ᶠ i in p, ∀ a ∈ s, F i a / f a ∈ u :=
  hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩,
    fun h _ ⟨u, hu, hv⟩ => mem_of_superset (h u hu) fun _ hi a ha => hv (hi a ha)⟩

Uniform Convergence on a Set in a Topological Group

Informal description

Let $G$ be a topological group with right uniformity $u$, and let $F_i : \alpha \to G$ be a family of functions indexed by $\iota$ converging to $f : \alpha \to G$ with respect to a filter $p$ on $\iota$. Then, $F_i$ converges uniformly to $f$ on a subset $s \subseteq \alpha$ if and only if for every neighborhood $u$ of the identity element $1 \in G$, there exists an event in $p$ such that for all indices $i$ in this event and all points $a \in s$, the ratio $F_i(a) / f(a)$ lies in $u$.

IsTopologicalGroup.tendstoLocallyUniformly_iff theorem

 [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (hu : IsTopologicalGroup.toUniformSpace G = u) :
  TendstoLocallyUniformly F f p ↔ ∀ u ∈ 𝓝 (1 : G), ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ i in p, ∀ a ∈ t, F i a / f a ∈ u

Full source

@[to_additive]
theorem tendstoLocallyUniformly_iff [TopologicalSpace α] (F : ι → α → G) (f : α → G)
    (p : Filter ι) (hu : IsTopologicalGroup.toUniformSpace G = u) :
    TendstoLocallyUniformlyTendstoLocallyUniformly F f p ↔
      ∀ u ∈ 𝓝 (1 : G), ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ i in p, ∀ a ∈ t, F i a / f a ∈ u :=
  hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩, fun h _ ⟨u, hu, hv⟩ x =>
    Exists.imp (fun _ ⟨h, hp⟩ => ⟨h, mem_of_superset hp fun _ hi a ha => hv (hi a ha)⟩)
      (h u hu x)⟩

Characterization of Locally Uniform Convergence in Topological Groups

Informal description

Let $G$ be a topological group with the right uniformity, and let $\alpha$ be a topological space. A family of functions $F_i \colon \alpha \to G$ converges locally uniformly to a function $f \colon \alpha \to G$ with respect to a filter $p$ on the index set $\iota$ if and only if for every neighborhood $u$ of the identity $1 \in G$ and every point $x \in \alpha$, there exists a neighborhood $t$ of $x$ such that for all indices $i$ eventually in $p$, the quotient $F_i(a) / f(a)$ lies in $u$ for all $a \in t$.

IsTopologicalGroup.tendstoLocallyUniformlyOn_iff theorem

 [TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α)
  (hu : IsTopologicalGroup.toUniformSpace G = u) :
  TendstoLocallyUniformlyOn F f p s ↔ ∀ u ∈ 𝓝 (1 : G), ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ i in p, ∀ a ∈ t, F i a / f a ∈ u

Full source

@[to_additive]
theorem tendstoLocallyUniformlyOn_iff [TopologicalSpace α] (F : ι → α → G) (f : α → G)
    (p : Filter ι) (s : Set α) (hu : IsTopologicalGroup.toUniformSpace G = u) :
    TendstoLocallyUniformlyOnTendstoLocallyUniformlyOn F f p s ↔
      ∀ u ∈ 𝓝 (1 : G), ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ i in p, ∀ a ∈ t, F i a / f a ∈ u :=
  hu ▸ ⟨fun h u hu => h _ ⟨u, hu, fun _ => id⟩, fun h _ ⟨u, hu, hv⟩ x =>
    (Exists.imp fun _ ⟨h, hp⟩ => ⟨h, mem_of_superset hp fun _ hi a ha => hv (hi a ha)⟩) ∘
      h u hu x⟩

Characterization of Locally Uniform Convergence on Topological Groups

Informal description

Let $G$ be a topological group with the right uniformity, and let $\alpha$ be a topological space. For a family of functions $F_n \colon \alpha \to G$, a function $f \colon \alpha \to G$, a filter $p$ on the index set, and a subset $s \subseteq \alpha$, the following are equivalent: 1. The sequence $F_n$ converges locally uniformly on $s$ to $f$ with respect to $p$. 2. For every neighborhood $u$ of the identity $1 \in G$ and every $x \in s$, there exists a neighborhood $t$ of $x$ in $s$ such that for all $n$ eventually in $p$, the difference $F_n(a) / f(a) \in u$ for all $a \in t$.

IsDenseInducing.extend_Z_bilin theorem

: Continuous (extend (de.prodMap df) (fun p : β × δ => φ p.1 p.2))

Full source

/-- Bourbaki GT III.6.5 Theorem I:
ℤ-bilinear continuous maps from dense images into a complete Hausdorff group extend by continuity.
Note: Bourbaki assumes that α and β are also complete Hausdorff, but this is not necessary. -/
theorem extend_Z_bilin : Continuous (extend (de.prodMap df) (fun p : β × δ => φ p.1 p.2)) := by
  refine continuous_extend_of_cauchy _ ?_
  rintro ⟨x₀, y₀⟩
  constructor
  · apply NeBot.map
    apply comap_neBot
    intro U h
    rcases mem_closure_iff_nhds.1 ((de.prodMap df).dense (x₀, y₀)) U h with ⟨x, x_in, ⟨z, z_x⟩⟩
    exists z
    aesop
  · suffices map (fun p : (β × δ) × β × δ => (fun p : β × δ => φ p.1 p.2) p.2 -
      (fun p : β × δ => φ p.1 p.2) p.1)
        (comap (fun p : (β × δ) × β × δ => ((e p.1.1, f p.1.2), (e p.2.1, f p.2.2)))
        (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀))) ≤ 𝓝 0 by
      rwa [uniformity_eq_comap_nhds_zero G, prod_map_map_eq, ← map_le_iff_le_comap, Filter.map_map,
        prod_comap_comap_eq]
    intro W' W'_nhd
    have key := extend_Z_bilin_key de df hφ W'_nhd x₀ y₀
    rcases key with ⟨U, U_nhd, V, V_nhd, h⟩
    rw [mem_comap] at U_nhd
    rcases U_nhd with ⟨U', U'_nhd, U'_sub⟩
    rw [mem_comap] at V_nhd
    rcases V_nhd with ⟨V', V'_nhd, V'_sub⟩
    rw [mem_map, mem_comap, nhds_prod_eq]
    exists (U' ×ˢ V') ×ˢ U' ×ˢ V'
    rw [mem_prod_same_iff]
    simp only [exists_prop]
    constructor
    · have := prod_mem_prod U'_nhd V'_nhd
      tauto
    · intro p h'
      simp only [Set.mem_preimage, Set.prodMk_mem_set_prod_eq] at h'
      rcases p with ⟨⟨x, y⟩, ⟨x', y'⟩⟩
      apply h <;> tauto

Continuous Extension Theorem for $\mathbb{Z}$-Bilinear Maps via Dense Subspaces

Informal description

Let $β$ and $δ$ be topological spaces with dense subspaces $α$ and $γ$ respectively, induced by dense inducing maps $e : α → β$ and $f : γ → δ$. Let $φ : β × δ → G$ be a $\mathbb{Z}$-bilinear continuous map into a complete Hausdorff additive commutative group $G$. Then the extension of $φ$ from $α × γ$ to $β × δ$ via the product map $e × f$ is continuous. More precisely, if $φ$ is continuous on $α × γ$ and $G$ is complete Hausdorff, then the unique continuous extension $\tilde{φ} : β × δ → G$ exists and is given by the limit construction through the dense subspaces.

QuotientGroup.completeSpace' instance

 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [FirstCountableTopology G] (N : Subgroup G)
  [N.Normal] [@CompleteSpace G (IsTopologicalGroup.toUniformSpace G)] :
  @CompleteSpace (G ⧸ N) (IsTopologicalGroup.toUniformSpace (G ⧸ N))

Full source

/-- The quotient `G ⧸ N` of a complete first countable topological group `G` by a normal subgroup
is itself complete. [N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b]

Because a topological group is not equipped with a `UniformSpace` instance by default, we must
explicitly provide it in order to consider completeness. See `QuotientGroup.completeSpace` for a
version in which `G` is already equipped with a uniform structure. -/
@[to_additive "The quotient `G ⧸ N` of a complete first countable topological additive group
`G` by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by
subspaces are complete. [N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b]

Because an additive topological group is not equipped with a `UniformSpace` instance by default,
we must explicitly provide it in order to consider completeness. See
`QuotientAddGroup.completeSpace` for a version in which `G` is already equipped with a uniform
structure."]
instance QuotientGroup.completeSpace' (G : Type u) [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] [FirstCountableTopology G] (N : Subgroup G) [N.Normal]
    [@CompleteSpace G (IsTopologicalGroup.toUniformSpace G)] :
    @CompleteSpace (G ⧸ N) (IsTopologicalGroup.toUniformSpace (G ⧸ N)) := by
  /- Since `G ⧸ N` is a topological group it is a uniform space, and since `G` is first countable
    the uniformities of both `G` and `G ⧸ N` are countably generated. Moreover, we may choose a
    sequential antitone neighborhood basis `u` for `𝓝 (1 : G)` so that `(u (n + 1)) ^ 2 ⊆ u n`, and
    this descends to an antitone neighborhood basis `v` for `𝓝 (1 : G ⧸ N)`. Since `𝓤 (G ⧸ N)` is
    countably generated, it suffices to show any Cauchy sequence `x` converges. -/
  letI : UniformSpace (G ⧸ N) := IsTopologicalGroup.toUniformSpace (G ⧸ N)
  letI : UniformSpace G := IsTopologicalGroup.toUniformSpace G
  haveI : (𝓤 (G ⧸ N)).IsCountablyGenerated := comap.isCountablyGenerated _ _
  obtain ⟨u, hu, u_mul⟩ := IsTopologicalGroup.exists_antitone_basis_nhds_one G
  obtain ⟨hv, v_anti⟩ := hu.map ((↑) : G → G ⧸ N)
  rw [← QuotientGroup.nhds_eq N 1, QuotientGroup.mk_one] at hv
  refine UniformSpace.complete_of_cauchySeq_tendsto fun x hx => ?_
  /- Given `n : ℕ`, for sufficiently large `a b : ℕ`, given any lift of `x b`, we can find a lift
    of `x a` such that the quotient of the lifts lies in `u n`. -/
  have key₀ : ∀ i j : ℕ, ∃ M : ℕ, j < M ∧ ∀ a b : ℕ, M ≤ a → M ≤ b →
      ∀ g : G, x b = g → ∃ g' : G, g / g' ∈ u i ∧ x a = g' := by
    have h𝓤GN : (𝓤 (G ⧸ N)).HasBasis (fun _ ↦ True) fun i ↦ { x | x.snd / x.fst ∈ (↑) '' u i } := by
      simpa [uniformity_eq_comap_nhds_one'] using hv.comap _
    rw [h𝓤GN.cauchySeq_iff] at hx
    simp only [mem_setOf_eq, forall_true_left, mem_image] at hx
    intro i j
    rcases hx i with ⟨M, hM⟩
    refine ⟨max j M + 1, (le_max_left _ _).trans_lt (lt_add_one _), fun a b ha hb g hg => ?_⟩
    obtain ⟨y, y_mem, hy⟩ :=
      hM a (((le_max_right j _).trans (lt_add_one _).le).trans ha) b
        (((le_max_right j _).trans (lt_add_one _).le).trans hb)
    refine
      ⟨y⁻¹ * g, by
        simpa only [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_cancel_left] using y_mem, ?_⟩
    rw [QuotientGroup.mk_mul, QuotientGroup.mk_inv, hy, hg, inv_div, div_mul_cancel]
  /- Inductively construct a subsequence `φ : ℕ → ℕ` using `key₀` so that if `a b : ℕ` exceed
    `φ (n + 1)`, then we may find lifts whose quotients lie within `u n`. -/
  set φ : ℕ → ℕ := fun n => Nat.recOn n (choose <| key₀ 0 0) fun k yk => choose <| key₀ (k + 1) yk
  have hφ :
    ∀ n : ℕ,
      φ n < φ (n + 1) ∧
        ∀ a b : ℕ,
          φ (n + 1) ≤ a →
            φ (n + 1) ≤ b → ∀ g : G, x b = g → ∃ g' : G, g / g' ∈ u (n + 1) ∧ x a = g' :=
    fun n => choose_spec (key₀ (n + 1) (φ n))
  /- Inductively construct a sequence `x' n : G` of lifts of `x (φ (n + 1))` such that quotients of
    successive terms lie in `x' n / x' (n + 1) ∈ u (n + 1)`. We actually need the proofs that each
    term is a lift to construct the next term, so we use a Σ-type. -/
  set x' : ∀ n, PSigma fun g : G => x (φ (n + 1)) = g := fun n =>
    Nat.recOn n
      ⟨choose (QuotientGroup.mk_surjective (x (φ 1))),
        (choose_spec (QuotientGroup.mk_surjective (x (φ 1)))).symm⟩
      fun k hk =>
      ⟨choose <| (hφ k).2 _ _ (hφ (k + 1)).1.le le_rfl hk.fst hk.snd,
        (choose_spec <| (hφ k).2 _ _ (hφ (k + 1)).1.le le_rfl hk.fst hk.snd).2⟩
  have hx' : ∀ n : ℕ, (x' n).fst / (x' (n + 1)).fst ∈ u (n + 1) := fun n =>
    (choose_spec <| (hφ n).2 _ _ (hφ (n + 1)).1.le le_rfl (x' n).fst (x' n).snd).1
  /- The sequence `x'` is Cauchy. This is where we exploit the condition on `u`. The key idea
    is to show by decreasing induction that `x' m / x' n ∈ u m` if `m ≤ n`. -/
  have x'_cauchy : CauchySeq fun n => (x' n).fst := by
    have h𝓤G : (𝓤 G).HasBasis (fun _ => True) fun i => { x | x.snd / x.fst ∈ u i } := by
      simpa [uniformity_eq_comap_nhds_one'] using hu.toHasBasis.comap _
    rw [h𝓤G.cauchySeq_iff']
    simp only [mem_setOf_eq, forall_true_left]
    exact fun m =>
      ⟨m, fun n hmn =>
        Nat.decreasingInduction'
          (fun k _ _ hk => u_mul k ⟨_, hx' k, _, hk, div_mul_div_cancel _ _ _⟩) hmn
          (by simpa only [div_self'] using mem_of_mem_nhds (hu.mem _))⟩
  /- Since `G` is complete, `x'` converges to some `x₀`, and so the image of this sequence under
    the quotient map converges to `↑x₀`. The image of `x'` is a convergent subsequence of `x`, and
    since `x` is Cauchy, this implies it converges. -/
  rcases cauchySeq_tendsto_of_complete x'_cauchy with ⟨x₀, hx₀⟩
  refine
    ⟨↑x₀,
      tendsto_nhds_of_cauchySeq_of_subseq hx
        (strictMono_nat_of_lt_succ fun n => (hφ (n + 1)).1).tendsto_atTop ?_⟩
  convert ((continuous_coinduced_rng : Continuous ((↑) : G → G ⧸ N)).tendsto x₀).comp hx₀
  exact funext fun n => (x' n).snd

Completeness of Quotient Groups for First-Countable Topological Groups

Informal description

Let $G$ be a first-countable topological group with a normal subgroup $N$. If $G$ is complete with respect to the right uniformity induced by its topology, then the quotient group $G/N$ is also complete with respect to the right uniformity induced by its quotient topology.

QuotientGroup.completeSpace instance

 (G : Type u) [Group G] [us : UniformSpace G] [IsUniformGroup G] [FirstCountableTopology G] (N : Subgroup G) [N.Normal]
  [hG : CompleteSpace G] : @CompleteSpace (G ⧸ N) (IsTopologicalGroup.toUniformSpace (G ⧸ N))

Full source

/-- The quotient `G ⧸ N` of a complete first countable uniform group `G` by a normal subgroup
is itself complete. In contrast to `QuotientGroup.completeSpace'`, in this version `G` is
already equipped with a uniform structure.
[N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b]

Even though `G` is equipped with a uniform structure, the quotient `G ⧸ N` does not inherit a
uniform structure, so it is still provided manually via `IsTopologicalGroup.toUniformSpace`.
In the most common use cases, this coincides (definitionally) with the uniform structure on the
quotient obtained via other means. -/
@[to_additive "The quotient `G ⧸ N` of a complete first countable uniform additive group
`G` by a normal additive subgroup is itself complete. Consequently, quotients of Banach spaces by
subspaces are complete. In contrast to `QuotientAddGroup.completeSpace'`, in this version
`G` is already equipped with a uniform structure.
[N. Bourbaki, *General Topology*, IX.3.1 Proposition 4][bourbaki1966b]

Even though `G` is equipped with a uniform structure, the quotient `G ⧸ N` does not inherit a
uniform structure, so it is still provided manually via `IsTopologicalAddGroup.toUniformSpace`.
In the most common use case ─ quotients of normed additive commutative groups by subgroups ─
significant care was taken so that the uniform structure inherent in that setting coincides
(definitionally) with the uniform structure provided here."]
instance QuotientGroup.completeSpace (G : Type u) [Group G] [us : UniformSpace G] [IsUniformGroup G]
    [FirstCountableTopology G] (N : Subgroup G) [N.Normal] [hG : CompleteSpace G] :
    @CompleteSpace (G ⧸ N) (IsTopologicalGroup.toUniformSpace (G ⧸ N)) := by
  rw [← @IsUniformGroup.toUniformSpace_eq _ us _ _] at hG
  infer_instance

Completeness of Quotient Groups for Uniform Groups

Informal description

Let $G$ be a first-countable uniform group with a normal subgroup $N$. If $G$ is complete with respect to its uniform structure, then the quotient group $G/N$ is also complete with respect to the uniform structure induced by the quotient topology.

Main results