mathlib documentation

topology.algebra.group.basic

Topological groups #

This file defines the following typeclasses:

There is an instance deducing has_continuous_sub from topological_group but we use a separate typeclass because, e.g., and ℝ≥0 have continuous subtraction but are not additive groups.

We also define homeomorph versions of several equivs: homeomorph.mul_left, homeomorph.mul_right, homeomorph.inv, and prove a few facts about neighbourhood filters in groups.

Tags #

topological space, group, topological group

Groups with continuous multiplication #

In this section we prove a few statements about groups with continuous (*).

@[protected]

Addition from the left in a topological additive group as a homeomorphism.

Equations
@[protected]
def homeomorph.mul_left {G : Type w} [topological_space G] [group G] [has_continuous_mul G] (a : G) :
G ≃ₜ G

Multiplication from the left in a topological group as a homeomorphism.

Equations
theorem is_open_map_add_left {G : Type w} [topological_space G] [add_group G] [has_continuous_add G] (a : G) :
is_open_map (λ (x : G), a + x)
theorem is_open_map_mul_left {G : Type w} [topological_space G] [group G] [has_continuous_mul G] (a : G) :
is_open_map (λ (x : G), a * x)
theorem is_open.left_add_coset {G : Type w} [topological_space G] [add_group G] [has_continuous_add G] {U : set G} (h : is_open U) (x : G) :
theorem is_open.left_coset {G : Type w} [topological_space G] [group G] [has_continuous_mul G] {U : set G} (h : is_open U) (x : G) :
theorem is_closed_map_mul_left {G : Type w} [topological_space G] [group G] [has_continuous_mul G] (a : G) :
is_closed_map (λ (x : G), a * x)
theorem is_closed_map_add_left {G : Type w} [topological_space G] [add_group G] [has_continuous_add G] (a : G) :
is_closed_map (λ (x : G), a + x)
theorem is_closed.left_coset {G : Type w} [topological_space G] [group G] [has_continuous_mul G] {U : set G} (h : is_closed U) (x : G) :
@[protected]

Addition from the right in a topological additive group as a homeomorphism.

Equations
@[protected]

Multiplication from the right in a topological group as a homeomorphism.

Equations
@[simp]
theorem homeomorph.coe_mul_right {G : Type w} [topological_space G] [group G] [has_continuous_mul G] (a : G) :
(homeomorph.mul_right a) = λ (g : G), g * a
@[simp]
theorem homeomorph.coe_add_right {G : Type w} [topological_space G] [add_group G] [has_continuous_add G] (a : G) :
(homeomorph.add_right a) = λ (g : G), g + a
theorem is_open_map_mul_right {G : Type w} [topological_space G] [group G] [has_continuous_mul G] (a : G) :
is_open_map (λ (x : G), x * a)
theorem is_open_map_add_right {G : Type w} [topological_space G] [add_group G] [has_continuous_add G] (a : G) :
is_open_map (λ (x : G), x + a)
theorem is_open.right_coset {G : Type w} [topological_space G] [group G] [has_continuous_mul G] {U : set G} (h : is_open U) (x : G) :
theorem is_closed_map_mul_right {G : Type w} [topological_space G] [group G] [has_continuous_mul G] (a : G) :
is_closed_map (λ (x : G), x * a)
theorem is_closed_map_add_right {G : Type w} [topological_space G] [add_group G] [has_continuous_add G] (a : G) :
is_closed_map (λ (x : G), x + a)
theorem is_closed.right_coset {G : Type w} [topological_space G] [group G] [has_continuous_mul G] {U : set G} (h : is_closed U) (x : G) :

has_continuous_inv and has_continuous_neg #

@[class]
structure has_continuous_inv (G : Type u) [topological_space G] [has_inv G] :
Prop

Basic hypothesis to talk about a topological group. A topological group over M, for example, is obtained by requiring the instances group M and has_continuous_mul M and has_continuous_inv M.

Instances of this typeclass
theorem filter.tendsto.inv {α : Type u} {G : Type w} [topological_space G] [has_inv G] [has_continuous_inv G] {f : α G} {l : filter α} {y : G} (h : filter.tendsto f l (nhds y)) :
filter.tendsto (λ (x : α), (f x)⁻¹) l (nhds y⁻¹)

If a function converges to a value in a multiplicative topological group, then its inverse converges to the inverse of this value. For the version in normed fields assuming additionally that the limit is nonzero, use tendsto.inv'.

theorem filter.tendsto.neg {α : Type u} {G : Type w} [topological_space G] [has_neg G] [has_continuous_neg G] {f : α G} {l : filter α} {y : G} (h : filter.tendsto f l (nhds y)) :
filter.tendsto (λ (x : α), -f x) l (nhds (-y))

If a function converges to a value in an additive topological group, then its negation converges to the negation of this value.

@[continuity]
theorem continuous.inv {α : Type u} {G : Type w} [topological_space G] [has_inv G] [has_continuous_inv G] [topological_space α] {f : α G} (hf : continuous f) :
continuous (λ (x : α), (f x)⁻¹)
@[continuity]
theorem continuous.neg {α : Type u} {G : Type w} [topological_space G] [has_neg G] [has_continuous_neg G] [topological_space α] {f : α G} (hf : continuous f) :
continuous (λ (x : α), -f x)
theorem continuous_at.neg {α : Type u} {G : Type w} [topological_space G] [has_neg G] [has_continuous_neg G] [topological_space α] {f : α G} {x : α} (hf : continuous_at f x) :
continuous_at (λ (x : α), -f x) x
theorem continuous_at.inv {α : Type u} {G : Type w} [topological_space G] [has_inv G] [has_continuous_inv G] [topological_space α] {f : α G} {x : α} (hf : continuous_at f x) :
continuous_at (λ (x : α), (f x)⁻¹) x
theorem continuous_on.inv {α : Type u} {G : Type w} [topological_space G] [has_inv G] [has_continuous_inv G] [topological_space α] {f : α G} {s : set α} (hf : continuous_on f s) :
continuous_on (λ (x : α), (f x)⁻¹) s
theorem continuous_on.neg {α : Type u} {G : Type w} [topological_space G] [has_neg G] [has_continuous_neg G] [topological_space α] {f : α G} {s : set α} (hf : continuous_on f s) :
continuous_on (λ (x : α), -f x) s
theorem continuous_within_at.inv {α : Type u} {G : Type w} [topological_space G] [has_inv G] [has_continuous_inv G] [topological_space α] {f : α G} {s : set α} {x : α} (hf : continuous_within_at f s x) :
continuous_within_at (λ (x : α), (f x)⁻¹) s x
theorem continuous_within_at.neg {α : Type u} {G : Type w} [topological_space G] [has_neg G] [has_continuous_neg G] [topological_space α] {f : α G} {s : set α} {x : α} (hf : continuous_within_at f s x) :
continuous_within_at (λ (x : α), -f x) s x
@[protected, instance]
def pi.has_continuous_inv {ι : Type u_1} {C : ι Type u_2} [Π (i : ι), topological_space (C i)] [Π (i : ι), has_inv (C i)] [ (i : ι), has_continuous_inv (C i)] :
has_continuous_inv (Π (i : ι), C i)
@[protected, instance]
def pi.has_continuous_neg {ι : Type u_1} {C : ι Type u_2} [Π (i : ι), topological_space (C i)] [Π (i : ι), has_neg (C i)] [ (i : ι), has_continuous_neg (C i)] :
has_continuous_neg (Π (i : ι), C i)
@[protected, instance]

A version of pi.has_continuous_neg for non-dependent functions. It is needed because sometimes Lean fails to use pi.has_continuous_neg for non-dependent functions.

@[protected, instance]

A version of pi.has_continuous_inv for non-dependent functions. It is needed because sometimes Lean fails to use pi.has_continuous_inv for non-dependent functions.

theorem is_closed_set_of_map_neg (G₁ : Type u_2) (G₂ : Type u_3) [topological_space G₂] [t2_space G₂] [has_neg G₁] [has_neg G₂] [has_continuous_neg G₂] :
is_closed {f : G₁ G₂ | (x : G₁), f (-x) = -f x}
theorem is_closed_set_of_map_inv (G₁ : Type u_2) (G₂ : Type u_3) [topological_space G₂] [t2_space G₂] [has_inv G₁] [has_inv G₂] [has_continuous_inv G₂] :
is_closed {f : G₁ G₂ | (x : G₁), f x⁻¹ = (f x)⁻¹}
@[protected]

Negation in a topological group as a homeomorphism.

Equations
@[protected]

Inversion in a topological group as a homeomorphism.

Equations
theorem is_open.neg {G : Type w} [topological_space G] [has_involutive_neg G] [has_continuous_neg G] {s : set G} (hs : is_open s) :
theorem has_continuous_inv_infi {G : Type w} {ι' : Sort u_1} [has_inv G] {ts' : ι' topological_space G} (h' : (i : ι'), has_continuous_inv G) :
theorem has_continuous_neg_infi {G : Type w} {ι' : Sort u_1} [has_neg G] {ts' : ι' topological_space G} (h' : (i : ι'), has_continuous_neg G) :
theorem inducing.has_continuous_neg {G : Type u_1} {H : Type u_2} [has_neg G] [has_neg H] [topological_space G] [topological_space H] [has_continuous_neg H] {f : G H} (hf : inducing f) (hf_inv : (x : G), f (-x) = -f x) :
theorem inducing.has_continuous_inv {G : Type u_1} {H : Type u_2} [has_inv G] [has_inv H] [topological_space G] [topological_space H] [has_continuous_inv H] {f : G H} (hf : inducing f) (hf_inv : (x : G), f x⁻¹ = (f x)⁻¹) :

Topological groups #

A topological group is a group in which the multiplication and inversion operations are continuous. Topological additive groups are defined in the same way. Equivalently, we can require that the division operation λ x y, x * y⁻¹ (resp., subtraction) is continuous.

Conjugation is jointly continuous on G × G when both mul and inv are continuous.

Conjugation is jointly continuous on G × G when both mul and inv are continuous.

theorem topological_add_group.continuous_conj {G : Type w} [topological_space G] [has_neg G] [has_add G] [has_continuous_add G] (g : G) :
continuous (λ (h : G), g + h + -g)

Conjugation by a fixed element is continuous when add is continuous.

theorem topological_group.continuous_conj {G : Type w} [topological_space G] [has_inv G] [has_mul G] [has_continuous_mul G] (g : G) :
continuous (λ (h : G), g * h * g⁻¹)

Conjugation by a fixed element is continuous when mul is continuous.

Conjugation acting on fixed element of the additive group is continuous when both add and neg are continuous.

Conjugation acting on fixed element of the group is continuous when both mul and inv are continuous.

@[continuity]
theorem continuous_zpow {G : Type w} [topological_space G] [group G] [topological_group G] (z : ) :
continuous (λ (a : G), a ^ z)
@[continuity]
theorem continuous_zsmul {G : Type w} [topological_space G] [add_group G] [topological_add_group G] (z : ) :
continuous (λ (a : G), z a)
@[continuity]
theorem continuous.zsmul {α : Type u} {G : Type w} [topological_space G] [add_group G] [topological_add_group G] [topological_space α] {f : α G} (h : continuous f) (z : ) :
continuous (λ (b : α), z f b)
@[continuity]
theorem continuous.zpow {α : Type u} {G : Type w} [topological_space G] [group G] [topological_group G] [topological_space α] {f : α G} (h : continuous f) (z : ) :
continuous (λ (b : α), f b ^ z)
theorem continuous_on_zpow {G : Type w} [topological_space G] [group G] [topological_group G] {s : set G} (z : ) :
continuous_on (λ (x : G), x ^ z) s
theorem continuous_on_zsmul {G : Type w} [topological_space G] [add_group G] [topological_add_group G] {s : set G} (z : ) :
continuous_on (λ (x : G), z x) s
theorem continuous_at_zsmul {G : Type w} [topological_space G] [add_group G] [topological_add_group G] (x : G) (z : ) :
continuous_at (λ (x : G), z x) x
theorem continuous_at_zpow {G : Type w} [topological_space G] [group G] [topological_group G] (x : G) (z : ) :
continuous_at (λ (x : G), x ^ z) x
theorem filter.tendsto.zpow {G : Type w} [topological_space G] [group G] [topological_group G] {α : Type u_1} {l : filter α} {f : α G} {x : G} (hf : filter.tendsto f l (nhds x)) (z : ) :
filter.tendsto (λ (x : α), f x ^ z) l (nhds (x ^ z))
theorem filter.tendsto.zsmul {G : Type w} [topological_space G] [add_group G] [topological_add_group G] {α : Type u_1} {l : filter α} {f : α G} {x : G} (hf : filter.tendsto f l (nhds x)) (z : ) :
filter.tendsto (λ (x : α), z f x) l (nhds (z x))
theorem continuous_within_at.zpow {α : Type u} {G : Type w} [topological_space G] [group G] [topological_group G] [topological_space α] {f : α G} {x : α} {s : set α} (hf : continuous_within_at f s x) (z : ) :
continuous_within_at (λ (x : α), f x ^ z) s x
theorem continuous_within_at.zsmul {α : Type u} {G : Type w} [topological_space G] [add_group G] [topological_add_group G] [topological_space α] {f : α G} {x : α} {s : set α} (hf : continuous_within_at f s x) (z : ) :
continuous_within_at (λ (x : α), z f x) s x
theorem continuous_at.zsmul {α : Type u} {G : Type w} [topological_space G] [add_group G] [topological_add_group G] [topological_space α] {f : α G} {x : α} (hf : continuous_at f x) (z : ) :
continuous_at (λ (x : α), z f x) x
theorem continuous_at.zpow {α : Type u} {G : Type w} [topological_space G] [group G] [topological_group G] [topological_space α] {f : α G} {x : α} (hf : continuous_at f x) (z : ) :
continuous_at (λ (x : α), f x ^ z) x
theorem continuous_on.zsmul {α : Type u} {G : Type w} [topological_space G] [add_group G] [topological_add_group G] [topological_space α] {f : α G} {s : set α} (hf : continuous_on f s) (z : ) :
continuous_on (λ (x : α), z f x) s
theorem continuous_on.zpow {α : Type u} {G : Type w} [topological_space G] [group G] [topological_group G] [topological_space α] {f : α G} {s : set α} (hf : continuous_on f s) (z : ) :
continuous_on (λ (x : α), f x ^ z) s
@[protected, instance]
@[protected, instance]
def pi.topological_add_group {β : Type v} {C : β Type u_1} [Π (b : β), topological_space (C b)] [Π (b : β), add_group (C b)] [ (b : β), topological_add_group (C b)] :
topological_add_group (Π (b : β), C b)
@[protected, instance]
def pi.topological_group {β : Type v} {C : β Type u_1} [Π (b : β), topological_space (C b)] [Π (b : β), group (C b)] [ (b : β), topological_group (C b)] :
topological_group (Π (b : β), C b)
@[protected, instance]

If addition is continuous in α, then it also is in αᵃᵒᵖ.

@[protected, instance]

If multiplication is continuous in α, then it also is in αᵐᵒᵖ.

theorem neg_mem_nhds_zero (G : Type w) [topological_space G] [add_group G] [topological_add_group G] {S : set G} (hS : S nhds 0) :
theorem inv_mem_nhds_one (G : Type w) [topological_space G] [group G] [topological_group G] {S : set G} (hS : S nhds 1) :
@[protected]

The map (x, y) ↦ (x, xy) as a homeomorphism. This is a shear mapping.

Equations
@[protected]

The map (x, y) ↦ (x, x + y) as a homeomorphism. This is a shear mapping.

Equations
@[protected]
theorem inducing.topological_group {G : Type w} {H : Type x} [topological_space G] [group G] [topological_group G] {F : Type u_1} [group H] [topological_space H] [monoid_hom_class F H G] (f : F) (hf : inducing f) :
@[protected]
theorem topological_group_induced {G : Type w} {H : Type x} [topological_space G] [group G] [topological_group G] {F : Type u_1} [group H] [monoid_hom_class F H G] (f : F) :
@[protected]
@[protected, instance]

The (topological-space) closure of a subgroup of a space M with has_continuous_mul is itself a subgroup.

Equations

The (topological-space) closure of an additive subgroup of a space M with has_continuous_add is itself an additive subgroup.

Equations

The topological closure of a normal additive subgroup is normal.

The topological closure of a normal subgroup is normal.

The connected component of 1 is a subgroup of G.

Equations
theorem exists_nhds_half_neg {G : Type w} [topological_space G] [add_group G] [topological_add_group G] {s : set G} (hs : s nhds 0) :
(V : set G) (H : V nhds 0), (v : G), v V (w : G), w V v - w s
theorem exists_nhds_split_inv {G : Type w} [topological_space G] [group G] [topological_group G] {s : set G} (hs : s nhds 1) :
(V : set G) (H : V nhds 1), (v : G), v V (w : G), w V v / w s
theorem nhds_translation_add_neg {G : Type w} [topological_space G] [add_group G] [topological_add_group G] (x : G) :
filter.comap (λ (y : G), y + -x) (nhds 0) = nhds x
theorem nhds_translation_mul_inv {G : Type w} [topological_space G] [group G] [topological_group G] (x : G) :
filter.comap (λ (y : G), y * x⁻¹) (nhds 1) = nhds x
@[simp]
theorem map_add_left_nhds {G : Type w} [topological_space G] [add_group G] [topological_add_group G] (x y : G) :
@[simp]
theorem map_mul_left_nhds {G : Type w} [topological_space G] [group G] [topological_group G] (x y : G) :
@[simp]
theorem map_add_right_nhds {G : Type w} [topological_space G] [add_group G] [topological_add_group G] (x y : G) :
filter.map (λ (z : G), z + x) (nhds y) = nhds (y + x)
@[simp]
theorem map_mul_right_nhds {G : Type w} [topological_space G] [group G] [topological_group G] (x y : G) :
filter.map (λ (z : G), z * x) (nhds y) = nhds (y * x)
theorem map_mul_right_nhds_one {G : Type w} [topological_space G] [group G] [topological_group G] (x : G) :
filter.map (λ (y : G), y * x) (nhds 1) = nhds x
theorem map_add_right_nhds_zero {G : Type w} [topological_space G] [add_group G] [topological_add_group G] (x : G) :
filter.map (λ (y : G), y + x) (nhds 0) = nhds x
theorem filter.has_basis.nhds_of_zero {G : Type w} [topological_space G] [add_group G] [topological_add_group G] {ι : Sort u_1} {p : ι Prop} {s : ι set G} (hb : (nhds 0).has_basis p s) (x : G) :
(nhds x).has_basis p (λ (i : ι), {y : G | y - x s i})
theorem filter.has_basis.nhds_of_one {G : Type w} [topological_space G] [group G] [topological_group G] {ι : Sort u_1} {p : ι Prop} {s : ι set G} (hb : (nhds 1).has_basis p s) (x : G) :
(nhds x).has_basis p (λ (i : ι), {y : G | y / x s i})
theorem mem_closure_iff_nhds_zero {G : Type w} [topological_space G] [add_group G] [topological_add_group G] {x : G} {s : set G} :
x closure s (U : set G), U nhds 0 ( (y : G) (H : y s), y - x U)
theorem mem_closure_iff_nhds_one {G : Type w} [topological_space G] [group G] [topological_group G] {x : G} {s : set G} :
x closure s (U : set G), U nhds 1 ( (y : G) (H : y s), y / x U)

A monoid homomorphism (a bundled morphism of a type that implements monoid_hom_class) from a topological group to a topological monoid is continuous provided that it is continuous at one. See also uniform_continuous_of_continuous_at_one.

An additive monoid homomorphism (a bundled morphism of a type that implements add_monoid_hom_class) from an additive topological group to an additive topological monoid is continuous provided that it is continuous at zero. See also uniform_continuous_of_continuous_at_zero.

theorem topological_group.ext {G : Type u_1} [group G] {t t' : topological_space G} (tg : topological_group G) (tg' : topological_group G) (h : nhds 1 = nhds 1) :
t = t'
theorem topological_add_group.ext {G : Type u_1} [add_group G] {t t' : topological_space G} (tg : topological_add_group G) (tg' : topological_add_group G) (h : nhds 0 = nhds 0) :
t = t'
theorem topological_group.ext_iff {G : Type u_1} [group G] {t t' : topological_space G} (tg : topological_group G) (tg' : topological_group G) :
t = t' nhds 1 = nhds 1
theorem has_continuous_inv.of_nhds_one {G : Type u_1} [group G] [topological_space G] (hinv : filter.tendsto (λ (x : G), x⁻¹) (nhds 1) (nhds 1)) (hleft : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ * x) (nhds 1)) (hconj : (x₀ : G), filter.tendsto (λ (x : G), x₀ * x * x₀⁻¹) (nhds 1) (nhds 1)) :
theorem has_continuous_neg.of_nhds_zero {G : Type u_1} [add_group G] [topological_space G] (hinv : filter.tendsto (λ (x : G), -x) (nhds 0) (nhds 0)) (hleft : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ + x) (nhds 0)) (hconj : (x₀ : G), filter.tendsto (λ (x : G), x₀ + x + -x₀) (nhds 0) (nhds 0)) :
theorem topological_group.of_nhds_one' {G : Type u} [group G] [topological_space G] (hmul : filter.tendsto (function.uncurry has_mul.mul) ((nhds 1).prod (nhds 1)) (nhds 1)) (hinv : filter.tendsto (λ (x : G), x⁻¹) (nhds 1) (nhds 1)) (hleft : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ * x) (nhds 1)) (hright : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x * x₀) (nhds 1)) :
theorem topological_add_group.of_nhds_zero' {G : Type u} [add_group G] [topological_space G] (hmul : filter.tendsto (function.uncurry has_add.add) ((nhds 0).prod (nhds 0)) (nhds 0)) (hinv : filter.tendsto (λ (x : G), -x) (nhds 0) (nhds 0)) (hleft : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ + x) (nhds 0)) (hright : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x + x₀) (nhds 0)) :
theorem topological_add_group.of_nhds_zero {G : Type u} [add_group G] [topological_space G] (hmul : filter.tendsto (function.uncurry has_add.add) ((nhds 0).prod (nhds 0)) (nhds 0)) (hinv : filter.tendsto (λ (x : G), -x) (nhds 0) (nhds 0)) (hleft : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ + x) (nhds 0)) (hconj : (x₀ : G), filter.tendsto (λ (x : G), x₀ + x + -x₀) (nhds 0) (nhds 0)) :
theorem topological_group.of_nhds_one {G : Type u} [group G] [topological_space G] (hmul : filter.tendsto (function.uncurry has_mul.mul) ((nhds 1).prod (nhds 1)) (nhds 1)) (hinv : filter.tendsto (λ (x : G), x⁻¹) (nhds 1) (nhds 1)) (hleft : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ * x) (nhds 1)) (hconj : (x₀ : G), filter.tendsto (λ (x : G), x₀ * x * x₀⁻¹) (nhds 1) (nhds 1)) :
theorem topological_add_group.of_comm_of_nhds_zero {G : Type u} [add_comm_group G] [topological_space G] (hmul : filter.tendsto (function.uncurry has_add.add) ((nhds 0).prod (nhds 0)) (nhds 0)) (hinv : filter.tendsto (λ (x : G), -x) (nhds 0) (nhds 0)) (hleft : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ + x) (nhds 0)) :
theorem topological_group.of_comm_of_nhds_one {G : Type u} [comm_group G] [topological_space G] (hmul : filter.tendsto (function.uncurry has_mul.mul) ((nhds 1).prod (nhds 1)) (nhds 1)) (hinv : filter.tendsto (λ (x : G), x⁻¹) (nhds 1) (nhds 1)) (hleft : (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ * x) (nhds 1)) :
@[protected, instance]

Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient.

Neighborhoods in the quotient are precisely the map of neighborhoods in the prequotient.

Any first countable topological additive group has an antitone neighborhood basis u : ℕ → set G for which u (n + 1) + u (n + 1) ⊆ u n. The existence of such a neighborhood basis is a key tool for quotient_add_group.complete_space

Any first countable topological group has an antitone neighborhood basis u : ℕ → set G for which (u (n + 1)) ^ 2 ⊆ u n. The existence of such a neighborhood basis is a key tool for quotient_group.complete_space

@[protected, instance]

In a first countable topological additive group G with normal additive subgroup N, 0 : G ⧸ N has a countable neighborhood basis.

@[protected, instance]

In a first countable topological group G with normal subgroup N, 1 : G ⧸ N has a countable neighborhood basis.

@[class]
structure has_continuous_sub (G : Type u_1) [topological_space G] [has_sub G] :
Prop

A typeclass saying that λ p : G × G, p.1 - p.2 is a continuous function. This property automatically holds for topological additive groups but it also holds, e.g., for ℝ≥0.

Instances of this typeclass
@[class]
structure has_continuous_div (G : Type u_1) [topological_space G] [has_div G] :
Prop

A typeclass saying that λ p : G × G, p.1 / p.2 is a continuous function. This property automatically holds for topological groups. Lemmas using this class have primes. The unprimed version is for group_with_zero.

Instances of this typeclass
theorem filter.tendsto.div' {α : Type u} {G : Type w} [topological_space G] [has_div G] [has_continuous_div G] {f g : α G} {l : filter α} {a b : G} (hf : filter.tendsto f l (nhds a)) (hg : filter.tendsto g l (nhds b)) :
filter.tendsto (λ (x : α), f x / g x) l (nhds (a / b))
theorem filter.tendsto.sub {α : Type u} {G : Type w} [topological_space G] [has_sub G] [has_continuous_sub G] {f g : α G} {l : filter α} {a b : G} (hf : filter.tendsto f l (nhds a)) (hg : filter.tendsto g l (nhds b)) :
filter.tendsto (λ (x : α), f x - g x) l (nhds (a - b))
theorem filter.tendsto.const_sub {α : Type u} {G : Type w} [topological_space G] [has_sub G] [has_continuous_sub G] (b : G) {c : G} {f : α G} {l : filter α} (h : filter.tendsto f l (nhds c)) :
filter.tendsto (λ (k : α), b - f k) l (nhds (b - c))
theorem filter.tendsto.const_div' {α : Type u} {G : Type w} [topological_space G] [has_div G] [has_continuous_div G] (b : G) {c : G} {f : α G} {l : filter α} (h : filter.tendsto f l (nhds c)) :
filter.tendsto (λ (k : α), b / f k) l (nhds (b / c))
theorem filter.tendsto.div_const' {α : Type u} {G : Type w} [topological_space G] [has_div G] [has_continuous_div G] (b : G) {c : G} {f : α G} {l : filter α} (h : filter.tendsto f l (nhds c)) :
filter.tendsto (λ (k : α), f k / b) l (nhds (c / b))
theorem filter.tendsto.sub_const {α : Type u} {G : Type w} [topological_space G] [has_sub G] [has_continuous_sub G] (b : G) {c : G} {f : α G} {l : filter α} (h : filter.tendsto f l (nhds c)) :
filter.tendsto (λ (k : α), f k - b) l (nhds (c - b))
@[continuity]
theorem continuous.div' {α : Type u} {G : Type w} [topological_space G] [has_div G] [has_continuous_div G] [topological_space α] {f g : α G} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : α), f x / g x)
@[continuity]
theorem continuous.sub {α : Type u} {G : Type w} [topological_space G] [has_sub G] [has_continuous_sub G] [topological_space α] {f g : α G} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : α), f x - g x)
theorem continuous_sub_left {G : Type w} [topological_space G] [has_sub G] [has_continuous_sub G] (a : G) :
continuous (λ (b : G), a - b)
theorem continuous_div_left' {G : Type w} [topological_space G] [has_div G] [has_continuous_div G] (a : G) :
continuous (λ (b : G), a / b)
theorem continuous_sub_right {G : Type w} [topological_space G] [has_sub G] [has_continuous_sub G] (a : G) :
continuous (λ (b : G), b - a)
theorem continuous_div_right' {G : Type w} [topological_space G] [has_div G] [has_continuous_div G] (a : G) :
continuous (λ (b : G), b / a)
theorem continuous_at.div' {α : Type u} {G : Type w} [topological_space G] [has_div G] [has_continuous_div G] [topological_space α] {f g : α G} {x : α} (hf : continuous_at f x) (hg : continuous_at g x) :
continuous_at (λ (x : α), f x / g x) x
theorem continuous_at.sub {α : Type u} {G : Type w} [topological_space G] [has_sub G] [has_continuous_sub G] [topological_space α] {f g : α G} {x : α} (hf : continuous_at f x) (hg : continuous_at g x) :
continuous_at (λ (x : α), f x - g x) x
theorem continuous_within_at.sub {α : Type u} {G : Type w} [topological_space G] [has_sub G] [has_continuous_sub G] [topological_space α] {f g : α G} {s : set α} {x : α} (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) :
continuous_within_at (λ (x : α), f x - g x) s x
theorem continuous_within_at.div' {α : Type u} {G : Type w} [topological_space G] [has_div G] [has_continuous_div G] [topological_space α] {f g : α G} {s : set α} {x : α} (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) :
continuous_within_at (λ (x : α), f x / g x) s x
theorem continuous_on.sub {α : Type u} {G : Type w} [topological_space G] [has_sub G] [has_continuous_sub G] [topological_space α] {f g : α G} {s : set α} (hf : continuous_on f s) (hg : continuous_on g s) :
continuous_on (λ (x : α), f x - g x) s
theorem continuous_on.div' {α : Type u} {G : Type w} [topological_space G] [has_div G] [has_continuous_div G] [topological_space α] {f g : α G} {s : set α} (hf : continuous_on f s) (hg : continuous_on g s) :
continuous_on (λ (x : α), f x / g x) s
@[simp]
def homeomorph.div_left {G : Type w} [group G] [topological_space G] [topological_group G] (x : G) :
G ≃ₜ G

A version of homeomorph.mul_left a b⁻¹ that is defeq to a / b.

Equations

A version of homeomorph.add_left a (-b) that is defeq to a - b.

Equations
@[simp]
@[simp]
@[simp]
theorem homeomorph.div_left_apply {G : Type w} [group G] [topological_space G] [topological_group G] (x ᾰ : G) :
(homeomorph.div_left x) = x /
@[simp]
@[simp]
theorem homeomorph.div_right_symm_apply {G : Type w} [group G] [topological_space G] [topological_group G] (x ᾰ : G) :
@[simp]
@[simp]
theorem homeomorph.div_right_apply {G : Type w} [group G] [topological_space G] [topological_group G] (x ᾰ : G) :
def homeomorph.div_right {G : Type w} [group G] [topological_space G] [topological_group G] (x : G) :
G ≃ₜ G

A version of homeomorph.mul_right a⁻¹ b that is defeq to b / a.

Equations
theorem is_open_map_sub_right {G : Type w} [add_group G] [topological_space G] [topological_add_group G] (a : G) :
is_open_map (λ (x : G), x - a)
theorem is_open_map_div_right {G : Type w} [group G] [topological_space G] [topological_group G] (a : G) :
is_open_map (λ (x : G), x / a)
theorem is_closed_map_sub_right {G : Type w} [add_group G] [topological_space G] [topological_add_group G] (a : G) :
is_closed_map (λ (x : G), x - a)
theorem is_closed_map_div_right {G : Type w} [group G] [topological_space G] [topological_group G] (a : G) :
is_closed_map (λ (x : G), x / a)
theorem tendsto_div_nhds_one_iff {G : Type w} [group G] [topological_space G] [topological_group G] {α : Type u_1} {l : filter α} {x : G} {u : α G} :
filter.tendsto (λ (n : α), u n / x) l (nhds 1) filter.tendsto u l (nhds x)
theorem tendsto_sub_nhds_zero_iff {G : Type w} [add_group G] [topological_space G] [topological_add_group G] {α : Type u_1} {l : filter α} {x : G} {u : α G} :
filter.tendsto (λ (n : α), u n - x) l (nhds 0) filter.tendsto u l (nhds x)
theorem nhds_translation_div {G : Type w} [group G] [topological_space G] [topological_group G] (x : G) :
filter.comap (λ (_x : G), _x / x) (nhds 1) = nhds x
theorem nhds_translation_sub {G : Type w} [add_group G] [topological_space G] [topological_add_group G] (x : G) :
filter.comap (λ (_x : G), _x - x) (nhds 0) = nhds x

Topological operations on pointwise sums and products #

A few results about interior and closure of the pointwise addition/multiplication of sets in groups with continuous addition/multiplication. See also submonoid.top_closure_mul_self_eq in topology.algebra.monoid.

theorem is_open.vadd_left {α : Type u} {β : Type v} [topological_space β] [add_group α] [add_action α β] [has_continuous_const_vadd α β] {s : set α} {t : set β} (ht : is_open t) :
theorem is_open.smul_left {α : Type u} {β : Type v} [topological_space β] [group α] [mul_action α β] [has_continuous_const_smul α β] {s : set α} {t : set β} (ht : is_open t) :
is_open (s t)
theorem subset_interior_smul_right {α : Type u} {β : Type v} [topological_space β] [group α] [mul_action α β] [has_continuous_const_smul α β] {s : set α} {t : set β} :
theorem subset_interior_vadd_right {α : Type u} {β : Type v} [topological_space β] [add_group α] [add_action α β] [has_continuous_const_vadd α β] {s : set α} {t : set β} :
theorem vadd_mem_nhds {α : Type u} {β : Type v} [topological_space β] [add_group α] [add_action α β] [has_continuous_const_vadd α β] {t : set β} (a : α) {x : β} (ht : t nhds x) :
a +ᵥ t nhds (a +ᵥ x)
theorem smul_mem_nhds {α : Type u} {β : Type v} [topological_space β] [group α] [mul_action α β] [has_continuous_const_smul α β] {t : set β} (a : α) {x : β} (ht : t nhds x) :
a t nhds (a x)
theorem subset_interior_smul {α : Type u} {β : Type v} [topological_space β] [group α] [mul_action α β] [has_continuous_const_smul α β] {s : set α} {t : set β} [topological_space α] :
theorem subset_interior_vadd {α : Type u} {β : Type v} [topological_space β] [add_group α] [add_action α β] [has_continuous_const_vadd α β] {s : set α} {t : set β} [topological_space α] :
theorem is_open.mul_left {α : Type u} [topological_space α] [group α] [has_continuous_const_smul α α] {s t : set α} :
theorem is_open.add_left {α : Type u} [topological_space α] [add_group α] [has_continuous_const_vadd α α] {s t : set α} :
theorem subset_interior_mul_right {α : Type u} [topological_space α] [group α] [has_continuous_const_smul α α] {s t : set α} :
s * interior t interior (s * t)
theorem subset_interior_mul {α : Type u} [topological_space α] [group α] [has_continuous_const_smul α α] {s t : set α} :
theorem singleton_mul_mem_nhds {α : Type u} [topological_space α] [group α] [has_continuous_const_smul α α] {s : set α} (a : α) {b : α} (h : s nhds b) :
{a} * s nhds (a * b)
theorem singleton_add_mem_nhds {α : Type u} [topological_space α] [add_group α] [has_continuous_const_vadd α α] {s : set α} (a : α) {b : α} (h : s nhds b) :
{a} + s nhds (a + b)
theorem singleton_mul_mem_nhds_of_nhds_one {α : Type u} [topological_space α] [group α] [has_continuous_const_smul α α] {s : set α} (a : α) (h : s nhds 1) :
{a} * s nhds a
theorem singleton_add_mem_nhds_of_nhds_zero {α : Type u} [topological_space α] [add_group α] [has_continuous_const_vadd α α] {s : set α} (a : α) (h : s nhds 0) :
{a} + s nhds a
theorem is_open.mul_right {α : Type u} [topological_space α] [group α] [has_continuous_const_smul αᵐᵒᵖ α] {s t : set α} (hs : is_open s) :
is_open (s * t)
theorem is_open.add_right {α : Type u} [topological_space α] [add_group α] [has_continuous_const_vadd αᵃᵒᵖ α] {s t : set α} (hs : is_open s) :
is_open (s + t)
theorem add_singleton_mem_nhds {α : Type u} [topological_space α] [add_group α] [has_continuous_const_vadd αᵃᵒᵖ α] {s : set α} (a : α) {b : α} (h : s nhds b) :
s + {a} nhds (b + a)
theorem mul_singleton_mem_nhds {α : Type u} [topological_space α] [group α] [has_continuous_const_smul αᵐᵒᵖ α] {s : set α} (a : α) {b : α} (h : s nhds b) :
s * {a} nhds (b * a)
theorem add_singleton_mem_nhds_of_nhds_zero {α : Type u} [topological_space α] [add_group α] [has_continuous_const_vadd αᵃᵒᵖ α] {s : set α} (a : α) (h : s nhds 0) :
s + {a} nhds a
theorem mul_singleton_mem_nhds_of_nhds_one {α : Type u} [topological_space α] [group α] [has_continuous_const_smul αᵐᵒᵖ α] {s : set α} (a : α) (h : s nhds 1) :
s * {a} nhds a
theorem is_open.div_left {α : Type u} [topological_space α] [group α] [topological_group α] {s t : set α} (ht : is_open t) :
is_open (s / t)
theorem is_open.sub_left {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {s t : set α} (ht : is_open t) :
is_open (s - t)
theorem is_open.div_right {α : Type u} [topological_space α] [group α] [topological_group α] {s t : set α} (hs : is_open s) :
is_open (s / t)
theorem is_open.sub_right {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {s t : set α} (hs : is_open s) :
is_open (s - t)
theorem subset_interior_div_left {α : Type u} [topological_space α] [group α] [topological_group α] {s t : set α} :
interior s / t interior (s / t)
theorem subset_interior_div_right {α : Type u} [topological_space α] [group α] [topological_group α] {s t : set α} :
s / interior t interior (s / t)
theorem subset_interior_div {α : Type u} [topological_space α] [group α] [topological_group α] {s t : set α} :
theorem is_open.mul_closure {α : Type u} [topological_space α] [group α] [topological_group α] {s : set α} (hs : is_open s) (t : set α) :
s * closure t = s * t
theorem is_open.add_closure {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {s : set α} (hs : is_open s) (t : set α) :
s + closure t = s + t
theorem is_open.closure_add {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {t : set α} (ht : is_open t) (s : set α) :
closure s + t = s + t
theorem is_open.closure_mul {α : Type u} [topological_space α] [group α] [topological_group α] {t : set α} (ht : is_open t) (s : set α) :
closure s * t = s * t
theorem is_open.sub_closure {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {s : set α} (hs : is_open s) (t : set α) :
s - closure t = s - t
theorem is_open.div_closure {α : Type u} [topological_space α] [group α] [topological_group α] {s : set α} (hs : is_open s) (t : set α) :
s / closure t = s / t
theorem is_open.closure_div {α : Type u} [topological_space α] [group α] [topological_group α] {t : set α} (ht : is_open t) (s : set α) :
closure s / t = s / t
theorem is_open.closure_sub {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {t : set α} (ht : is_open t) (s : set α) :
closure s - t = s - t
@[class]
structure add_group_with_zero_nhd (G : Type u) :

additive group with a neighbourhood around 0. Only used to construct a topology and uniform space.

This is currently only available for commutative groups, but it can be extended to non-commutative groups too.

Instances for add_group_with_zero_nhd
  • add_group_with_zero_nhd.has_sizeof_inst
@[protected, instance]

A subgroup S of a topological group G acts on G properly discontinuously on the left, if it is discrete in the sense that S ∩ K is finite for all compact K. (See also discrete_topology.)

A subgroup S of an additive topological group G acts on G properly discontinuously on the left, if it is discrete in the sense that S ∩ K is finite for all compact K. (See also discrete_topology.

A subgroup S of an additive topological group G acts on G properly discontinuously on the right, if it is discrete in the sense that S ∩ K is finite for all compact K. (See also discrete_topology.)

If G is Hausdorff, this can be combined with t2_space_of_properly_discontinuous_vadd_of_t2_space to show that the quotient group G ⧸ S is Hausdorff.

A subgroup S of a topological group G acts on G properly discontinuously on the right, if it is discrete in the sense that S ∩ K is finite for all compact K. (See also discrete_topology.)

If G is Hausdorff, this can be combined with t2_space_of_properly_discontinuous_smul_of_t2_space to show that the quotient group G ⧸ S is Hausdorff.

Some results about an open set containing the product of two sets in a topological group.

theorem compact_open_separated_add_right {G : Type w} [topological_space G] [add_group G] [topological_add_group G] {K U : set G} (hK : is_compact K) (hU : is_open U) (hKU : K U) :
(V : set G) (H : V nhds 0), K + V U

Given a compact set K inside an open set U, there is a open neighborhood V of 0 such that K + V ⊆ U.

theorem compact_open_separated_mul_right {G : Type w} [topological_space G] [group G] [topological_group G] {K U : set G} (hK : is_compact K) (hU : is_open U) (hKU : K U) :
(V : set G) (H : V nhds 1), K * V U

Given a compact set K inside an open set U, there is a open neighborhood V of 1 such that K * V ⊆ U.

theorem compact_open_separated_add_left {G : Type w} [topological_space G] [add_group G] [topological_add_group G] {K U : set G} (hK : is_compact K) (hU : is_open U) (hKU : K U) :
(V : set G) (H : V nhds 0), V + K U

Given a compact set K inside an open set U, there is a open neighborhood V of 0 such that V + K ⊆ U.

theorem compact_open_separated_mul_left {G : Type w} [topological_space G] [group G] [topological_group G] {K U : set G} (hK : is_compact K) (hU : is_open U) (hKU : K U) :
(V : set G) (H : V nhds 1), V * K U

Given a compact set K inside an open set U, there is a open neighborhood V of 1 such that V * K ⊆ U.

theorem compact_covered_by_add_left_translates {G : Type w} [topological_space G] [add_group G] [topological_add_group G] {K V : set G} (hK : is_compact K) (hV : (interior V).nonempty) :
(t : finset G), K (g : G) (H : g t), (λ (h : G), g + h) ⁻¹' V

A compact set is covered by finitely many left additive translates of a set with non-empty interior.

theorem compact_covered_by_mul_left_translates {G : Type w} [topological_space G] [group G] [topological_group G] {K V : set G} (hK : is_compact K) (hV : (interior V).nonempty) :
(t : finset G), K (g : G) (H : g t), (λ (h : G), g * h) ⁻¹' V

A compact set is covered by finitely many left multiplicative translates of a set with non-empty interior.

@[protected, instance]

Every locally compact separable topological group is σ-compact. Note: this is not true if we drop the topological group hypothesis.

@[protected, instance]

Every locally compact separable topological group is σ-compact. Note: this is not true if we drop the topological group hypothesis.

Given two compact sets in a noncompact additive topological group, there is a translate of the second one that is disjoint from the first one.

theorem exists_disjoint_smul_of_is_compact {G : Type w} [topological_space G] [group G] [topological_group G] [noncompact_space G] {K L : set G} (hK : is_compact K) (hL : is_compact L) :
(g : G), disjoint K (g L)

Given two compact sets in a noncompact topological group, there is a translate of the second one that is disjoint from the first one.

In a locally compact additive group, any neighborhood of the identity contains a compact closed neighborhood of the identity, even without separation assumptions on the space.

In a locally compact group, any neighborhood of the identity contains a compact closed neighborhood of the identity, even without separation assumptions on the space.

theorem nhds_mul {G : Type w} [topological_space G] [group G] [topological_group G] (x y : G) :
nhds (x * y) = nhds x * nhds y
theorem nhds_add {G : Type w} [topological_space G] [add_group G] [topological_add_group G] (x y : G) :
nhds (x + y) = nhds x + nhds y
@[simp]

On an additive topological group, 𝓝 : G → filter G can be promoted to an add_hom.

Equations

On a topological group, 𝓝 : G → filter G can be promoted to a mul_hom.

Equations