# 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 `equiv`s: `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} [add_group 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} [group G] (a : G) :
G ≃ₜ G

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

Equations
@[simp]
theorem homeomorph.coe_add_left {G : Type w} [add_group G] (a : G) :
@[simp]
theorem homeomorph.coe_mul_left {G : Type w} [group G] (a : G) :
theorem homeomorph.add_left_symm {G : Type w} [add_group G] (a : G) :
theorem homeomorph.mul_left_symm {G : Type w} [group G] (a : G) :
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)
@[protected]
def homeomorph.add_right {G : Type w} [add_group 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} [group 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} [group G] (a : G) :
= λ (g : G), g * a
@[simp]
theorem homeomorph.coe_add_right {G : Type w} [add_group G] (a : G) :
= λ (g : G), g + a
theorem homeomorph.mul_right_symm {G : Type w} [group G] (a : G) :
theorem homeomorph.add_right_symm {G : Type w} [add_group G] (a : G) :
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)
theorem is_open_map_sub_right {G : Type w} [add_group G] (a : G) :
is_open_map (λ (x : G), x - a)
theorem is_open_map_div_right {G : Type w} [group G] (a : G) :
is_open_map (λ (x : G), x / a)
theorem is_closed_map_sub_right {G : Type w} [add_group G] (a : G) :
is_closed_map (λ (x : G), x - a)
theorem is_closed_map_div_right {G : Type w} [group G] (a : G) :
is_closed_map (λ (x : G), x / a)
theorem discrete_topology_of_open_singleton_zero {G : Type w} [add_group G] (h : is_open {0}) :
theorem discrete_topology_of_open_singleton_one {G : Type w} [group G] (h : is_open {1}) :

### 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} [group α] {s t : set α} (ht : is_open t) :
is_open (s * t)
theorem is_open.add_left {α : Type u} [add_group α] {s t : set α} (ht : is_open t) :
is_open (s + t)
theorem is_open.mul_right {α : Type u} [group α] {s t : set α} (hs : is_open s) :
is_open (s * t)
theorem is_open.add_right {α : Type u} [add_group α] {s t : set α} (hs : is_open s) :
is_open (s + t)
theorem subset_interior_mul_left {α : Type u} [group α] {s t : set α} :
(interior s) * t interior (s * t)
theorem subset_interior_add_left {α : Type u} [add_group α] {s t : set α} :
+ t interior (s + t)
theorem subset_interior_add_right {α : Type u} [add_group α] {s t : set α} :
s + interior (s + t)
theorem subset_interior_mul_right {α : Type u} [group α] {s t : set α} :
s * interior (s * t)
theorem subset_interior_add {α : Type u} [add_group α] {s t : set α} :
interior (s + t)
theorem subset_interior_mul {α : Type u} [group α] {s t : set α} :
(interior s) * interior (s * t)

### 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} (h : (𝓝 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} (h : (𝓝 y)) :
filter.tendsto (λ (x : α), -f x) l (𝓝 (-y))
@[continuity]
theorem continuous.inv {α : Type u} {G : Type w} [group G] {f : α → G} (hf : continuous f) :
continuous (λ (x : α), (f x)⁻¹)
@[continuity]
theorem continuous.neg {α : Type u} {G : Type w} [add_group G] {f : α → G} (hf : continuous f) :
continuous (λ (x : α), -f x)
theorem continuous_at.neg {α : Type u} {G : Type w} [add_group G] {f : α → G} {x : α} (hf : x) :
continuous_at (λ (x : α), -f x) x
theorem continuous_at.inv {α : Type u} {G : Type w} [group G] {f : α → G} {x : α} (hf : x) :
continuous_at (λ (x : α), (f x)⁻¹) x
theorem continuous_on.inv {α : Type u} {G : Type w} [group G] {f : α → G} {s : set α} (hf : s) :
continuous_on (λ (x : α), (f x)⁻¹) s
theorem continuous_on.neg {α : Type u} {G : Type w} [add_group G] {f : α → G} {s : set α} (hf : s) :
continuous_on (λ (x : α), -f x) s
theorem continuous_within_at.inv {α : Type u} {G : Type w} [group G] {f : α → G} {s : set α} {x : α} (hf : x) :
continuous_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 : α} (hf : x) :
continuous_within_at (λ (x : α), -f x) s x
theorem tendsto_inv_nhds_within_Ioi {H : Type x} {a : H} :
theorem tendsto_neg_nhds_within_Ioi {H : Type x} {a : H} :
theorem tendsto_inv_nhds_within_Iio {H : Type x} {a : H} :
theorem tendsto_neg_nhds_within_Iio {H : Type x} {a : H} :
theorem tendsto_inv_nhds_within_Ioi_inv {H : Type x} {a : H} :
(𝓝[] a)
theorem tendsto_neg_nhds_within_Ioi_neg {H : Type x} {a : H} :
(𝓝[] a)
theorem tendsto_inv_nhds_within_Iio_inv {H : Type x} {a : H} :
(𝓝[] a)
theorem tendsto_neg_nhds_within_Iio_neg {H : Type x} {a : H} :
(𝓝[] a)
theorem tendsto_inv_nhds_within_Ici {H : Type x} {a : H} :
theorem tendsto_neg_nhds_within_Ici {H : Type x} {a : H} :
theorem tendsto_inv_nhds_within_Iic {H : Type x} {a : H} :
theorem tendsto_neg_nhds_within_Iic {H : Type x} {a : H} :
theorem tendsto_neg_nhds_within_Ici_neg {H : Type x} {a : H} :
(𝓝[] a)
theorem tendsto_inv_nhds_within_Ici_inv {H : Type x} {a : H} :
(𝓝[] a)
theorem tendsto_neg_nhds_within_Iic_neg {H : Type x} {a : H} :
(𝓝[] a)
theorem tendsto_inv_nhds_within_Iic_inv {H : Type x} {a : H} :
(𝓝[] a)
@[protected, instance]
@[protected, instance]
def prod.topological_group {G : Type w} {H : Type x} [group G] [group H]  :
@[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 (Π (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]
def homeomorph.neg (G : Type w) [add_group G]  :
G ≃ₜ G

Negation in a topological group as a homeomorphism.

Equations
@[protected]
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
@[protected]
def homeomorph.shear_mul_right (G : Type w) [group G]  :
G × G ≃ₜ G × G

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

Equations
@[protected]
G × G ≃ₜ G × G

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) [group G]  :
= λ (z : G × G), (z.fst, (z.fst) * z.snd)
@[simp]
= λ (z : G × G), (z.fst, z.fst + z.snd)
@[simp]
= λ (z : G × G), (z.fst, -z.fst + z.snd)
@[simp]
theorem homeomorph.shear_mul_right_symm_coe (G : Type w) [group G]  :
= λ (z : G × G), (z.fst, (z.fst)⁻¹ * z.snd)
theorem is_open.inv {G : Type w} [group G] {s : set G} (hs : is_open s) :
theorem is_open.neg {G : Type w} [add_group G] {s : set G} (hs : is_open s) :
theorem is_closed.neg {G : Type w} [add_group G] {s : set G} (hs : is_closed s) :
theorem is_closed.inv {G : Type w} [group G] {s : set G} (hs : is_closed s) :
@[protected, instance]
@[protected, instance]
def subgroup.topological_group {G : Type w} [group G] (S : subgroup G) :
theorem neg_closure {G : Type w} [add_group G] (s : set G) :
theorem inv_closure {G : Type w} [group G] (s : set G) :
def subgroup.topological_closure {G : Type w} [group G] (s : subgroup G) :

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
@[simp]
theorem subgroup.topological_closure_coe {G : Type w} [group G] {s : subgroup G} :
@[simp]
@[protected, instance]
@[protected, instance]
theorem subgroup.subgroup_topological_closure {G : Type w} [group G] (s : subgroup G) :
theorem subgroup.is_closed_topological_closure {G : Type w} [group G] (s : subgroup G) :
theorem add_subgroup.topological_closure_minimal {G : Type w} [add_group G] (s : add_subgroup G) {t : add_subgroup G} (h : s t) (ht : is_closed t) :
theorem subgroup.topological_closure_minimal {G : Type w} [group G] (s : subgroup G) {t : subgroup G} (h : s t) (ht : is_closed t) :
theorem dense_range.topological_closure_map_add_subgroup {G : Type w} {H : Type x} [add_group G] [add_group H] {f : G →+ H} (hf : continuous f) (hf' : dense_range f) {s : add_subgroup G} (hs : s.topological_closure = ) :
theorem dense_range.topological_closure_map_subgroup {G : Type w} {H : Type x} [group G] [group H] {f : G →* H} (hf : continuous f) (hf' : dense_range f) {s : subgroup G} (hs : s.topological_closure = ) :
theorem exists_nhds_half_neg {G : Type w} [add_group G] {s : set G} (hs : 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} (hs : 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
@[simp]
theorem map_add_left_nhds {G : Type w} [add_group G] (x y : G) :
(𝓝 y) = 𝓝 (x + y)
@[simp]
theorem map_mul_left_nhds {G : Type w} [group G] (x y : G) :
(𝓝 y) = 𝓝 (x * y)
theorem map_add_left_nhds_zero {G : Type w} [add_group G] (x : G) :
(𝓝 0) = 𝓝 x
theorem map_mul_left_nhds_one {G : Type w} [group G] (x : G) :
(𝓝 1) = 𝓝 x
theorem topological_group.ext {G : Type u_1} [group G] {t t' : topological_space G} (tg : topological_group G) (tg' : topological_group G) (h : 𝓝 1 = 𝓝 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 : 𝓝 0 = 𝓝 0) :
t = t'
theorem topological_group.of_nhds_aux {G : Type u_1} [group G] (hinv : filter.tendsto (λ (x : G), x⁻¹) (𝓝 1) (𝓝 1)) (hleft : ∀ (x₀ : G), 𝓝 x₀ = filter.map (λ (x : G), x₀ * x) (𝓝 1)) (hconj : ∀ (x₀ : G), filter.map (λ (x : G), (x₀ * x) * x₀⁻¹) (𝓝 1) 𝓝 1) :
continuous (λ (x : G), x⁻¹)
theorem topological_add_group.of_nhds_aux {G : Type u_1} [add_group G] (hinv : filter.tendsto (λ (x : G), -x) (𝓝 0) (𝓝 0)) (hleft : ∀ (x₀ : G), 𝓝 x₀ = filter.map (λ (x : G), x₀ + x) (𝓝 0)) (hconj : ∀ (x₀ : G), filter.map (λ (x : G), x₀ + x + -x₀) (𝓝 0) 𝓝 0) :
continuous (λ (x : G), -x)
theorem topological_group.of_nhds_one' {G : Type u} [group G] (hmul : (𝓝 1 ×ᶠ 𝓝 1) (𝓝 1)) (hinv : filter.tendsto (λ (x : G), x⁻¹) (𝓝 1) (𝓝 1)) (hleft : ∀ (x₀ : G), 𝓝 x₀ = filter.map (λ (x : G), x₀ * x) (𝓝 1)) (hright : ∀ (x₀ : G), 𝓝 x₀ = filter.map (λ (x : G), x * x₀) (𝓝 1)) :
theorem topological_add_group.of_nhds_zero' {G : Type u} [add_group G] (hmul : (𝓝 0 ×ᶠ 𝓝 0) (𝓝 0)) (hinv : filter.tendsto (λ (x : G), -x) (𝓝 0) (𝓝 0)) (hleft : ∀ (x₀ : G), 𝓝 x₀ = filter.map (λ (x : G), x₀ + x) (𝓝 0)) (hright : ∀ (x₀ : G), 𝓝 x₀ = filter.map (λ (x : G), x + x₀) (𝓝 0)) :
theorem topological_add_group.of_nhds_zero {G : Type u} [add_group G] (hmul : (𝓝 0 ×ᶠ 𝓝 0) (𝓝 0)) (hinv : filter.tendsto (λ (x : G), -x) (𝓝 0) (𝓝 0)) (hleft : ∀ (x₀ : G), 𝓝 x₀ = filter.map (λ (x : G), x₀ + x) (𝓝 0)) (hconj : ∀ (x₀ : G), filter.tendsto (λ (x : G), x₀ + x + -x₀) (𝓝 0) (𝓝 0)) :
theorem topological_group.of_nhds_one {G : Type u} [group G] (hmul : (𝓝 1 ×ᶠ 𝓝 1) (𝓝 1)) (hinv : filter.tendsto (λ (x : G), x⁻¹) (𝓝 1) (𝓝 1)) (hleft : ∀ (x₀ : G), 𝓝 x₀ = filter.map (λ (x : G), x₀ * x) (𝓝 1)) (hconj : ∀ (x₀ : G), filter.tendsto (λ (x : G), (x₀ * x) * x₀⁻¹) (𝓝 1) (𝓝 1)) :
theorem topological_add_group.of_comm_of_nhds_zero {G : Type u} (hmul : (𝓝 0 ×ᶠ 𝓝 0) (𝓝 0)) (hinv : filter.tendsto (λ (x : G), -x) (𝓝 0) (𝓝 0)) (hleft : ∀ (x₀ : G), 𝓝 x₀ = filter.map (λ (x : G), x₀ + x) (𝓝 0)) :
theorem topological_group.of_comm_of_nhds_one {G : Type u} [comm_group G] (hmul : (𝓝 1 ×ᶠ 𝓝 1) (𝓝 1)) (hinv : filter.tendsto (λ (x : G), x⁻¹) (𝓝 1) (𝓝 1)) (hleft : ∀ (x₀ : G), 𝓝 x₀ = filter.map (λ (x : G), x₀ * x) (𝓝 1)) :
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem quotient_group.is_open_map_coe {G : Type w} [group G] (N : subgroup G) :
@[protected, instance]
@[protected, 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
@[class]
structure has_continuous_div (G : Type u_1) [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
@[protected, instance]
@[protected, instance]
theorem filter.tendsto.div' {α : Type u} {G : Type w} [has_div G] {f g : α → G} {l : filter α} {a b : G} (hf : (𝓝 a)) (hg : (𝓝 b)) :
filter.tendsto (λ (x : α), f x / g x) l (𝓝 (a / b))
theorem filter.tendsto.sub {α : Type u} {G : Type w} [has_sub G] {f g : α → G} {l : filter α} {a b : G} (hf : (𝓝 a)) (hg : (𝓝 b)) :
filter.tendsto (λ (x : α), f x - g x) l (𝓝 (a - b))
theorem filter.tendsto.const_sub {α : Type u} {G : Type w} [has_sub G] (b : G) {c : G} {f : α → G} {l : filter α} (h : (𝓝 c)) :
filter.tendsto (λ (k : α), b - f k) l (𝓝 (b - c))
theorem filter.tendsto.const_div' {α : Type u} {G : Type w} [has_div G] (b : G) {c : G} {f : α → G} {l : filter α} (h : (𝓝 c)) :
filter.tendsto (λ (k : α), b / f k) l (𝓝 (b / c))
theorem filter.tendsto.div_const' {α : Type u} {G : Type w} [has_div G] (b : G) {c : G} {f : α → G} {l : filter α} (h : (𝓝 c)) :
filter.tendsto (λ (k : α), f k / b) l (𝓝 (c / b))
theorem filter.tendsto.sub_const {α : Type u} {G : Type w} [has_sub G] (b : G) {c : G} {f : α → G} {l : filter α} (h : (𝓝 c)) :
filter.tendsto (λ (k : α), f k - b) l (𝓝 (c - b))
@[continuity]
theorem continuous.div' {α : Type u} {G : Type w} [has_div G] {f g : α → G} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : α), f x / g x)
@[continuity]
theorem continuous.sub {α : Type u} {G : Type w} [has_sub G] {f g : α → G} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : α), f x - g x)
theorem continuous_sub_left {G : Type w} [has_sub G] (a : G) :
continuous (λ (b : G), a - b)
theorem continuous_div_left' {G : Type w} [has_div G] (a : G) :
continuous (λ (b : G), a / b)
theorem continuous_sub_right {G : Type w} [has_sub G] (a : G) :
continuous (λ (b : G), b - a)
theorem continuous_div_right' {G : Type w} [has_div G] (a : G) :
continuous (λ (b : G), b / a)
theorem continuous_at.div' {α : Type u} {G : Type w} [has_div G] {f g : α → G} {x : α} (hf : x) (hg : x) :
continuous_at (λ (x : α), f x / g x) x
theorem continuous_at.sub {α : Type u} {G : Type w} [has_sub G] {f g : α → G} {x : α} (hf : x) (hg : x) :
continuous_at (λ (x : α), f x - g x) x
theorem continuous_within_at.sub {α : Type u} {G : Type w} [has_sub G] {f g : α → G} {s : set α} {x : α} (hf : x) (hg : x) :
continuous_within_at (λ (x : α), f x - g x) s x
theorem continuous_within_at.div' {α : Type u} {G : Type w} [has_div G] {f g : α → G} {s : set α} {x : α} (hf : x) (hg : x) :
continuous_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 α} (hf : s) (hg : s) :
continuous_on (λ (x : α), f x - g x) s
theorem continuous_on.div' {α : Type u} {G : Type w} [has_div G] {f g : α → G} {s : set α} (hf : s) (hg : s) :
continuous_on (λ (x : α), f x / g x) s
theorem nhds_translation_div {G : Type w} [group G] (x : G) :
filter.comap (λ (y : G), y / x) (𝓝 1) = 𝓝 x
theorem nhds_translation_sub {G : Type w} [add_group G] (x : G) :
filter.comap (λ (y : G), y - x) (𝓝 0) = 𝓝 x
@[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.

theorem topological_add_group.t1_space (G : Type w) [add_group G] (h : is_closed {0}) :
theorem topological_group.t1_space (G : Type w) [group G] (h : 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} (hK : is_compact K) (hU : is_open U) (hKU : 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} (hK : is_compact K) (hU : is_open U) (hKU : 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} (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} [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]
@[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} [comm_group G] (x y : G) :
𝓝 (x * y) = (𝓝 x) * 𝓝 y
theorem nhds_add {G : Type w} (x y : G) :
𝓝 (x + y) = 𝓝 x + 𝓝 y
@[simp]
theorem nhds_mul_hom_apply {G : Type w} [comm_group G] (a : G) :
= 𝓝 a
def nhds_add_hom {G : Type w}  :
(filter G)

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

Equations
@[simp]
theorem nhds_add_hom_apply {G : Type w} (a : G) :
= 𝓝 a
def nhds_mul_hom {G : Type w} [comm_group G]  :
(filter G)

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

Equations
@[protected, instance]
def additive.topological_add_group {G : Type u_1} [h : topological_space G] [group G]  :
@[protected, instance]
def multiplicative.topological_group {G : Type u_1} [h : topological_space G] [add_group G]  :
@[protected, instance]
def units.topological_group {α : Type u} [monoid α]  :
def units.homeomorph.prod_units {α : Type u} {β : Type v} [monoid α] [monoid β]  :
× β)ˣ ≃ₜ αˣ × βˣ

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

Equations

### 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
• to_topological_space :
• to_topological_group :

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

Type u
• to_topological_space :

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

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.

theorem group_topology.continuous_inv' {α : Type u} [group α] (g : group_topology α) :

A version of the global `continuous_inv` suitable for dot notation.

@[ext]
theorem group_topology.ext' {α : Type u} [group α] {f g : group_topology α}  :
f = g
f = g
@[protected, instance]
def group_topology.partial_order {α : Type u} [group α] :

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]
Equations
@[simp]
theorem group_topology.to_topological_space_le {α : Type u} [group α] {x y : group_topology α} :
@[simp]
@[protected, instance]
def group_topology.has_top {α : Type u} [group α] :
Equations
@[protected, instance]
Equations
@[simp]
@[simp]
theorem group_topology.to_topological_space_top {α : Type u} [group α] :
@[protected, instance]
def group_topology.has_bot {α : Type u} [group α] :
Equations
@[protected, instance]
Equations
@[simp]
@[simp]
theorem group_topology.to_topological_space_bot {α : Type u} [group α] :
@[protected, instance]
def group_topology.bounded_order {α : Type u} [group α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def group_topology.has_inf {α : Type u} [group α] :
Equations
@[protected, instance]
Equations
@[simp]
@[simp]
theorem group_topology.to_topological_space_inf {α : Type u} [group α] (x y : group_topology α) :
@[protected, instance]
def group_topology.semilattice_inf {α : Type u} [group α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def group_topology.inhabited {α : Type u} [group α] :
Equations
@[protected, instance]
def group_topology.has_Inf {α : Type u} [group α] :
Equations
@[protected, instance]

Infimum of a collection of additive group topologies

Equations
@[simp]
theorem group_topology.to_topological_space_Inf {α : Type u} [group α] (s : set ) :
@[simp]
theorem add_group_topology.to_topological_space_Inf {α : Type u} [add_group α] (s : set ) :
@[simp]
theorem group_topology.to_topological_space_infi {α : Type u} [group α] {ι : Sort u_1} (s : ι → ) :
(⨅ (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 : ι → ) :
(⨅ (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
@[protected, instance]
Equations
@[protected, instance]
def group_topology.complete_lattice {α : Type u} [group α] :
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 : α → β) :