mathlib documentation

topology.algebra.group

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]
def homeomorph.add_left {G : Type w} [topological_space G] [add_group G] [has_continuous_add G] (a : G) :
G ≃ₜ G

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_add_coset {G : Type w} [topological_space G] [add_group G] [has_continuous_add G] {U : set G} (h : is_closed U) (x : G) :
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]
def homeomorph.add_right {G : Type w} [topological_space G] [add_group G] [has_continuous_add G] (a : G) :
G ≃ₜ G

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

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

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_open.right_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_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) :
theorem is_closed.right_add_coset {G : Type w} [topological_space G] [add_group G] [has_continuous_add 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 tendsto_neg {G : Type w} [topological_space G] [has_neg G] [has_continuous_neg G] (a : G) :
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))
@[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]
@[protected, instance]
@[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]
def pi.has_continuous_neg' {G : Type w} [topological_space G] [has_neg G] [has_continuous_neg G] {ι : Type u_1} :

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]
def pi.has_continuous_inv' {G : Type w} [topological_space G] [has_inv G] [has_continuous_inv G] {ι : Type u_1} :

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, instance]
theorem is_compact.neg {G : Type w} [topological_space G] [has_involutive_neg G] [has_continuous_neg G] {s : set G} (hs : is_compact s) :
@[protected]

Negation in a topological group as a homeomorphism.

Equations
@[protected]

Inversion in a topological group as a homeomorphism.

Equations
theorem is_open.inv {G : Type w} [topological_space G] [has_involutive_inv G] [has_continuous_inv G] {s : set G} (hs : is_open s) :
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 is_closed.neg {G : Type w} [topological_space G] [has_involutive_neg G] [has_continuous_neg G] {s : set G} (hs : is_closed s) :
theorem neg_closure {G : Type w} [topological_space G] [has_involutive_neg G] [has_continuous_neg G] (s : set G) :
theorem has_continuous_neg_Inf {G : Type w} [has_neg G] {ts : set (topological_space G)} (h : ∀ (t : topological_space G), t tshas_continuous_neg G) :
theorem has_continuous_inv_Inf {G : Type w} [has_inv G] {ts : set (topological_space G)} (h : ∀ (t : topological_space G), t tshas_continuous_inv G) :
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 has_continuous_inv_inf {G : Type w} [has_inv G] {t₁ t₂ : topological_space G} (h₁ : has_continuous_inv G) (h₂ : has_continuous_inv G) :
theorem has_continuous_neg_inf {G : Type w} [has_neg G] {t₁ t₂ : topological_space G} (h₁ : has_continuous_neg G) (h₂ : has_continuous_neg G) :

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.

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

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

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

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 αᵐᵒᵖ.

@[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
@[simp]
theorem homeomorph.shear_mul_right_coe (G : Type w) [topological_space G] [group G] [topological_group G] :
(homeomorph.shear_mul_right G) = λ (z : G × G), (z.fst, z.fst * z.snd)
@[simp]
@[simp]
@[protected, instance]

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

Equations
Instances for subgroup.topological_closure

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

Equations
Instances for add_subgroup.topological_closure

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

The connected component of 0 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 Vv - 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 Vv / 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) :
theorem map_mul_left_nhds_one {G : Type w} [topological_space G] [group G] [topological_group G] (x : G) :
theorem continuous_of_continuous_at_one {G : Type w} [topological_space G] [group G] [topological_group G] {M : Type u_1} {hom : Type u_2} [mul_one_class M] [topological_space M] [has_continuous_mul M] [monoid_hom_class hom G M] (f : hom) (hf : continuous_at f 1) :

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.

theorem continuous_of_continuous_at_zero {G : Type w} [topological_space G] [add_group G] [topological_add_group G] {M : Type u_1} {hom : Type u_2} [add_zero_class M] [topological_space M] [has_continuous_add M] [add_monoid_hom_class hom G M] (f : hom) (hf : continuous_at f 0) :

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.of_nhds_aux {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.map (λ (x : G), x₀ * x * x₀⁻¹) (nhds 1) nhds 1) :
continuous (λ (x : G), x⁻¹)
theorem topological_add_group.of_nhds_aux {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.map (λ (x : G), x₀ + x + -x₀) (nhds 0) nhds 0) :
continuous (λ (x : G), -x)
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]
@[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]
theorem homeomorph.sub_left_symm_apply {G : Type w} [add_group G] [topological_space G] [topological_add_group G] (x ᾰ : G) :
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
def homeomorph.sub_left {G : Type w} [add_group G] [topological_space G] [topological_add_group G] (x : G) :
G ≃ₜ G

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

Equations
@[simp]
theorem homeomorph.div_left_symm_apply {G : Type w} [group G] [topological_space G] [topological_group G] (x ᾰ : G) :
@[simp]
theorem homeomorph.sub_left_apply {G : Type w} [add_group G] [topological_space G] [topological_add_group G] (x ᾰ : G) :
(homeomorph.sub_left x) = x -
@[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]
theorem homeomorph.sub_right_symm_apply {G : Type w} [add_group G] [topological_space G] [topological_add_group G] (x ᾰ : G) :
@[simp]
theorem homeomorph.div_right_symm_apply {G : Type w} [group G] [topological_space G] [topological_group G] (x ᾰ : G) :
@[simp]
theorem homeomorph.sub_right_apply {G : Type w} [add_group G] [topological_space G] [topological_add_group G] (x ᾰ : G) :
@[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
def homeomorph.sub_right {G : Type w} [add_group G] [topological_space G] [topological_add_group G] (x : G) :
G ≃ₜ G

A version of homeomorph.add_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.mul_left {α : Type u} [topological_space α] [group α] [has_continuous_mul α] {s t : set α} (ht : is_open t) :
is_open (s * t)
theorem is_open.add_left {α : Type u} [topological_space α] [add_group α] [has_continuous_add α] {s t : set α} (ht : is_open t) :
is_open (s + t)
theorem is_open.mul_right {α : Type u} [topological_space α] [group α] [has_continuous_mul α] {s t : set α} (hs : is_open s) :
is_open (s * t)
theorem is_open.add_right {α : Type u} [topological_space α] [add_group α] [has_continuous_add α] {s t : set α} (hs : is_open s) :
is_open (s + t)
theorem subset_interior_mul_left {α : Type u} [topological_space α] [group α] [has_continuous_mul α] {s t : set α} :
interior s * t interior (s * t)
theorem subset_interior_add_left {α : Type u} [topological_space α] [add_group α] [has_continuous_add α] {s t : set α} :
interior s + t interior (s + t)
theorem subset_interior_add_right {α : Type u} [topological_space α] [add_group α] [has_continuous_add α] {s t : set α} :
s + interior t interior (s + t)
theorem subset_interior_mul_right {α : Type u} [topological_space α] [group α] [has_continuous_mul α] {s t : set α} :
s * interior t interior (s * t)
theorem subset_interior_add {α : Type u} [topological_space α] [add_group α] [has_continuous_add α] {s t : set α} :
theorem subset_interior_mul {α : Type u} [topological_space α] [group α] [has_continuous_mul α] {s t : set α} :
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_sub_left {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {s t : set α} :
interior s - t interior (s - t)
theorem subset_interior_sub_right {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {s t : set α} :
s - interior 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_sub {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {s t : set α} :
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) :
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]

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.

Every separated topological group in which there exists a compact set with nonempty interior is locally compact.

theorem nhds_mul {G : Type w} [topological_space G] [comm_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_comm_group G] [topological_add_group G] (x y : G) :
nhds (x + y) = nhds x + nhds y
@[simp]
theorem nhds_mul_hom_apply {G : Type w} [topological_space G] [comm_group G] [topological_group G] (a : G) :

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

Equations
@[simp]

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

Equations
@[protected, instance]
@[protected, instance]
theorem quotient_add_group.continuous_smul₁ {G : Type w} [add_group G] [topological_space G] [topological_add_group G] {Γ : add_subgroup G} (x : G Γ) :
continuous (λ (g : G), g +ᵥ x)
theorem quotient_group.continuous_smul₁ {G : Type w} [group G] [topological_space G] [topological_group G] {Γ : subgroup G} (x : G Γ) :
continuous (λ (g : G), g x)
@[protected, instance]
@[protected, instance]
def units.homeomorph.prod_units {α : Type u} {β : Type v} [monoid α] [topological_space α] [has_continuous_mul α] [monoid β] [topological_space β] [has_continuous_mul β] :
× β)ˣ ≃ₜ αˣ × βˣ

The topological group isomorphism between the units of a product of two monoids, and the product of the units of each monoid.

Equations
theorem topological_group_Inf {G : Type w} [group G] {ts : set (topological_space G)} (h : ∀ (t : topological_space G), t tstopological_group G) :
theorem topological_add_group_infi {G : Type w} {ι : Sort u_1} [add_group G] {ts' : ι → topological_space G} (h' : ∀ (i : ι), topological_add_group G) :
theorem topological_group_infi {G : Type w} {ι : Sort u_1} [group G] {ts' : ι → topological_space G} (h' : ∀ (i : ι), topological_group G) :
theorem topological_group_inf {G : Type w} [group G] {t₁ t₂ : topological_space G} (h₁ : topological_group G) (h₂ : topological_group G) :
theorem topological_group_induced {G : Type w} {H : Type x} [group G] [group H] {t : topological_space H} [topological_group H] {F : Type u_2} [monoid_hom_class F G H] (f : F) :
theorem topological_add_group_induced {G : Type w} {H : Type x} [add_group G] [add_group H] {t : topological_space H} [topological_add_group H] {F : Type u_2} [add_monoid_hom_class F G H] (f : F) :

Lattice of group topologies #

We define a type class group_topology α which endows a group α with a topology such that all group operations are continuous.

Group topologies on a fixed group α are ordered, by reverse inclusion. They form a complete lattice, with the discrete topology and the indiscrete topology.

Any function f : α → β induces coinduced f : topological_space α → group_topology β.

The additive version add_group_topology α and corresponding results are provided as well.

structure group_topology (α : Type u) [group α] :
Type u

A group topology on a group α is a topology for which multiplication and inversion are continuous.

Instances for group_topology
structure add_group_topology (α : Type u) [add_group α] :
Type u

An additive group topology on an additive group α is a topology for which addition and negation are continuous.

Instances for add_group_topology
theorem add_group_topology.continuous_add' {α : Type u} [add_group α] (g : add_group_topology α) :
continuous (λ (p : α × α), p.fst + p.snd)
theorem group_topology.continuous_mul' {α : Type u} [group α] (g : group_topology α) :
continuous (λ (p : α × α), p.fst * p.snd)

A version of the global continuous_mul suitable for dot notation.

A version of the global continuous_inv suitable for dot notation.

@[ext]
theorem group_topology.ext' {α : Type u} [group α] {f g : group_topology α} (h : f.to_topological_space.is_open = g.to_topological_space.is_open) :
f = g
@[protected, instance]

The ordering on group topologies on the group γ. t ≤ s if every set open in s is also open in t (t is finer than s).

Equations
@[protected, instance]
def group_topology.has_top {α : Type u} [group α] :
Equations
@[protected, instance]
def group_topology.has_bot {α : Type u} [group α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def group_topology.inhabited {α : Type u} [group α] :
Equations
@[protected, instance]

Infimum of a collection of additive group topologies

Equations
@[simp]
theorem group_topology.to_topological_space_infi {α : Type u} [group α] {ι : Sort u_1} (s : ι → group_topology α) :
(⨅ (i : ι), s i).to_topological_space = ⨅ (i : ι), (s i).to_topological_space
@[simp]
theorem add_group_topology.to_topological_space_infi {α : Type u} [add_group α] {ι : Sort u_1} (s : ι → add_group_topology α) :
(⨅ (i : ι), s i).to_topological_space = ⨅ (i : ι), (s i).to_topological_space
@[protected, instance]

Group topologies on γ form a complete lattice, with the discrete topology and the indiscrete topology.

The infimum of a collection of group topologies is the topology generated by all their open sets (which is a group topology).

The supremum of two group topologies s and t is the infimum of the family of all group topologies contained in the intersection of s and t.

Equations
def add_group_topology.coinduced {α : Type u_1} {β : Type u_2} [t : topological_space α] [add_group β] (f : α → β) :

Given f : α → β and a topology on α, the coinduced additive group topology on β is the finest topology such that f is continuous and β is a topological additive group.

Equations
def group_topology.coinduced {α : Type u_1} {β : Type u_2} [t : topological_space α] [group β] (f : α → β) :

Given f : α → β and a topology on α, the coinduced group topology on β is the finest topology such that f is continuous and β is a topological group.

Equations
theorem group_topology.coinduced_continuous {α : Type u_1} {β : Type u_2} [t : topological_space α] [group β] (f : α → β) :
theorem add_group_topology.coinduced_continuous {α : Type u_1} {β : Type u_2} [t : topological_space α] [add_group β] (f : α → β) :