Uniform structure on topological groups #
Main results #
extension of ℤ-bilinear maps to complete groups (useful for ring completions)
QuotientGroup.completeSpaceandQuotientAddGroup.completeSpaceguarantee that quotients of first countable topological groups by normal subgroups are themselves complete. In particular, the quotient of a Banach space by a subspace is complete.
theorem
isUniformEmbedding_translate_mul
{α : Type u_1}
[UniformSpace α]
[Group α]
[IsUniformGroup α]
(a : α)
:
IsUniformEmbedding fun (x : α) => x * a
theorem
isUniformEmbedding_translate_add
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[IsUniformAddGroup α]
(a : α)
:
IsUniformEmbedding fun (x : α) => x + a
theorem
IsUniformGroup.cauchy_iff_tendsto
{G : Type u_4}
[Group G]
[UniformSpace G]
[IsUniformGroup G]
(𝓕 : Filter G)
:
theorem
IsUniformAddGroup.cauchy_iff_tendsto
{G : Type u_4}
[AddGroup G]
[UniformSpace G]
[IsUniformAddGroup G]
(𝓕 : Filter G)
:
theorem
IsUniformGroup.cauchy_iff_tendsto_swapped
{G : Type u_4}
[Group G]
[UniformSpace G]
[IsUniformGroup G]
(𝓕 : Filter G)
:
theorem
IsUniformAddGroup.cauchy_iff_tendsto_swapped
{G : Type u_4}
[AddGroup G]
[UniformSpace G]
[IsUniformAddGroup G]
(𝓕 : Filter G)
:
theorem
IsUniformGroup.cauchy_map_iff_tendsto
{ι : Type u_3}
{G : Type u_4}
[Group G]
[UniformSpace G]
[IsUniformGroup G]
(𝓕 : Filter ι)
(f : ι → G)
:
Cauchy (Filter.map f 𝓕) ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun (p : ι × ι) => f p.1 / f p.2) (𝓕 ×ˢ 𝓕) (nhds 1)
theorem
IsUniformAddGroup.cauchy_map_iff_tendsto
{ι : Type u_3}
{G : Type u_4}
[AddGroup G]
[UniformSpace G]
[IsUniformAddGroup G]
(𝓕 : Filter ι)
(f : ι → G)
:
Cauchy (Filter.map f 𝓕) ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun (p : ι × ι) => f p.1 - f p.2) (𝓕 ×ˢ 𝓕) (nhds 0)
theorem
IsUniformGroup.cauchy_map_iff_tendsto_swapped
{ι : Type u_3}
{G : Type u_4}
[Group G]
[UniformSpace G]
[IsUniformGroup G]
(𝓕 : Filter ι)
(f : ι → G)
:
Cauchy (Filter.map f 𝓕) ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun (p : ι × ι) => f p.2 / f p.1) (𝓕 ×ˢ 𝓕) (nhds 1)
theorem
IsUniformAddGroup.cauchy_map_iff_tendsto_swapped
{ι : Type u_3}
{G : Type u_4}
[AddGroup G]
[UniformSpace G]
[IsUniformAddGroup G]
(𝓕 : Filter ι)
(f : ι → G)
:
Cauchy (Filter.map f 𝓕) ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun (p : ι × ι) => f p.2 - f p.1) (𝓕 ×ˢ 𝓕) (nhds 0)
instance
Subgroup.isUniformGroup
{α : Type u_1}
[UniformSpace α]
[Group α]
[IsUniformGroup α]
(S : Subgroup α)
:
instance
AddSubgroup.isUniformAddGroup
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[IsUniformAddGroup α]
(S : AddSubgroup α)
:
theorem
CauchySeq.mul
{α : Type u_1}
[UniformSpace α]
[Group α]
[IsUniformGroup α]
{ι : Type u_3}
[Preorder ι]
{u v : ι → α}
(hu : CauchySeq u)
(hv : CauchySeq v)
:
theorem
CauchySeq.add
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[IsUniformAddGroup α]
{ι : Type u_3}
[Preorder ι]
{u v : ι → α}
(hu : CauchySeq u)
(hv : CauchySeq v)
:
theorem
CauchySeq.mul_const
{α : Type u_1}
[UniformSpace α]
[Group α]
[IsUniformGroup α]
{ι : Type u_3}
[Preorder ι]
{u : ι → α}
{x : α}
(hu : CauchySeq u)
:
theorem
CauchySeq.add_const
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[IsUniformAddGroup α]
{ι : Type u_3}
[Preorder ι]
{u : ι → α}
{x : α}
(hu : CauchySeq u)
:
theorem
CauchySeq.const_mul
{α : Type u_1}
[UniformSpace α]
[Group α]
[IsUniformGroup α]
{ι : Type u_3}
[Preorder ι]
{u : ι → α}
{x : α}
(hu : CauchySeq u)
:
theorem
CauchySeq.const_add
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[IsUniformAddGroup α]
{ι : Type u_3}
[Preorder ι]
{u : ι → α}
{x : α}
(hu : CauchySeq u)
:
theorem
CauchySeq.inv
{α : Type u_1}
[UniformSpace α]
[Group α]
[IsUniformGroup α]
{ι : Type u_3}
[Preorder ι]
{u : ι → α}
(h : CauchySeq u)
:
theorem
CauchySeq.neg
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[IsUniformAddGroup α]
{ι : Type u_3}
[Preorder ι]
{u : ι → α}
(h : CauchySeq u)
:
theorem
totallyBounded_iff_subset_finite_iUnion_nhds_one
{α : Type u_1}
[UniformSpace α]
[Group α]
[IsUniformGroup α]
{s : Set α}
:
theorem
totallyBounded_iff_subset_finite_iUnion_nhds_zero
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[IsUniformAddGroup α]
{s : Set α}
:
theorem
totallyBounded_inv
{α : Type u_1}
[UniformSpace α]
[Group α]
[IsUniformGroup α]
{s : Set α}
(hs : TotallyBounded s)
:
theorem
totallyBounded_neg
{α : Type u_1}
[UniformSpace α]
[AddGroup α]
[IsUniformAddGroup α]
{s : Set α}
(hs : TotallyBounded s)
:
TotallyBounded (-s)
theorem
TendstoUniformlyOnFilter.mul
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[IsUniformGroup α]
{ι : Type u_3}
{l : Filter ι}
{l' : Filter β}
{f f' : ι → β → α}
{g g' : β → α}
(hf : TendstoUniformlyOnFilter f g l l')
(hf' : TendstoUniformlyOnFilter f' g' l l')
:
TendstoUniformlyOnFilter (f * f') (g * g') l l'
theorem
TendstoUniformlyOnFilter.add
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[IsUniformAddGroup α]
{ι : Type u_3}
{l : Filter ι}
{l' : Filter β}
{f f' : ι → β → α}
{g g' : β → α}
(hf : TendstoUniformlyOnFilter f g l l')
(hf' : TendstoUniformlyOnFilter f' g' l l')
:
TendstoUniformlyOnFilter (f + f') (g + g') l l'
theorem
TendstoUniformlyOnFilter.div
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[IsUniformGroup α]
{ι : Type u_3}
{l : Filter ι}
{l' : Filter β}
{f f' : ι → β → α}
{g g' : β → α}
(hf : TendstoUniformlyOnFilter f g l l')
(hf' : TendstoUniformlyOnFilter f' g' l l')
:
TendstoUniformlyOnFilter (f / f') (g / g') l l'
theorem
TendstoUniformlyOnFilter.sub
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[IsUniformAddGroup α]
{ι : Type u_3}
{l : Filter ι}
{l' : Filter β}
{f f' : ι → β → α}
{g g' : β → α}
(hf : TendstoUniformlyOnFilter f g l l')
(hf' : TendstoUniformlyOnFilter f' g' l l')
:
TendstoUniformlyOnFilter (f - f') (g - g') l l'
theorem
TendstoUniformlyOn.mul
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[IsUniformGroup α]
{ι : Type u_3}
{l : Filter ι}
{f f' : ι → β → α}
{g g' : β → α}
{s : Set β}
(hf : TendstoUniformlyOn f g l s)
(hf' : TendstoUniformlyOn f' g' l s)
:
TendstoUniformlyOn (f * f') (g * g') l s
theorem
TendstoUniformlyOn.add
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[IsUniformAddGroup α]
{ι : Type u_3}
{l : Filter ι}
{f f' : ι → β → α}
{g g' : β → α}
{s : Set β}
(hf : TendstoUniformlyOn f g l s)
(hf' : TendstoUniformlyOn f' g' l s)
:
TendstoUniformlyOn (f + f') (g + g') l s
theorem
TendstoUniformlyOn.div
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[IsUniformGroup α]
{ι : Type u_3}
{l : Filter ι}
{f f' : ι → β → α}
{g g' : β → α}
{s : Set β}
(hf : TendstoUniformlyOn f g l s)
(hf' : TendstoUniformlyOn f' g' l s)
:
TendstoUniformlyOn (f / f') (g / g') l s
theorem
TendstoUniformlyOn.sub
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[IsUniformAddGroup α]
{ι : Type u_3}
{l : Filter ι}
{f f' : ι → β → α}
{g g' : β → α}
{s : Set β}
(hf : TendstoUniformlyOn f g l s)
(hf' : TendstoUniformlyOn f' g' l s)
:
TendstoUniformlyOn (f - f') (g - g') l s
theorem
TendstoUniformly.mul
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[IsUniformGroup α]
{ι : Type u_3}
{l : Filter ι}
{f f' : ι → β → α}
{g g' : β → α}
(hf : TendstoUniformly f g l)
(hf' : TendstoUniformly f' g' l)
:
TendstoUniformly (f * f') (g * g') l
theorem
TendstoUniformly.add
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[IsUniformAddGroup α]
{ι : Type u_3}
{l : Filter ι}
{f f' : ι → β → α}
{g g' : β → α}
(hf : TendstoUniformly f g l)
(hf' : TendstoUniformly f' g' l)
:
TendstoUniformly (f + f') (g + g') l
theorem
TendstoUniformly.div
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[IsUniformGroup α]
{ι : Type u_3}
{l : Filter ι}
{f f' : ι → β → α}
{g g' : β → α}
(hf : TendstoUniformly f g l)
(hf' : TendstoUniformly f' g' l)
:
TendstoUniformly (f / f') (g / g') l
theorem
TendstoUniformly.sub
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[IsUniformAddGroup α]
{ι : Type u_3}
{l : Filter ι}
{f f' : ι → β → α}
{g g' : β → α}
(hf : TendstoUniformly f g l)
(hf' : TendstoUniformly f' g' l)
:
TendstoUniformly (f - f') (g - g') l
theorem
UniformCauchySeqOn.mul
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[IsUniformGroup α]
{ι : Type u_3}
{l : Filter ι}
{f f' : ι → β → α}
{s : Set β}
(hf : UniformCauchySeqOn f l s)
(hf' : UniformCauchySeqOn f' l s)
:
UniformCauchySeqOn (f * f') l s
theorem
UniformCauchySeqOn.add
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[IsUniformAddGroup α]
{ι : Type u_3}
{l : Filter ι}
{f f' : ι → β → α}
{s : Set β}
(hf : UniformCauchySeqOn f l s)
(hf' : UniformCauchySeqOn f' l s)
:
UniformCauchySeqOn (f + f') l s
theorem
UniformCauchySeqOn.div
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[Group α]
[IsUniformGroup α]
{ι : Type u_3}
{l : Filter ι}
{f f' : ι → β → α}
{s : Set β}
(hf : UniformCauchySeqOn f l s)
(hf' : UniformCauchySeqOn f' l s)
:
UniformCauchySeqOn (f / f') l s
theorem
UniformCauchySeqOn.sub
{α : Type u_1}
{β : Type u_2}
[UniformSpace α]
[AddGroup α]
[IsUniformAddGroup α]
{ι : Type u_3}
{l : Filter ι}
{f f' : ι → β → α}
{s : Set β}
(hf : UniformCauchySeqOn f l s)
(hf' : UniformCauchySeqOn f' l s)
:
UniformCauchySeqOn (f - f') l s
instance
IsUniformGroup.of_compactSpace
{β : Type u_2}
[UniformSpace β]
[Group β]
[ContinuousDiv β]
[CompactSpace β]
:
instance
IsUniformAddGroup.of_compactSpace
{β : Type u_2}
[UniformSpace β]
[AddGroup β]
[ContinuousSub β]
[CompactSpace β]
:
@[deprecated IsUniformGroup.of_compactSpace (since := "2025-09-27")]
theorem
topologicalGroup_is_uniform_of_compactSpace
(G : Type u_1)
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
[CompactSpace G]
:
@[deprecated IsUniformGroup.of_compactSpace (since := "2025-09-27")]
theorem
topologicalAddGroup_is_uniform_of_compactSpace
(G : Type u_1)
[AddGroup G]
[TopologicalSpace G]
[IsTopologicalAddGroup G]
[CompactSpace G]
:
instance
Subgroup.isClosed_of_discrete
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
[T2Space G]
{H : Subgroup G}
[DiscreteTopology ↥H]
:
IsClosed ↑H
instance
AddSubgroup.isClosed_of_discrete
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[IsTopologicalAddGroup G]
[T2Space G]
{H : AddSubgroup G}
[DiscreteTopology ↥H]
:
IsClosed ↑H
theorem
Subgroup.tendsto_coe_cofinite_of_discrete
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
[T2Space G]
(H : Subgroup G)
[DiscreteTopology ↥H]
:
theorem
AddSubgroup.tendsto_coe_cofinite_of_discrete
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[IsTopologicalAddGroup G]
[T2Space G]
(H : AddSubgroup G)
[DiscreteTopology ↥H]
:
theorem
MonoidHom.tendsto_coe_cofinite_of_discrete
{G : Type u_1}
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
[T2Space G]
{H : Type u_2}
[Group H]
{f : H →* G}
(hf : Function.Injective ⇑f)
(hf' : DiscreteTopology ↥f.range)
:
theorem
AddMonoidHom.tendsto_coe_cofinite_of_discrete
{G : Type u_1}
[AddGroup G]
[TopologicalSpace G]
[IsTopologicalAddGroup G]
[T2Space G]
{H : Type u_2}
[AddGroup H]
{f : H →+ G}
(hf : Function.Injective ⇑f)
(hf' : DiscreteTopology ↥f.range)
:
theorem
IsTopologicalGroup.tendstoUniformly_iff
{ι : Type u_1}
{α : Type u_2}
{G : Type u_3}
[Group G]
[u : UniformSpace G]
[IsTopologicalGroup G]
(F : ι → α → G)
(f : α → G)
(p : Filter ι)
(hu : toUniformSpace G = u)
:
theorem
IsTopologicalAddGroup.tendstoUniformly_iff
{ι : Type u_1}
{α : Type u_2}
{G : Type u_3}
[AddGroup G]
[u : UniformSpace G]
[IsTopologicalAddGroup G]
(F : ι → α → G)
(f : α → G)
(p : Filter ι)
(hu : toUniformSpace G = u)
:
theorem
IsTopologicalGroup.tendstoUniformlyOn_iff
{ι : Type u_1}
{α : Type u_2}
{G : Type u_3}
[Group G]
[u : UniformSpace G]
[IsTopologicalGroup G]
(F : ι → α → G)
(f : α → G)
(p : Filter ι)
(s : Set α)
(hu : toUniformSpace G = u)
:
theorem
IsTopologicalAddGroup.tendstoUniformlyOn_iff
{ι : Type u_1}
{α : Type u_2}
{G : Type u_3}
[AddGroup G]
[u : UniformSpace G]
[IsTopologicalAddGroup G]
(F : ι → α → G)
(f : α → G)
(p : Filter ι)
(s : Set α)
(hu : toUniformSpace G = u)
:
theorem
IsTopologicalGroup.tendstoLocallyUniformly_iff
{ι : Type u_1}
{α : Type u_2}
{G : Type u_3}
[Group G]
[u : UniformSpace G]
[IsTopologicalGroup G]
[TopologicalSpace α]
(F : ι → α → G)
(f : α → G)
(p : Filter ι)
(hu : toUniformSpace G = u)
:
theorem
IsTopologicalAddGroup.tendstoLocallyUniformly_iff
{ι : Type u_1}
{α : Type u_2}
{G : Type u_3}
[AddGroup G]
[u : UniformSpace G]
[IsTopologicalAddGroup G]
[TopologicalSpace α]
(F : ι → α → G)
(f : α → G)
(p : Filter ι)
(hu : toUniformSpace G = u)
:
theorem
IsTopologicalGroup.tendstoLocallyUniformlyOn_iff
{ι : Type u_1}
{α : Type u_2}
{G : Type u_3}
[Group G]
[u : UniformSpace G]
[IsTopologicalGroup G]
[TopologicalSpace α]
(F : ι → α → G)
(f : α → G)
(p : Filter ι)
(s : Set α)
(hu : toUniformSpace G = u)
:
TendstoLocallyUniformlyOn F f p s ↔ ∀ u_1 ∈ nhds 1, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u_1
theorem
IsTopologicalAddGroup.tendstoLocallyUniformlyOn_iff
{ι : Type u_1}
{α : Type u_2}
{G : Type u_3}
[AddGroup G]
[u : UniformSpace G]
[IsTopologicalAddGroup G]
[TopologicalSpace α]
(F : ι → α → G)
(f : α → G)
(p : Filter ι)
(s : Set α)
(hu : toUniformSpace G = u)
:
TendstoLocallyUniformlyOn F f p s ↔ ∀ u_1 ∈ nhds 0, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a - f a ∈ u_1
theorem
IsDenseInducing.extend_Z_bilin
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{G : Type u_5}
[TopologicalSpace α]
[AddCommGroup α]
[IsTopologicalAddGroup α]
[TopologicalSpace β]
[AddCommGroup β]
[TopologicalSpace γ]
[AddCommGroup γ]
[IsTopologicalAddGroup γ]
[TopologicalSpace δ]
[AddCommGroup δ]
[UniformSpace G]
[AddCommGroup G]
{e : β →+ α}
(de : IsDenseInducing ⇑e)
{f : δ →+ γ}
(df : IsDenseInducing ⇑f)
{φ : β →+ δ →+ G}
(hφ : Continuous fun (p : β × δ) => (φ p.1) p.2)
[IsUniformAddGroup G]
[T0Space G]
[CompleteSpace G]
:
Continuous (⋯.extend fun (p : β × δ) => (φ p.1) p.2)
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.
instance
QuotientGroup.completeSpace'
(G : Type u)
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
[FirstCountableTopology G]
(N : Subgroup G)
[N.Normal]
[CompleteSpace G]
:
CompleteSpace (G ⧸ N)
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.
instance
QuotientAddGroup.completeSpace'
(G : Type u)
[AddGroup G]
[TopologicalSpace G]
[IsTopologicalAddGroup G]
[FirstCountableTopology G]
(N : AddSubgroup G)
[N.Normal]
[CompleteSpace G]
:
CompleteSpace (G ⧸ N)
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]
[us : UniformSpace G]
[IsUniformGroup G]
[FirstCountableTopology G]
(N : Subgroup G)
[N.Normal]
[hG : CompleteSpace G]
:
CompleteSpace (G ⧸ N)
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.
instance
QuotientAddGroup.completeSpace
(G : Type u)
[AddGroup G]
[us : UniformSpace G]
[IsUniformAddGroup G]
[FirstCountableTopology G]
(N : AddSubgroup G)
[N.Normal]
[hG : CompleteSpace G]
:
CompleteSpace (G ⧸ N)
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.