mathlib documentation

topology.algebra.group

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

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.

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_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)
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.

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
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_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_open_map_sub_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_map_div_right {G : Type w} [topological_space G] [group G] [has_continuous_mul G] (a : G) :
is_open_map (λ (x : G), x / a)
theorem is_closed_map_sub_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_map_div_right {G : Type w} [topological_space G] [group G] [has_continuous_mul 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.

theorem filter.tendsto.inv {α : Type u} {G : Type w} [topological_space G] [group G] [topological_group G] {f : α → G} {l : filter α} {y : G} (h : filter.tendsto f l (𝓝 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} [topological_space G] [add_group G] [topological_add_group G] {f : α → G} {l : filter α} {y : G} (h : filter.tendsto f l (𝓝 y)) :
filter.tendsto (λ (x : α), -f x) l (𝓝 (-y))
theorem continuous.inv {α : Type u} {G : Type w} [topological_space G] [group G] [topological_group G] [topological_space α] {f : α → G} (hf : continuous f) :
continuous (λ (x : α), (f x)⁻¹)
theorem continuous.neg {α : Type u} {G : Type w} [topological_space G] [add_group G] [topological_add_group G] [topological_space α] {f : α → G} (hf : continuous f) :
continuous (λ (x : α), -f x)
theorem continuous_on.inv {α : Type u} {G : Type w} [topological_space G] [group G] [topological_group 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] [add_group G] [topological_add_group 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] [group G] [topological_group 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] [add_group G] [topological_add_group G] [topological_space α] {f : α → G} {s : set α} {x : α} (hf : continuous_within_at f s x) :
continuous_within_at (λ (x : α), -f x) s x
@[instance]
@[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)
@[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)

Negation in a topological group as a homeomorphism.

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

Inversion in a topological group as a homeomorphism.

Equations

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

Equations

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

@[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]
theorem neg_closure {G : Type w} [topological_space G] [add_group G] [topological_add_group G] (s : set G) :
theorem inv_closure {G : Type w} [topological_space G] [group G] [topological_group G] (s : set 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.

theorem exists_nhds_half_neg {G : Type w} [topological_space G] [add_group G] [topological_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} [topological_space G] [group G] [topological_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} [topological_space G] [add_group G] [topological_add_group G] (x : G) :
filter.comap (λ (y : G), y + -x) (𝓝 0) = 𝓝 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⁻¹) (𝓝 1) = 𝓝 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 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] [topological_space 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] [topological_space 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] [topological_space G] (hmul : filter.tendsto (function.uncurry has_mul.mul) (𝓝 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] [topological_space G] (hmul : filter.tendsto (function.uncurry has_add.add) (𝓝 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] [topological_space G] (hmul : filter.tendsto (function.uncurry has_add.add) (𝓝 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] [topological_space G] (hmul : filter.tendsto (function.uncurry has_mul.mul) (𝓝 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} [add_comm_group G] [topological_space G] (hmul : filter.tendsto (function.uncurry has_add.add) (𝓝 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] [topological_space G] (hmul : filter.tendsto (function.uncurry has_mul.mul) (𝓝 1 ×ᶠ 𝓝 1) (𝓝 1)) (hinv : filter.tendsto (λ (x : G), x⁻¹) (𝓝 1) (𝓝 1)) (hleft : ∀ (x₀ : G), 𝓝 x₀ = filter.map (λ (x : G), x₀ * x) (𝓝 1)) :
@[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
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 (𝓝 a)) (hg : filter.tendsto g l (𝓝 b)) :
filter.tendsto (λ (x : α), f x - g x) l (𝓝 (a - b))
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_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_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 nhds_translation {G : Type w} [topological_space G] [add_group G] [topological_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 is_open.mul_left {G : Type w} [topological_space G] [group G] [topological_group G] {s t : set G} :
is_open tis_open (s * t)
theorem is_open.add_left {G : Type w} [topological_space G] [add_group G] [topological_add_group G] {s t : set G} :
is_open tis_open (s + t)
theorem is_open.mul_right {G : Type w} [topological_space G] [group G] [topological_group G] {s t : set G} :
is_open sis_open (s * t)
theorem is_open.add_right {G : Type w} [topological_space G] [add_group G] [topological_add_group G] {s t : set G} :
is_open sis_open (s + t)

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

theorem compact_open_separated_add {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), is_open V 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} [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), is_open V 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} [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.

@[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) :
𝓝 (x * y) = (𝓝 x) * 𝓝 y
theorem nhds_add {G : Type w} [topological_space G] [add_comm_group G] [topological_add_group G] (x y : G) :
𝓝 (x + y) = 𝓝 x + 𝓝 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.

@[simp]

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

Equations