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 Gmeans thatGhas 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 (*).
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
- 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 := _}
@[simp]
theorem
homeomorph.coe_add_left
{G : Type w}
[topological_space G]
[add_group G]
[has_continuous_add G]
(a : G) :
⇑(homeomorph.add_left a) = has_add.add a
@[simp]
theorem
homeomorph.coe_mul_left
{G : Type w}
[topological_space G]
[group G]
[has_continuous_mul G]
(a : G) :
⇑(homeomorph.mul_left a) = has_mul.mul a
theorem
homeomorph.add_left_symm
{G : Type w}
[topological_space G]
[add_group G]
[has_continuous_add G]
(a : G) :
(homeomorph.add_left a).symm = homeomorph.add_left (-a)
theorem
homeomorph.mul_left_symm
{G : Type w}
[topological_space G]
[group G]
[has_continuous_mul G]
(a : G) :
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
- 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 := _}
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)
theorem
discrete_topology_of_open_singleton_zero
{G : Type w}
[topological_space G]
[add_group G]
[has_continuous_add G]
(h : is_open {0}) :
theorem
discrete_topology_of_open_singleton_one
{G : Type w}
[topological_space G]
[group G]
[has_continuous_mul G]
(h : is_open {1}) :
theorem
discrete_topology_iff_open_singleton_zero
{G : Type w}
[topological_space G]
[add_group G]
[has_continuous_add G] :
discrete_topology G ↔ is_open {0}
theorem
discrete_topology_iff_open_singleton_one
{G : Type w}
[topological_space G]
[group G]
[has_continuous_mul G] :
discrete_topology G ↔ is_open {1}
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]
- 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
- uniform_add_group.to_topological_add_group
- linear_ordered_add_comm_group.topological_add_group
- topological_ring.to_topological_add_group
- normed_top_group
- add_group_filter_basis.is_topological_add_group
- nonarchimedean_add_group.to_topological_add_group
- prod.topological_add_group
- pi.topological_add_group
- add_subgroup.topological_closure_topological_add_group
- topological_add_group_quotient
- additive.topological_add_group
- real.topological_add_group
- rat.topological_add_group
- tangent_space.topological_add_group
@[class]
- 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.
theorem
continuous_on_inv
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
{s : set G} :
theorem
continuous_on_neg
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
{s : set G} :
theorem
continuous_within_at_inv
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
{s : set G}
{x : G} :
theorem
continuous_within_at_neg
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
{s : set G}
{x : G} :
theorem
continuous_at_neg
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
{x : G} :
theorem
continuous_at_inv
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
{x : G} :
theorem
tendsto_inv
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
(a : G) :
filter.tendsto has_inv.inv (𝓝 a) (𝓝 a⁻¹)
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))
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
theorem
tendsto_inv_nhds_within_Ioi
{H : Type x}
[topological_space H]
[ordered_comm_group H]
[topological_group H]
{a : H} :
filter.tendsto has_inv.inv (𝓝[set.Ioi a] a) (𝓝[set.Iio a⁻¹] a⁻¹)
theorem
tendsto_neg_nhds_within_Ioi
{H : Type x}
[topological_space H]
[ordered_add_comm_group H]
[topological_add_group H]
{a : H} :
filter.tendsto has_neg.neg (𝓝[set.Ioi a] a) (𝓝[set.Iio (-a)] -a)
theorem
tendsto_inv_nhds_within_Iio
{H : Type x}
[topological_space H]
[ordered_comm_group H]
[topological_group H]
{a : H} :
filter.tendsto has_inv.inv (𝓝[set.Iio a] a) (𝓝[set.Ioi a⁻¹] a⁻¹)
theorem
tendsto_neg_nhds_within_Iio
{H : Type x}
[topological_space H]
[ordered_add_comm_group H]
[topological_add_group H]
{a : H} :
filter.tendsto has_neg.neg (𝓝[set.Iio a] a) (𝓝[set.Ioi (-a)] -a)
theorem
tendsto_inv_nhds_within_Ioi_inv
{H : Type x}
[topological_space H]
[ordered_comm_group H]
[topological_group H]
{a : H} :
filter.tendsto has_inv.inv (𝓝[set.Ioi a⁻¹] a⁻¹) (𝓝[set.Iio a] a)
theorem
tendsto_neg_nhds_within_Ioi_neg
{H : Type x}
[topological_space H]
[ordered_add_comm_group H]
[topological_add_group H]
{a : H} :
filter.tendsto has_neg.neg (𝓝[set.Ioi (-a)] -a) (𝓝[set.Iio a] a)
theorem
tendsto_inv_nhds_within_Iio_inv
{H : Type x}
[topological_space H]
[ordered_comm_group H]
[topological_group H]
{a : H} :
filter.tendsto has_inv.inv (𝓝[set.Iio a⁻¹] a⁻¹) (𝓝[set.Ioi a] a)
theorem
tendsto_neg_nhds_within_Iio_neg
{H : Type x}
[topological_space H]
[ordered_add_comm_group H]
[topological_add_group H]
{a : H} :
filter.tendsto has_neg.neg (𝓝[set.Iio (-a)] -a) (𝓝[set.Ioi a] a)
theorem
tendsto_inv_nhds_within_Ici
{H : Type x}
[topological_space H]
[ordered_comm_group H]
[topological_group H]
{a : H} :
filter.tendsto has_inv.inv (𝓝[set.Ici a] a) (𝓝[set.Iic a⁻¹] a⁻¹)
theorem
tendsto_neg_nhds_within_Ici
{H : Type x}
[topological_space H]
[ordered_add_comm_group H]
[topological_add_group H]
{a : H} :
filter.tendsto has_neg.neg (𝓝[set.Ici a] a) (𝓝[set.Iic (-a)] -a)
theorem
tendsto_inv_nhds_within_Iic
{H : Type x}
[topological_space H]
[ordered_comm_group H]
[topological_group H]
{a : H} :
filter.tendsto has_inv.inv (𝓝[set.Iic a] a) (𝓝[set.Ici a⁻¹] a⁻¹)
theorem
tendsto_neg_nhds_within_Iic
{H : Type x}
[topological_space H]
[ordered_add_comm_group H]
[topological_add_group H]
{a : H} :
filter.tendsto has_neg.neg (𝓝[set.Iic a] a) (𝓝[set.Ici (-a)] -a)
theorem
tendsto_neg_nhds_within_Ici_neg
{H : Type x}
[topological_space H]
[ordered_add_comm_group H]
[topological_add_group H]
{a : H} :
filter.tendsto has_neg.neg (𝓝[set.Ici (-a)] -a) (𝓝[set.Iic a] a)
theorem
tendsto_inv_nhds_within_Ici_inv
{H : Type x}
[topological_space H]
[ordered_comm_group H]
[topological_group H]
{a : H} :
filter.tendsto has_inv.inv (𝓝[set.Ici a⁻¹] a⁻¹) (𝓝[set.Iic a] a)
theorem
tendsto_neg_nhds_within_Iic_neg
{H : Type x}
[topological_space H]
[ordered_add_comm_group H]
[topological_add_group H]
{a : H} :
filter.tendsto has_neg.neg (𝓝[set.Iic (-a)] -a) (𝓝[set.Ici a] a)
theorem
tendsto_inv_nhds_within_Iic_inv
{H : Type x}
[topological_space H]
[ordered_comm_group H]
[topological_group H]
{a : H} :
filter.tendsto has_inv.inv (𝓝[set.Iic a⁻¹] a⁻¹) (𝓝[set.Ici a] a)
@[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)
@[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)
@[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)
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.
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 := _}
theorem
nhds_one_symm
(G : Type w)
[topological_space G]
[group G]
[topological_group G] :
filter.comap has_inv.inv (𝓝 1) = 𝓝 1
theorem
nhds_zero_symm
(G : Type w)
[topological_space G]
[add_group G]
[topological_add_group G] :
filter.comap has_neg.neg (𝓝 0) = 𝓝 0
The map (x, y) ↦ (x, xy) as a homeomorphism. This is a shear mapping.
Equations
- homeomorph.shear_mul_right G = {to_equiv := {to_fun := ((equiv.refl G).prod_shear equiv.mul_left).to_fun, inv_fun := ((equiv.refl G).prod_shear equiv.mul_left).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
def
homeomorph.shear_add_right
(G : Type w)
[topological_space G]
[add_group G]
[topological_add_group G] :
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] :
@[simp]
theorem
homeomorph.shear_add_right_coe
(G : Type w)
[topological_space G]
[add_group G]
[topological_add_group G] :
@[simp]
theorem
homeomorph.shear_add_right_symm_coe
(G : Type w)
[topological_space G]
[add_group G]
[topological_add_group G] :
@[simp]
theorem
homeomorph.shear_mul_right_symm_coe
(G : Type w)
[topological_space G]
[group G]
[topological_group G] :
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) :
def
subgroup.topological_closure
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
(s : subgroup G) :
subgroup G
The (topological-space) closure of a subgroup of a space M with has_continuous_mul is
itself a subgroup.
def
add_subgroup.topological_closure
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
(s : add_subgroup G) :
The (topological-space) closure of an additive subgroup of a space M with
has_continuous_add is itself an additive subgroup.
@[simp]
theorem
subgroup.topological_closure_coe
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
{s : subgroup G} :
↑(s.topological_closure) = closure ↑s
@[simp]
theorem
add_subgroup.topological_closure_coe
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
{s : add_subgroup G} :
↑(s.topological_closure) = closure ↑s
@[instance]
def
add_subgroup.topological_closure_topological_add_group
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
(s : add_subgroup G) :
@[instance]
def
subgroup.topological_closure_topological_group
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
(s : subgroup G) :
theorem
add_subgroup.add_subgroup_topological_closure
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
(s : add_subgroup G) :
s ≤ s.topological_closure
theorem
subgroup.subgroup_topological_closure
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
(s : subgroup G) :
s ≤ s.topological_closure
theorem
subgroup.is_closed_topological_closure
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
(s : subgroup G) :
theorem
add_subgroup.is_closed_topological_closure
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
(s : add_subgroup G) :
theorem
add_subgroup.topological_closure_minimal
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
(s : add_subgroup G)
{t : add_subgroup G}
(h : s ≤ t)
(ht : is_closed ↑t) :
s.topological_closure ≤ t
theorem
subgroup.topological_closure_minimal
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
(s : subgroup G)
{t : subgroup G}
(h : s ≤ t)
(ht : is_closed ↑t) :
s.topological_closure ≤ t
theorem
dense_range.topological_closure_map_add_subgroup
{G : Type w}
{H : Type x}
[topological_space G]
[add_group G]
[topological_add_group G]
[add_group H]
[topological_space H]
[topological_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}
[topological_space G]
[group G]
[topological_group G]
[group H]
[topological_space H]
[topological_group H]
{f : G →* H}
(hf : continuous ⇑f)
(hf' : dense_range ⇑f)
{s : subgroup G}
(hs : s.topological_closure = ⊤) :
(subgroup.map f s).topological_closure = ⊤
theorem
exists_nhds_half_neg
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
{s : set G}
(hs : s ∈ 𝓝 0) :
theorem
exists_nhds_split_inv
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
{s : set G}
(hs : s ∈ 𝓝 1) :
theorem
nhds_translation_add_neg
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
(x : G) :
theorem
nhds_translation_mul_inv
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
(x : G) :
@[simp]
theorem
map_add_left_nhds
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
(x y : G) :
filter.map (has_add.add x) (𝓝 y) = 𝓝 (x + y)
@[simp]
theorem
map_mul_left_nhds
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
(x y : G) :
filter.map (has_mul.mul x) (𝓝 y) = 𝓝 (x * y)
theorem
map_add_left_nhds_zero
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
(x : G) :
filter.map (has_add.add x) (𝓝 0) = 𝓝 x
theorem
map_mul_left_nhds_one
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
(x : G) :
filter.map (has_mul.mul x) (𝓝 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]
[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)) :
@[instance]
def
quotient_group.quotient.topological_space
{G : Type u_1}
[group G]
[topological_space G]
(N : subgroup G) :
@[instance]
def
quotient_add_group.quotient.topological_space
{G : Type u_1}
[add_group G]
[topological_space G]
(N : add_subgroup G) :
theorem
quotient_group.is_open_map_coe
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
(N : subgroup G) :
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) :
@[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] :
@[instance]
def
topological_group_quotient
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
(N : subgroup G)
[N.normal] :
@[class]
- 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.
@[instance]
def
topological_add_group.to_has_continuous_sub
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G] :
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]
- 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.
theorem
is_open.mul_left
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
{s t : set G} :
theorem
is_open.add_left
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
{s t : set G} :
theorem
is_open.mul_right
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
{s t : set G} :
theorem
is_open.add_right
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
{s t : set G} :
theorem
topological_add_group.t1_space
(G : Type w)
[topological_space G]
[add_group G]
[topological_add_group G]
(h : is_closed {0}) :
t1_space G
theorem
topological_group.t1_space
(G : Type w)
[topological_space G]
[group G]
[topological_group G]
(h : is_closed {1}) :
t1_space G
theorem
topological_add_group.regular_space
(G : Type w)
[topological_space G]
[add_group G]
[topological_add_group G]
[t1_space G] :
theorem
topological_group.regular_space
(G : Type w)
[topological_space G]
[group G]
[topological_group G]
[t1_space G] :
theorem
topological_add_group.t2_space
(G : Type w)
[topological_space G]
[add_group G]
[topological_add_group G]
[t1_space G] :
t2_space G
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.
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) :
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) :
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) :
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) :
A compact set is covered by finitely many left multiplicative translates of a set with non-empty interior.
@[instance]
def
separable_locally_compact_add_group.sigma_compact_space
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
[topological_space.separable_space G]
[locally_compact_space G] :
@[instance]
def
separable_locally_compact_group.sigma_compact_space
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
[topological_space.separable_space G]
[locally_compact_space G] :
Every locally compact separable topological group is σ-compact. Note: this is not true if we drop the topological group hypothesis.
theorem
topological_space.positive_compacts.locally_compact_space_of_add_group
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
[t2_space G]
(K : topological_space.positive_compacts G) :
theorem
topological_space.positive_compacts.locally_compact_space_of_group
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
[t2_space G]
(K : topological_space.positive_compacts G) :
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) :
theorem
nhds_add
{G : Type w}
[topological_space G]
[add_comm_group G]
[topological_add_group G]
(x y : G) :
@[simp]
theorem
nhds_mul_hom_apply
{G : Type w}
[topological_space G]
[comm_group G]
[topological_group G]
(a : G) :
⇑nhds_mul_hom a = 𝓝 a
On an additive topological group, 𝓝 : G → filter G can be promoted to an
add_hom.
@[simp]
theorem
nhds_add_hom_apply
{G : Type w}
[topological_space G]
[add_comm_group G]
[topological_add_group G]
(a : G) :
⇑nhds_add_hom a = 𝓝 a
On a topological group, 𝓝 : G → filter G can be promoted to a mul_hom.
@[instance]
def
additive.topological_add_group
{G : Type u_1}
[h : topological_space G]
[group G]
[topological_group G] :
@[instance]
def
multiplicative.topological_group
{G : Type u_1}
[h : topological_space G]
[add_group G]
[topological_add_group G] :
@[instance]