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

source

def homeomorph.add_left {G : Type w} [topological_space G] [add_group G] [has_continuous_add G] :

G → G ≃ₜ G

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

source

def homeomorph.mul_left {G : Type w} [topological_space G] [group G] [has_continuous_mul G] :

G → G ≃ₜ G

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

Equations

homeomorph.mul_left a = {to_equiv := {to_fun := (equiv.mul_left a).to_fun, inv_fun := (equiv.mul_left a).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}

source

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)

source

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)

source

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)

source

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)

source

def homeomorph.add_right {G : Type w} [topological_space G] [add_group G] [has_continuous_add G] :

G → G ≃ₜ G

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

source

def homeomorph.mul_right {G : Type w} [topological_space G] [group G] [has_continuous_mul G] :

G → G ≃ₜ G

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

Equations

homeomorph.mul_right a = {to_equiv := {to_fun := (equiv.mul_right a).to_fun, inv_fun := (equiv.mul_right a).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}

source

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)

source

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)

source

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)

source

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)

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.

source

@[class]

structure topological_add_group (G : Type u) [topological_space G] [add_group G] :

Prop

to_has_continuous_add : has_continuous_add G
continuous_neg : continuous (λ (a : G), -a)

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

Instances

source

@[class]

structure topological_group (G : Type u_1) [topological_space G] [group G] :

Prop

to_has_continuous_mul : has_continuous_mul G
continuous_inv : continuous has_inv.inv

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

Instances

source

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

continuous_on has_inv.inv s

source

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

continuous_on has_neg.neg s

source

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

continuous_within_at has_inv.inv s x

source

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

continuous_within_at has_neg.neg s x

source

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

continuous_at has_neg.neg x

source

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

continuous_at has_inv.inv x

source

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

filter.tendsto has_inv.inv (𝓝 a) (𝓝 a⁻¹)

source

theorem tendsto_neg {G : Type w} [topological_space G] [add_group G] [topological_add_group G] (a : G) :

filter.tendsto has_neg.neg (𝓝 a) (𝓝 (-a))

source

theorem filter.tendsto.inv {α : Type u} {G : Type w} [topological_space G] [group G] [topological_group G] {f : α → G} {l : filter α} {y : G} :

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

source

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} :

filter.tendsto f l (𝓝 y) → filter.tendsto (λ (x : α), -f x) l (𝓝 (-y))

source

theorem continuous.inv {α : Type u} {G : Type w} [topological_space G] [group G] [topological_group G] [topological_space α] {f : α → G} :

continuous f → continuous (λ (x : α), (f x)⁻¹)

source

theorem continuous.neg {α : Type u} {G : Type w} [topological_space G] [add_group G] [topological_add_group G] [topological_space α] {f : α → G} :

continuous f → continuous (λ (x : α), -f x)

source

theorem continuous_on.inv {α : Type u} {G : Type w} [topological_space G] [group G] [topological_group G] [topological_space α] {f : α → G} {s : set α} :

continuous_on f s → continuous_on (λ (x : α), (f x)⁻¹) s

source

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 α} :

continuous_on f s → continuous_on (λ (x : α), -f x) s

source

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 : α} :

continuous_within_at f s x → continuous_within_at (λ (x : α), (f x)⁻¹) s x

source

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 : α} :

continuous_within_at f s x → continuous_within_at (λ (x : α), -f x) s x

source

@[instance]

def prod.topological_add_group {G : Type w} {H : Type x} [topological_space G] [add_group G] [topological_add_group G] [topological_space H] [add_group H] [topological_add_group H] :

topological_add_group (G × H)

source

@[instance]

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

topological_group (G × H)

source

def homeomorph.neg (G : Type w) [topological_space G] [add_group G] [topological_add_group G] :

G ≃ₜ G

Negation in a topological group as a homeomorphism.

source

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

homeomorph.inv G = {to_equiv := {to_fun := (equiv.inv G).to_fun, inv_fun := (equiv.inv G).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}

source

theorem nhds_one_symm (G : Type w) [topological_space G] [group G] [topological_group G] :

filter.comap has_inv.inv (𝓝 1) = 𝓝 1

source

theorem nhds_zero_symm (G : Type w) [topological_space G] [add_group G] [topological_add_group G] :

filter.comap has_neg.neg (𝓝 0) = 𝓝 0

source

theorem exists_nhds_half_neg {G : Type w} [topological_space G] [add_group G] [topological_add_group G] {s : set G} :

s ∈ 𝓝 0 → (∃ (V : set G) (H : V ∈ 𝓝 0), ∀ (v : G), v ∈ V → ∀ (w : G), w ∈ V → v + -w ∈ s)

source

theorem exists_nhds_split_inv {G : Type w} [topological_space G] [group G] [topological_group G] {s : set G} :

s ∈ 𝓝 1 → (∃ (V : set G) (H : V ∈ 𝓝 1), ∀ (v : G), v ∈ V → ∀ (w : G), w ∈ V → v * w⁻¹ ∈ s)

source

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

source

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

source

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

topological_group G → topological_group G → 𝓝 1 = 𝓝 1 → t = t'

source

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

topological_add_group G → topological_add_group G → 𝓝 0 = 𝓝 0 → t = t'

source

@[instance]

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

topological_space (quotient_group.quotient N)

Equations

quotient_group.quotient.topological_space N = quotient.topological_space

source

@[instance]

def quotient_add_group.quotient.topological_space {G : Type u_1} [add_group G] [topological_space G] (N : add_subgroup G) :

topological_space (quotient_add_group.quotient N)

source

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

is_open_map coe

source

theorem quotient_add_group.is_open_map_coe {G : Type w} [topological_space G] [add_group G] [topological_add_group G] (N : add_subgroup G) :

is_open_map coe

source

@[instance]

def topological_add_group_quotient {G : Type w} [topological_space G] [add_group G] [topological_add_group G] (N : add_subgroup G) [N.normal] :

topological_add_group (quotient_add_group.quotient N)

source

@[instance]

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

topological_group (quotient_group.quotient N)

source

@[class]

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

Prop

continuous_sub : continuous (λ (p : G × G), p.fst - p.snd)

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

source

@[instance]

def topological_add_group.to_has_continuous_sub {G : Type w} [topological_space G] [add_group G] [topological_add_group G] :

has_continuous_sub G

source

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} :

filter.tendsto f l (𝓝 a) → filter.tendsto g l (𝓝 b) → filter.tendsto (λ (x : α), f x - g x) l (𝓝 (a - b))

source

theorem continuous.sub {α : Type u} {G : Type w} [topological_space G] [has_sub G] [has_continuous_sub G] [topological_space α] {f g : α → G} :

continuous f → continuous g → continuous (λ (x : α), f x - g x)

source

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 : α} :

continuous_within_at f s x → continuous_within_at g s x → continuous_within_at (λ (x : α), f x - g x) s x

source

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 α} :

continuous_on f s → continuous_on g s → continuous_on (λ (x : α), f x - g x) s

source

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

source

@[class]

structure add_group_with_zero_nhd :

Type u → Type u

to_add_comm_group : add_comm_group G
Z : filter G
zero_Z : pure 0 ≤ add_group_with_zero_nhd.Z G
sub_Z : filter.tendsto (λ (p : G × G), p.fst - p.snd) (add_group_with_zero_nhd.Z G ×ᶠ add_group_with_zero_nhd.Z G) (add_group_with_zero_nhd.Z G)

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.

source

@[instance]

def add_group_with_zero_nhd.topological_space (G : Type w) [add_group_with_zero_nhd G] :

topological_space G

Equations

add_group_with_zero_nhd.topological_space G = topological_space.mk_of_nhds (λ (a : G), filter.map (λ (x : G), x + a) (add_group_with_zero_nhd.Z G))

source

theorem add_group_with_zero_nhd.neg_Z {G : Type w} [add_group_with_zero_nhd G] :

filter.tendsto (λ (a : G), -a) (add_group_with_zero_nhd.Z G) (add_group_with_zero_nhd.Z G)

source

theorem add_group_with_zero_nhd.add_Z {G : Type w} [add_group_with_zero_nhd G] :

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

source

theorem add_group_with_zero_nhd.exists_Z_half {G : Type w} [add_group_with_zero_nhd G] {s : set G} :

s ∈ add_group_with_zero_nhd.Z G → (∃ (V : set G) (H : V ∈ add_group_with_zero_nhd.Z G), ∀ (v : G), v ∈ V → ∀ (w : G), w ∈ V → v + w ∈ s)

source

theorem add_group_with_zero_nhd.nhds_eq {G : Type w} [add_group_with_zero_nhd G] (a : G) :

𝓝 a = filter.map (λ (x : G), x + a) (add_group_with_zero_nhd.Z G)

source

theorem add_group_with_zero_nhd.nhds_zero_eq_Z {G : Type w} [add_group_with_zero_nhd G] :

𝓝 0 = add_group_with_zero_nhd.Z G

source

@[instance]

def add_group_with_zero_nhd.has_continuous_add {G : Type w} [add_group_with_zero_nhd G] :

has_continuous_add G

source

@[instance]

def add_group_with_zero_nhd.topological_add_group {G : Type w} [add_group_with_zero_nhd G] :

topological_add_group G

source

theorem is_open.mul_left {G : Type w} [topological_space G] [group G] [topological_group G] {s t : set G} :

is_open t → is_open (s * t)

source

theorem is_open.add_left {G : Type w} [topological_space G] [add_group G] [topological_add_group G] {s t : set G} :

is_open t → is_open (s + t)

source

theorem is_open.mul_right {G : Type w} [topological_space G] [group G] [topological_group G] {s t : set G} :

is_open s → is_open (s * t)

source

theorem is_open.add_right {G : Type w} [topological_space G] [add_group G] [topological_add_group G] {s t : set G} :

is_open s → is_open (s + t)

source

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

is_closed {1} → t1_space G

source

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

regular_space G

source

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

t2_space G

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

source

theorem compact_open_separated_add {G : Type w} [topological_space G] [add_group G] [topological_add_group G] {K U : set G} :

is_compact K → is_open U → 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.

source

theorem compact_open_separated_mul {G : Type w} [topological_space G] [group G] [topological_group G] {K U : set G} :

is_compact K → is_open U → 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.

source

theorem compact_covered_by_add_left_translates {G : Type w} [topological_space G] [add_group G] [topological_add_group G] {K V : set G} :

is_compact K → (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.

source

theorem compact_covered_by_mul_left_translates {G : Type w} [topological_space G] [group G] [topological_group G] {K V : set G} :

is_compact K → (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.

source

theorem nhds_mul {G : Type w} [topological_space G] [comm_group G] [topological_group G] (x y : G) :

𝓝 (x * y) = (𝓝 x) * 𝓝 y

source

theorem nhds_add {G : Type w} [topological_space G] [add_comm_group G] [topological_add_group G] (x y : G) :

𝓝 (x + y) = 𝓝 x + 𝓝 y

source

theorem nhds_is_add_hom {G : Type w} [topological_space G] [add_comm_group G] [topological_add_group G] :

is_add_hom (λ (x : G), 𝓝 x)

source

theorem nhds_is_mul_hom {G : Type w} [topological_space G] [comm_group G] [topological_group G] :

is_mul_hom (λ (x : G), 𝓝 x)