# mathlibdocumentation

topology.algebra.group

# Theory of topological groups

This file defines the following typeclasses:

• topological_group, topological_add_group: multiplicative and additive topological groups, i.e., groups with continuous (*) and (⁻¹) / (+) and (-);

• has_continuous_sub G means that G has a continuous subtraction operation.

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 (*).

G → G ≃ₜ G

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

def homeomorph.mul_left {G : Type w} [group G]  :
G → G ≃ₜ G

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

Equations
theorem is_open_map_add_left {G : Type w} [add_group G] (a : G) :
is_open_map (λ (x : G), a + x)

theorem is_open_map_mul_left {G : Type w} [group G] (a : G) :
is_open_map (λ (x : G), a * x)

theorem is_closed_map_mul_left {G : Type w} [group G] (a : G) :
is_closed_map (λ (x : G), a * x)

theorem is_closed_map_add_left {G : Type w} [add_group G] (a : G) :
is_closed_map (λ (x : G), a + x)

G → G ≃ₜ G

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

def homeomorph.mul_right {G : Type w} [group G]  :
G → G ≃ₜ G

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

Equations
theorem is_open_map_mul_right {G : Type w} [group G] (a : G) :
is_open_map (λ (x : G), x * a)

theorem is_open_map_add_right {G : Type w} [add_group G] (a : G) :
is_open_map (λ (x : G), x + a)

theorem is_closed_map_mul_right {G : Type w} [group G] (a : G) :
is_closed_map (λ (x : G), x * a)

theorem is_closed_map_add_right {G : Type w} [add_group G] (a : G) :
is_closed_map (λ (x : G), x + a)

### 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.

@[class]
Prop
• continuous_neg : continuous (λ (a : G), -a)

A topological (additive) group is a group in which the addition and negation operations are continuous.

Instances
@[class]
structure topological_group (G : Type u_1) [group G] :
Prop
• to_has_continuous_mul :
• continuous_inv :

A topological group is a group in which the multiplication and inversion operations are continuous.

Instances
theorem continuous_on_inv {G : Type w} [group G] {s : set G} :

theorem continuous_on_neg {G : Type w} [add_group G] {s : set G} :

theorem continuous_within_at_inv {G : Type w} [group G] {s : set G} {x : G} :

theorem continuous_within_at_neg {G : Type w} [add_group G] {s : set G} {x : G} :

theorem continuous_at_neg {G : Type w} [add_group G] {x : G} :

theorem continuous_at_inv {G : Type w} [group G] {x : G} :

theorem tendsto_inv {G : Type w} [group G] (a : G) :

theorem tendsto_neg {G : Type w} [add_group G] (a : G) :
(𝓝 (-a))

theorem filter.tendsto.inv {α : Type u} {G : Type w} [group G] {f : α → G} {l : filter α} {y : G} :
(𝓝 y)filter.tendsto (λ (x : α), (f x)⁻¹) l (𝓝 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} [add_group G] {f : α → G} {l : filter α} {y : G} :
(𝓝 y)filter.tendsto (λ (x : α), -f x) l (𝓝 (-y))

theorem continuous.inv {α : Type u} {G : Type w} [group G] {f : α → G} :
continuous (λ (x : α), (f x)⁻¹)

theorem continuous.neg {α : Type u} {G : Type w} [add_group G] {f : α → G} :
continuous (λ (x : α), -f x)

theorem continuous_on.inv {α : Type u} {G : Type w} [group G] {f : α → G} {s : set α} :
continuous_on (λ (x : α), (f x)⁻¹) s

theorem continuous_on.neg {α : Type u} {G : Type w} [add_group G] {f : α → G} {s : set α} :
continuous_on (λ (x : α), -f x) s

theorem continuous_within_at.inv {α : Type u} {G : Type w} [group G] {f : α → G} {s : set α} {x : α} :
xcontinuous_within_at (λ (x : α), (f x)⁻¹) s x

theorem continuous_within_at.neg {α : Type u} {G : Type w} [add_group G] {f : α → G} {s : set α} {x : α} :
xcontinuous_within_at (λ (x : α), -f x) s x

@[instance]

@[instance]
def prod.topological_group {G : Type w} {H : Type x} [group G] [group H]  :

def homeomorph.neg (G : Type w) [add_group G]  :
G ≃ₜ G

Negation in a topological group as a homeomorphism.

def homeomorph.inv (G : Type w) [group G]  :
G ≃ₜ G

Inversion in a topological group as a homeomorphism.

Equations
theorem nhds_one_symm (G : Type w) [group G]  :
= 𝓝 1

theorem nhds_zero_symm (G : Type w) [add_group G]  :
= 𝓝 0

theorem exists_nhds_half_neg {G : Type w} [add_group G] {s : set G} :
s 𝓝 0(∃ (V : set G) (H : V 𝓝 0), ∀ (v : G), v V∀ (w : G), w Vv + -w s)

theorem exists_nhds_split_inv {G : Type w} [group G] {s : set G} :
s 𝓝 1(∃ (V : set G) (H : V 𝓝 1), ∀ (v : G), v V∀ (w : G), w Vv * w⁻¹ s)

theorem nhds_translation_add_neg {G : Type w} [add_group G] (x : G) :
filter.comap (λ (y : G), y + -x) (𝓝 0) = 𝓝 x

theorem nhds_translation_mul_inv {G : Type w} [group G] (x : G) :
filter.comap (λ (y : G), y * x⁻¹) (𝓝 1) = 𝓝 x

theorem topological_group.ext {G : Type u_1} [group G] {t t' : topological_space G} :
𝓝 1 = 𝓝 1t = t'

theorem topological_add_group.ext {G : Type u_1} [add_group G] {t t' : topological_space G} :
𝓝 0 = 𝓝 0t = t'

@[instance]
def quotient_group.quotient.topological_space {G : Type u_1} [group G] (N : subgroup G) :

Equations
@[instance]

theorem quotient_group.is_open_map_coe {G : Type w} [group G] (N : subgroup G) :

@[instance]

@[instance]
def topological_group_quotient {G : Type w} [group G] (N : subgroup G) [N.normal] :

@[class]
structure has_continuous_sub (G : Type u_1) [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
@[instance]

theorem filter.tendsto.sub {α : Type u} {G : Type w} [has_sub G] {f g : α → G} {l : filter α} {a b : G} :
(𝓝 a) (𝓝 b)filter.tendsto (λ (x : α), f x - g x) l (𝓝 (a - b))

theorem continuous.sub {α : Type u} {G : Type w} [has_sub G] {f g : α → G} :
continuous (λ (x : α), f x - g x)

theorem continuous_within_at.sub {α : Type u} {G : Type w} [has_sub G] {f g : α → G} {s : set α} {x : α} :
x xcontinuous_within_at (λ (x : α), f x - g x) s x

theorem continuous_on.sub {α : Type u} {G : Type w} [has_sub G] {f g : α → G} {s : set α} :
continuous_on (λ (x : α), f x - g x) s

theorem nhds_translation {G : Type w} [add_group G] (x : G) :
filter.comap (λ (y : G), y - x) (𝓝 0) = 𝓝 x

@[class]
Type uType 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.

@[instance]

Equations
theorem add_group_with_zero_nhd.neg_Z {G : Type w}  :
filter.tendsto (λ (a : G), -a)

filter.tendsto (λ (p : G × G), p.fst + p.snd)

theorem add_group_with_zero_nhd.exists_Z_half {G : Type w} {s : set G} :
(∃ (V : set G) (H : , ∀ (v : G), v V∀ (w : G), w Vv + w s)

theorem add_group_with_zero_nhd.nhds_eq {G : Type w} (a : G) :
𝓝 a = filter.map (λ (x : G), x + a)

@[instance]

@[instance]

theorem is_open.mul_left {G : Type w} [group G] {s t : set G} :
is_open (s * t)

theorem is_open.add_left {G : Type w} [add_group G] {s t : set G} :
is_open (s + t)

theorem is_open.mul_right {G : Type w} [group G] {s t : set G} :
is_open (s * t)

theorem is_open.add_right {G : Type w} [add_group G] {s t : set G} :
is_open (s + t)

theorem topological_group.t1_space (G : Type w) [group G]  :
is_closed {1}

theorem topological_group.regular_space (G : Type w) [group G] [t1_space G] :

theorem topological_group.t2_space (G : Type w) [group G] [t1_space G] :

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

theorem compact_open_separated_add {G : Type w} [add_group G] {K U : set G} :
K U(∃ (V : set G), 0 V 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 {G : Type w} [group G] {K U : set G} :
K U(∃ (V : set G), 1 V K * V U)

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

theorem compact_covered_by_add_left_translates {G : Type w} [add_group G] {K V : set G} :
(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} [group G] {K V : set G} :
(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.

theorem nhds_mul {G : Type w} [comm_group G] (x y : G) :
𝓝 (x * y) = (𝓝 x) * 𝓝 y

theorem nhds_add {G : Type w} (x y : G) :
𝓝 (x + y) = 𝓝 x + 𝓝 y

theorem nhds_is_add_hom {G : Type w}  :
is_add_hom (λ (x : G), 𝓝 x)

theorem nhds_is_mul_hom {G : Type w} [comm_group G]  :
is_mul_hom (λ (x : G), 𝓝 x)