mathlib docs: topology.algebra.group

source

@[class]

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

Prop

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

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

Instances

source

@[class]

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

Prop

to_has_continuous_mul : has_continuous_mul α
continuous_inv : continuous (λ (a : α), a⁻¹)

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

Instances

source

theorem continuous_neg {α : Type u} [topological_space α] [add_group α] [topological_add_group α] :

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

source

theorem continuous_inv {α : Type u} [topological_space α] [group α] [topological_group α] :

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

source

theorem continuous.inv {α : Type u} {β : Type v} [topological_space α] [group α] [topological_group α] [topological_space β] {f : β → α} (hf : continuous f) :

continuous (λ (x : β), (f x)⁻¹)

source

theorem continuous.neg {α : Type u} {β : Type v} [topological_space α] [add_group α] [topological_add_group α] [topological_space β] {f : β → α} (hf : continuous f) :

continuous (λ (x : β), -f x)

source

theorem continuous_on_inv {α : Type u} [topological_space α] [group α] [topological_group α] {s : set α} :

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

source

theorem continuous_on_neg {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {s : set α} :

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

source

theorem continuous_on.inv {α : Type u} {β : Type v} [topological_space α] [group α] [topological_group α] [topological_space β] {f : β → α} {s : set β} (hf : continuous_on f s) :

continuous_on (λ (x : β), (f x)⁻¹) s

source

theorem continuous_on.neg {α : Type u} {β : Type v} [topological_space α] [add_group α] [topological_add_group α] [topological_space β] {f : β → α} {s : set β} (hf : continuous_on f s) :

continuous_on (λ (x : β), -f x) s

source

theorem tendsto_inv {α : Type u_1} [group α] [topological_space α] [topological_group α] (a : α) :

(λ (x : α), x⁻¹)→_{a}a⁻¹

source

theorem tendsto_neg {α : Type u_1} [add_group α] [topological_space α] [topological_add_group α] (a : α) :

(λ (x : α), -x)→_{a}-a

source

theorem filter.tendsto.inv {α : Type u} {β : Type v} [topological_space α] [group α] [topological_group α] {f : β → α} {x : filter β} {a : α} (hf : filter.tendsto f x (𝓝 a)) :

filter.tendsto (λ (x : β), (f x)⁻¹) x (𝓝 a⁻¹)

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} {β : Type v} [topological_space α] [add_group α] [topological_add_group α] {f : β → α} {x : filter β} {a : α} (hf : filter.tendsto f x (𝓝 a)) :

filter.tendsto (λ (x : β), -f x) x (𝓝 (-a))

source

theorem continuous_at.neg {α : Type u} {β : Type v} [topological_space α] [add_group α] [topological_add_group α] [topological_space β] {f : β → α} {x : β} (hf : continuous_at f x) :

continuous_at (λ (x : β), -f x) x

source

theorem continuous_at.inv {α : Type u} {β : Type v} [topological_space α] [group α] [topological_group α] [topological_space β] {f : β → α} {x : β} (hf : continuous_at f x) :

continuous_at (λ (x : β), (f x)⁻¹) x

source

theorem continuous_within_at.inv {α : Type u} {β : Type v} [topological_space α] [group α] [topological_group α] [topological_space β] {f : β → α} {s : set β} {x : β} (hf : continuous_within_at f s x) :

continuous_within_at (λ (x : β), (f x)⁻¹) s x

source

theorem continuous_within_at.neg {α : Type u} {β : Type v} [topological_space α] [add_group α] [topological_add_group α] [topological_space β] {f : β → α} {s : set β} {x : β} (hf : continuous_within_at f s x) :

continuous_within_at (λ (x : β), -f x) s x

source

@[instance]

def prod.topological_add_group {α : Type u} {β : Type v} [topological_space α] [add_group α] [topological_add_group α] [topological_space β] [add_group β] [topological_add_group β] :

topological_add_group (α × β)

source

@[instance]

def prod.topological_group {α : Type u} {β : Type v} [topological_space α] [group α] [topological_group α] [topological_space β] [group β] [topological_group β] :

topological_group (α × β)

source

def homeomorph.add_left {α : Type u} [topological_space α] [add_group α] [topological_add_group α] (a : α) :

α ≃ₜ α

source

def homeomorph.mul_left {α : Type u} [topological_space α] [group α] [topological_group α] (a : α) :

α ≃ₜ α

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 {α : Type u} [topological_space α] [add_group α] [topological_add_group α] (a : α) :

is_open_map (λ (x : α), a + x)

source

theorem is_open_map_mul_left {α : Type u} [topological_space α] [group α] [topological_group α] (a : α) :

is_open_map (λ (x : α), a * x)

source

theorem is_closed_map_mul_left {α : Type u} [topological_space α] [group α] [topological_group α] (a : α) :

is_closed_map (λ (x : α), a * x)

source

theorem is_closed_map_add_left {α : Type u} [topological_space α] [add_group α] [topological_add_group α] (a : α) :

is_closed_map (λ (x : α), a + x)

source

def homeomorph.add_right {α : Type u_1} [topological_space α] [add_group α] [topological_add_group α] (a : α) :

α ≃ₜ α

source

def homeomorph.mul_right {α : Type u_1} [topological_space α] [group α] [topological_group α] (a : α) :

α ≃ₜ α

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 {α : Type u} [topological_space α] [group α] [topological_group α] (a : α) :

is_open_map (λ (x : α), x * a)

source

theorem is_open_map_add_right {α : Type u} [topological_space α] [add_group α] [topological_add_group α] (a : α) :

is_open_map (λ (x : α), x + a)

source

theorem is_closed_map_mul_right {α : Type u} [topological_space α] [group α] [topological_group α] (a : α) :

is_closed_map (λ (x : α), x * a)

source

theorem is_closed_map_add_right {α : Type u} [topological_space α] [add_group α] [topological_add_group α] (a : α) :

is_closed_map (λ (x : α), x + a)

source

def homeomorph.neg (α : Type u_1) [topological_space α] [add_group α] [topological_add_group α] :

α ≃ₜ α

source

def homeomorph.inv (α : Type u_1) [topological_space α] [group α] [topological_group α] :

α ≃ₜ α

Equations

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

source

theorem exists_nhds_half {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {s : set α} (hs : s ∈ 𝓝 0) :

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

source

theorem exists_nhds_split {α : Type u} [topological_space α] [group α] [topological_group α] {s : set α} (hs : s ∈ 𝓝 1) :

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

source

theorem exists_nhds_half_neg {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {s : set α} (hs : s ∈ 𝓝 0) :

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

source

theorem exists_nhds_split_inv {α : Type u} [topological_space α] [group α] [topological_group α] {s : set α} (hs : s ∈ 𝓝 1) :

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

source

theorem exists_nhds_split4 {α : Type u} [topological_space α] [group α] [topological_group α] {u : set α} (hu : u ∈ 𝓝 1) :

∃ (V : set α) (H : V ∈ 𝓝 1), ∀ {v w s t : α}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → ((v * w) * s) * t ∈ u

source

theorem exists_nhds_quarter {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {u : set α} (hu : u ∈ 𝓝 0) :

∃ (V : set α) (H : V ∈ 𝓝 0), ∀ {v w s t : α}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v + w + s + t ∈ u

source

theorem nhds_one_symm (α : Type u) [topological_space α] [group α] [topological_group α] :

filter.comap (λ (r : α), r⁻¹) (𝓝 1) = 𝓝 1

source

theorem nhds_zero_symm (α : Type u) [topological_space α] [add_group α] [topological_add_group α] :

filter.comap (λ (r : α), -r) (𝓝 0) = 𝓝 0

source

theorem nhds_translation_add_neg {α : Type u} [topological_space α] [add_group α] [topological_add_group α] (x : α) :

filter.comap (λ (y : α), y + -x) (𝓝 0) = 𝓝 x

source

theorem nhds_translation_mul_inv {α : Type u} [topological_space α] [group α] [topological_group α] (x : α) :

filter.comap (λ (y : α), y * x⁻¹) (𝓝 1) = 𝓝 x

source

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'

source

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'

source

@[instance]

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

topological_space (quotient_group.quotient N)

Equations

quotient_group.quotient.topological_space N = id quotient.topological_space

source

@[instance]

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

topological_space (quotient_add_group.quotient N)

source

theorem quotient_add_group_saturate {α : Type u} [add_group α] (N : add_subgroup α) (s : set α) :

coe ⁻¹' (coe '' s) = ⋃ (x : ↥N), (λ (y : α), y + x.val) '' s

source

theorem quotient_group_saturate {α : Type u} [group α] (N : subgroup α) (s : set α) :

coe ⁻¹' (coe '' s) = ⋃ (x : ↥N), (λ (y : α), y * x.val) '' s

source

theorem quotient_group.open_coe {α : Type u} [topological_space α] [group α] [topological_group α] (N : subgroup α) :

is_open_map coe

source

theorem quotient_add_group.open_coe {α : Type u} [topological_space α] [add_group α] [topological_add_group α] (N : add_subgroup α) :

is_open_map coe

source

@[instance]

def topological_add_group_quotient {α : Type u} [topological_space α] [add_group α] [topological_add_group α] (N : add_subgroup α) (n : N.normal) :

topological_add_group (quotient_add_group.quotient N)

source

@[instance]

def topological_group_quotient {α : Type u} [topological_space α] [group α] [topological_group α] (N : subgroup α) (n : N.normal) :

topological_group (quotient_group.quotient N)

source

theorem continuous.sub {α : Type u} {β : Type v} [topological_space α] [add_group α] [topological_add_group α] [topological_space β] {f g : β → α} (hf : continuous f) (hg : continuous g) :

continuous (λ (x : β), f x - g x)

source

theorem continuous_sub {α : Type u} [topological_space α] [add_group α] [topological_add_group α] :

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

source

theorem continuous_on.sub {α : Type u} {β : Type v} [topological_space α] [add_group α] [topological_add_group α] [topological_space β] {f g : β → α} {s : set β} (hf : continuous_on f s) (hg : continuous_on g s) :

continuous_on (λ (x : β), f x - g x) s

source

theorem filter.tendsto.sub {α : Type u} {β : Type v} [topological_space α] [add_group α] [topological_add_group α] {f g : β → α} {x : filter β} {a b : α} (hf : filter.tendsto f x (𝓝 a)) (hg : filter.tendsto g x (𝓝 b)) :

filter.tendsto (λ (x : β), f x - g x) x (𝓝 (a - b))

source

theorem nhds_translation {α : Type u} [topological_space α] [add_group α] [topological_add_group α] (x : α) :

filter.comap (λ (y : α), y - x) (𝓝 0) = 𝓝 x

source

@[class]

structure add_group_with_zero_nhd (α : Type u) :

Type u

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

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 (α : Type u) [add_group_with_zero_nhd α] :

topological_space α

Equations

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

source

theorem add_group_with_zero_nhd.neg_Z {α : Type u} [add_group_with_zero_nhd α] :

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

source

theorem add_group_with_zero_nhd.add_Z {α : Type u} [add_group_with_zero_nhd α] :

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

source

theorem add_group_with_zero_nhd.exists_Z_half {α : Type u} [add_group_with_zero_nhd α] {s : set α} (hs : s ∈ add_group_with_zero_nhd.Z α) :

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

source

theorem add_group_with_zero_nhd.nhds_eq {α : Type u} [add_group_with_zero_nhd α] (a : α) :

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

source

theorem add_group_with_zero_nhd.nhds_zero_eq_Z {α : Type u} [add_group_with_zero_nhd α] :

𝓝 0 = add_group_with_zero_nhd.Z α

source

@[instance]

def add_group_with_zero_nhd.has_continuous_add {α : Type u} [add_group_with_zero_nhd α] :

has_continuous_add α

source

@[instance]

def add_group_with_zero_nhd.topological_add_group {α : Type u} [add_group_with_zero_nhd α] :

topological_add_group α

source

theorem is_open_add_left {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {s t : set α} (a : is_open t) :

is_open (s + t)

source

theorem is_open_mul_left {α : Type u} [topological_space α] [group α] [topological_group α] {s t : set α} (a : is_open t) :

is_open (s * t)

source

theorem is_open_mul_right {α : Type u} [topological_space α] [group α] [topological_group α] {s t : set α} (a : is_open s) :

is_open (s * t)

source

theorem is_open_add_right {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {s t : set α} (a : is_open s) :

is_open (s + t)

source

theorem topological_group.t1_space (α : Type u) [topological_space α] [group α] [topological_group α] (h : is_closed {1}) :

t1_space α

source

theorem topological_group.regular_space (α : Type u) [topological_space α] [group α] [topological_group α] [t1_space α] :

regular_space α

source

theorem topological_group.t2_space (α : Type u) [topological_space α] [group α] [topological_group α] [t1_space α] :

t2_space α

source

theorem one_open_separated_mul {α : Type u} [topological_space α] [group α] [topological_group α] {U : set α} (h1U : is_open U) (h2U : 1 ∈ U) :

∃ (V : set α), is_open V ∧ 1 ∈ V ∧ V * V ⊆ U

Given a open neighborhood U of 1 there is a open neighborhood V of 1 such that VV ⊆ U.

source

theorem zero_open_separated_add {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {U : set α} (h1U : is_open U) (h2U : 0 ∈ U) :

∃ (V : set α), is_open V ∧ 0 ∈ V ∧ V + V ⊆ U

Given a open neighborhood U of 0 there is a open neighborhood V of 0 such that V + V ⊆ U.

source

theorem compact_open_separated_add {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {K U : set α} (hK : is_compact K) (hU : is_open U) (hKU : K ⊆ U) :

∃ (V : set α), 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 {α : Type u} [topological_space α] [group α] [topological_group α] {K U : set α} (hK : is_compact K) (hU : is_open U) (hKU : K ⊆ U) :

∃ (V : set α), 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 {α : Type u} [topological_space α] [add_group α] [topological_add_group α] {K V : set α} (hK : is_compact K) (hV : (interior V).nonempty) :

∃ (t : finset α), K ⊆ ⋃ (g : α) (H : g ∈ t), (λ (h : α), 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 {α : Type u} [topological_space α] [group α] [topological_group α] {K V : set α} (hK : is_compact K) (hV : (interior V).nonempty) :

∃ (t : finset α), K ⊆ ⋃ (g : α) (H : g ∈ t), (λ (h : α), 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 {α : Type u} [topological_space α] [comm_group α] [topological_group α] (x y : α) :

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

source

theorem nhds_add {α : Type u} [topological_space α] [add_comm_group α] [topological_add_group α] (x y : α) :

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

source

theorem nhds_is_add_hom {α : Type u} [topological_space α] [add_comm_group α] [topological_add_group α] :

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

source

theorem nhds_is_mul_hom {α : Type u} [topological_space α] [comm_group α] [topological_group α] :

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