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 (*).
@[protected]
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.
Equations
- homeomorph.add_left a = {to_equiv := {to_fun := (equiv.add_left a).to_fun, inv_fun := (equiv.add_left a).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[protected]
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)
@[protected]
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.
Equations
- homeomorph.add_right a = {to_equiv := {to_fun := (equiv.add_right a).to_fun, inv_fun := (equiv.add_right a).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[protected]
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 := _}
@[simp]
theorem
homeomorph.coe_mul_right
{G : Type w}
[topological_space G]
[group G]
[has_continuous_mul G]
(a : G) :
⇑(homeomorph.mul_right a) = λ (g : G), g * a
@[simp]
theorem
homeomorph.coe_add_right
{G : Type w}
[topological_space G]
[add_group G]
[has_continuous_add G]
(a : G) :
⇑(homeomorph.add_right a) = λ (g : G), g + a
theorem
homeomorph.mul_right_symm
{G : Type w}
[topological_space G]
[group G]
[has_continuous_mul G]
(a : G) :
theorem
homeomorph.add_right_symm
{G : Type w}
[topological_space G]
[add_group G]
[has_continuous_add G]
(a : G) :
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 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}
[topological_space α]
[group α]
[has_continuous_mul α]
{s t : set α}
(ht : is_open t) :
theorem
is_open.add_left
{α : Type u}
[topological_space α]
[add_group α]
[has_continuous_add α]
{s t : set α}
(ht : is_open t) :
theorem
is_open.mul_right
{α : Type u}
[topological_space α]
[group α]
[has_continuous_mul α]
{s t : set α}
(hs : is_open s) :
theorem
is_open.add_right
{α : Type u}
[topological_space α]
[add_group α]
[has_continuous_add α]
{s t : set α}
(hs : is_open s) :
theorem
subset_interior_mul_left
{α : Type u}
[topological_space α]
[group α]
[has_continuous_mul α]
{s t : set α} :
theorem
subset_interior_add_left
{α : Type u}
[topological_space α]
[add_group α]
[has_continuous_add α]
{s t : set α} :
theorem
subset_interior_add_right
{α : Type u}
[topological_space α]
[add_group α]
[has_continuous_add α]
{s t : set α} :
theorem
subset_interior_mul_right
{α : Type u}
[topological_space α]
[group α]
[has_continuous_mul α]
{s t : set α} :
theorem
subset_interior_add
{α : Type u}
[topological_space α]
[add_group α]
[has_continuous_add α]
{s t : set α} :
theorem
subset_interior_mul
{α : Type u}
[topological_space α]
[group α]
[has_continuous_mul α]
{s t : set α} :
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_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
- submodule.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.
Instances
- group_filter_basis.is_topological_group
- nonarchimedean_group.to_topological_group
- prod.topological_group
- pi.topological_group
- subgroup.topological_group
- subgroup.topological_closure_topological_group
- topological_group_quotient
- multiplicative.topological_group
- units.topological_group
- circle.topological_group
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))
@[continuity]
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)⁻¹)
@[continuity]
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_at.neg
{α : Type u}
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
[topological_space α]
{f : α → G}
{x : α}
(hf : continuous_at f x) :
continuous_at (λ (x : α), -f x) x
theorem
continuous_at.inv
{α : Type u}
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
[topological_space α]
{f : α → G}
{x : α}
(hf : continuous_at f x) :
continuous_at (λ (x : α), (f x)⁻¹) 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)
@[protected, 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)
@[protected, 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)
@[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 (C 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)
[topological_space G]
[add_group G]
[topological_add_group G] :
G ≃ₜ G
Negation in a topological group as a homeomorphism.
Equations
- homeomorph.neg G = {to_equiv := {to_fun := (equiv.neg G).to_fun, inv_fun := (equiv.neg G).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[protected]
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
@[protected]
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 := _}
@[protected]
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.
Equations
- homeomorph.shear_add_right G = {to_equiv := {to_fun := ((equiv.refl G).prod_shear equiv.add_left).to_fun, inv_fun := ((equiv.refl G).prod_shear equiv.add_left).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[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
is_open.inv
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
{s : set G}
(hs : is_open s) :
theorem
is_open.neg
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
{s : set G}
(hs : is_open s) :
theorem
is_closed.neg
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
{s : set G}
(hs : is_closed s) :
theorem
is_closed.inv
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
{s : set G}
(hs : is_closed s) :
@[protected, instance]
def
add_subgroup.topological_add_group
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
(S : add_subgroup G) :
@[protected, instance]
def
subgroup.topological_group
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
(S : subgroup 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
@[protected, 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) :
@[protected, 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)) :
@[protected, instance]
def
quotient_group.quotient.topological_space
{G : Type u_1}
[group G]
[topological_space G]
(N : subgroup G) :
topological_space (G ⧸ N)
@[protected, instance]
def
quotient_add_group.quotient.topological_space
{G : Type u_1}
[add_group G]
[topological_space G]
(N : add_subgroup G) :
topological_space (G ⧸ N)
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) :
@[protected, 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 (G ⧸ N)
@[protected, instance]
def
topological_group_quotient
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
(N : subgroup G)
[N.normal] :
topological_group (G ⧸ N)
@[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.
@[class]
- continuous_div' : 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 groups. Lemmas using this class have primes.
The unprimed version is for group_with_zero.
Instances
@[protected, instance]
def
topological_add_group.to_has_continuous_sub
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G] :
@[protected, instance]
def
topological_group.to_has_continuous_div
{G : Type w}
[topological_space G]
[group G]
[topological_group G] :
theorem
filter.tendsto.div'
{α : Type u}
{G : Type w}
[topological_space G]
[has_div G]
[has_continuous_div 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
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
filter.tendsto.const_sub
{α : Type u}
{G : Type w}
[topological_space G]
[has_sub G]
[has_continuous_sub G]
(b : G)
{c : G}
{f : α → G}
{l : filter α}
(h : filter.tendsto f l (𝓝 c)) :
filter.tendsto (λ (k : α), b - f k) l (𝓝 (b - c))
theorem
filter.tendsto.const_div'
{α : Type u}
{G : Type w}
[topological_space G]
[has_div G]
[has_continuous_div G]
(b : G)
{c : G}
{f : α → G}
{l : filter α}
(h : filter.tendsto f l (𝓝 c)) :
filter.tendsto (λ (k : α), b / f k) l (𝓝 (b / c))
theorem
filter.tendsto.div_const'
{α : Type u}
{G : Type w}
[topological_space G]
[has_div G]
[has_continuous_div G]
(b : G)
{c : G}
{f : α → G}
{l : filter α}
(h : filter.tendsto f l (𝓝 c)) :
filter.tendsto (λ (k : α), f k / b) l (𝓝 (c / b))
theorem
filter.tendsto.sub_const
{α : Type u}
{G : Type w}
[topological_space G]
[has_sub G]
[has_continuous_sub G]
(b : G)
{c : G}
{f : α → G}
{l : filter α}
(h : filter.tendsto f l (𝓝 c)) :
filter.tendsto (λ (k : α), f k - b) l (𝓝 (c - b))
@[continuity]
theorem
continuous.div'
{α : Type u}
{G : Type w}
[topological_space G]
[has_div G]
[has_continuous_div G]
[topological_space α]
{f g : α → G}
(hf : continuous f)
(hg : continuous g) :
continuous (λ (x : α), f x / g x)
@[continuity]
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_sub_left
{G : Type w}
[topological_space G]
[has_sub G]
[has_continuous_sub G]
(a : G) :
continuous (λ (b : G), a - b)
theorem
continuous_div_left'
{G : Type w}
[topological_space G]
[has_div G]
[has_continuous_div G]
(a : G) :
continuous (λ (b : G), a / b)
theorem
continuous_sub_right
{G : Type w}
[topological_space G]
[has_sub G]
[has_continuous_sub G]
(a : G) :
continuous (λ (b : G), b - a)
theorem
continuous_div_right'
{G : Type w}
[topological_space G]
[has_div G]
[has_continuous_div G]
(a : G) :
continuous (λ (b : G), b / a)
theorem
continuous_at.div'
{α : Type u}
{G : Type w}
[topological_space G]
[has_div G]
[has_continuous_div G]
[topological_space α]
{f g : α → G}
{x : α}
(hf : continuous_at f x)
(hg : continuous_at g x) :
continuous_at (λ (x : α), f x / g x) x
theorem
continuous_at.sub
{α : Type u}
{G : Type w}
[topological_space G]
[has_sub G]
[has_continuous_sub G]
[topological_space α]
{f g : α → G}
{x : α}
(hf : continuous_at f x)
(hg : continuous_at g x) :
continuous_at (λ (x : α), f x - g x) 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_within_at.div'
{α : Type u}
{G : Type w}
[topological_space G]
[has_div G]
[has_continuous_div 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
continuous_on.div'
{α : Type u}
{G : Type w}
[topological_space G]
[has_div G]
[has_continuous_div 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_div
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
(x : G) :
filter.comap (λ (y : G), y / x) (𝓝 1) = 𝓝 x
theorem
nhds_translation_sub
{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
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.
@[protected, 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] :
@[protected, 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.
@[protected, instance]
def
additive.topological_add_group
{G : Type u_1}
[h : topological_space G]
[group G]
[topological_group G] :
@[protected, instance]
def
multiplicative.topological_group
{G : Type u_1}
[h : topological_space G]
[add_group G]
[topological_add_group G] :
@[protected, instance]
def
units.homeomorph.prod_units
{α : Type u}
{β : Type v}
[monoid α]
[topological_space α]
[has_continuous_mul α]
[monoid β]
[topological_space β]
[has_continuous_mul β] :
The topological group isomorphism between the units of a product of two monoids, and the product of the units of each monoid.
Equations
- units.homeomorph.prod_units = {to_equiv := {to_fun := mul_equiv.prod_units.to_fun, inv_fun := mul_equiv.prod_units.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
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.
- to_topological_space : topological_space α
- to_topological_group : topological_group α
A group topology on a group α is a topology for which multiplication and inversion
are continuous.
- to_topological_space : topological_space α
- to_topological_add_group : topological_add_group α
An additive group topology on an additive group α is a topology for which addition and
negation are continuous.
theorem
add_group_topology.continuous_add'
{α : Type u}
[add_group α]
(g : add_group_topology α) :
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.
A version of the global continuous_inv suitable for dot notation.
@[ext]
theorem
group_topology.ext'
{α : Type u}
[group α]
{f g : group_topology α}
(h : f.to_topological_space.is_open = g.to_topological_space.is_open) :
f = g
theorem
add_group_topology.ext'
{α : Type u}
[add_group α]
{f g : add_group_topology α}
(h : f.to_topological_space.is_open = g.to_topological_space.is_open) :
f = g
@[protected, instance]
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).
@[protected, instance]
@[simp]
theorem
group_topology.to_topological_space_le
{α : Type u}
[group α]
{x y : group_topology α} :
x.to_topological_space ≤ y.to_topological_space ↔ x ≤ y
@[simp]
theorem
add_group_topology.to_topological_space_le
{α : Type u}
[add_group α]
{x y : add_group_topology α} :
x.to_topological_space ≤ y.to_topological_space ↔ x ≤ y
@[protected, instance]
Equations
- group_topology.has_top = {top := {to_topological_space := ⊤, to_topological_group := _}}
@[protected, instance]
Equations
@[simp]
@[simp]
@[protected, instance]
Equations
- group_topology.has_bot = {bot := {to_topological_space := ⊥, to_topological_group := _}}
@[protected, instance]
Equations
@[simp]
@[simp]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
- group_topology.has_inf = {inf := λ (x y : group_topology α), {to_topological_space := x.to_topological_space ⊓ y.to_topological_space, to_topological_group := _}}
@[protected, instance]
Equations
- add_group_topology.has_inf = {inf := λ (x y : add_group_topology α), {to_topological_space := x.to_topological_space ⊓ y.to_topological_space, to_topological_add_group := _}}
@[simp]
theorem
add_group_topology.to_topological_space_inf
{α : Type u}
[add_group α]
(x y : add_group_topology α) :
@[simp]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
- group_topology.has_Inf = {Inf := λ (S : set (group_topology α)), {to_topological_space := Inf (group_topology.to_topological_space '' S), to_topological_group := _}}
@[protected, instance]
Infimum of a collection of additive group topologies
Equations
- add_group_topology.has_Inf = {Inf := λ (S : set (add_group_topology α)), {to_topological_space := Inf (add_group_topology.to_topological_space '' S), to_topological_add_group := _}}
@[simp]
theorem
group_topology.to_topological_space_Inf
{α : Type u}
[group α]
(s : set (group_topology α)) :
@[simp]
theorem
add_group_topology.to_topological_space_Inf
{α : Type u}
[add_group α]
(s : set (add_group_topology α)) :
@[simp]
theorem
group_topology.to_topological_space_infi
{α : Type u}
[group α]
{ι : Sort u_1}
(s : ι → group_topology α) :
(⨅ (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 : ι → add_group_topology α) :
(⨅ (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
- group_topology.complete_semilattice_Inf = {le := partial_order.le group_topology.partial_order, lt := partial_order.lt group_topology.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, Inf := Inf group_topology.has_Inf, Inf_le := _, le_Inf := _}
@[protected, instance]
Equations
- add_group_topology.complete_semilattice_Inf = {le := partial_order.le add_group_topology.partial_order, lt := partial_order.lt add_group_topology.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, Inf := Inf add_group_topology.has_Inf, Inf_le := _, le_Inf := _}
@[protected, instance]
Equations
- add_group_topology.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_complete_semilattice_Inf (add_group_topology α)), le := semilattice_inf.le add_group_topology.semilattice_inf, lt := semilattice_inf.lt add_group_topology.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf add_group_topology.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_complete_semilattice_Inf (add_group_topology α)), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_complete_semilattice_Inf (add_group_topology α)), Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}
@[protected, instance]
Equations
- group_topology.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_complete_semilattice_Inf (group_topology α)), le := semilattice_inf.le group_topology.semilattice_inf, lt := semilattice_inf.lt group_topology.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf group_topology.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_complete_semilattice_Inf (group_topology α)), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_complete_semilattice_Inf (group_topology α)), Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}
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
- group_topology.coinduced f = Inf {b : group_topology β | topological_space.coinduced f t ≤ b.to_topological_space}
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 : α → β) :