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_open.left_add_coset
{G : Type w}
[topological_space G]
[add_group G]
[has_continuous_add G]
{U : set G}
(h : is_open U)
(x : G) :
is_open (left_add_coset x U)
theorem
is_open.left_coset
{G : Type w}
[topological_space G]
[group G]
[has_continuous_mul G]
{U : set G}
(h : is_open U)
(x : G) :
is_open (left_coset x U)
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)
theorem
is_closed.left_add_coset
{G : Type w}
[topological_space G]
[add_group G]
[has_continuous_add G]
{U : set G}
(h : is_closed U)
(x : G) :
is_closed (left_add_coset x U)
theorem
is_closed.left_coset
{G : Type w}
[topological_space G]
[group G]
[has_continuous_mul G]
{U : set G}
(h : is_closed U)
(x : G) :
is_closed (left_coset x U)
@[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_open.right_coset
{G : Type w}
[topological_space G]
[group G]
[has_continuous_mul G]
{U : set G}
(h : is_open U)
(x : G) :
is_open (right_coset U x)
theorem
is_open.right_add_coset
{G : Type w}
[topological_space G]
[add_group G]
[has_continuous_add G]
{U : set G}
(h : is_open U)
(x : G) :
is_open (right_add_coset U x)
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_closed.right_coset
{G : Type w}
[topological_space G]
[group G]
[has_continuous_mul G]
{U : set G}
(h : is_closed U)
(x : G) :
is_closed (right_coset U x)
theorem
is_closed.right_add_coset
{G : Type w}
[topological_space G]
[add_group G]
[has_continuous_add G]
{U : set G}
(h : is_closed U)
(x : G) :
is_closed (right_add_coset U x)
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}
@[class]
- continuous_neg : continuous (λ (a : G), -a)
Basic hypothesis to talk about a topological additive group. A topological additive group
over M, for example, is obtained by requiring the instances add_group M and
has_continuous_add M and has_continuous_neg M.
Instances of this typeclass
- has_continuous_neg_of_discrete_topology
- topological_add_group.to_has_continuous_neg
- topological_ring.to_has_continuous_neg
- prod.has_continuous_neg
- pi.has_continuous_neg
- pi.has_continuous_neg'
- additive.has_continuous_neg
- add_opposite.has_continuous_neg
- mul_opposite.has_continuous_neg
- matrix.has_continuous_neg
- metric.sphere.has_continuous_neg
- metric.ball.has_continuous_neg
- metric.closed_ball.has_continuous_neg
@[class]
- continuous_inv : continuous (λ (a : G), a⁻¹)
Basic hypothesis to talk about a topological group. A topological group over M, for example,
is obtained by requiring the instances group M and has_continuous_mul M and
has_continuous_inv M.
theorem
continuous_on_inv
{G : Type w}
[topological_space G]
[has_inv G]
[has_continuous_inv G]
{s : set G} :
theorem
continuous_on_neg
{G : Type w}
[topological_space G]
[has_neg G]
[has_continuous_neg G]
{s : set G} :
theorem
continuous_within_at_inv
{G : Type w}
[topological_space G]
[has_inv G]
[has_continuous_inv G]
{s : set G}
{x : G} :
theorem
continuous_within_at_neg
{G : Type w}
[topological_space G]
[has_neg G]
[has_continuous_neg G]
{s : set G}
{x : G} :
theorem
continuous_at_neg
{G : Type w}
[topological_space G]
[has_neg G]
[has_continuous_neg G]
{x : G} :
theorem
continuous_at_inv
{G : Type w}
[topological_space G]
[has_inv G]
[has_continuous_inv G]
{x : G} :
theorem
tendsto_inv
{G : Type w}
[topological_space G]
[has_inv G]
[has_continuous_inv G]
(a : G) :
filter.tendsto has_inv.inv (nhds a) (nhds a⁻¹)
theorem
tendsto_neg
{G : Type w}
[topological_space G]
[has_neg G]
[has_continuous_neg G]
(a : G) :
filter.tendsto has_neg.neg (nhds a) (nhds (-a))
theorem
filter.tendsto.inv
{α : Type u}
{G : Type w}
[topological_space G]
[has_inv G]
[has_continuous_inv G]
{f : α → G}
{l : filter α}
{y : G}
(h : filter.tendsto f l (nhds y)) :
filter.tendsto (λ (x : α), (f x)⁻¹) l (nhds 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]
[has_neg G]
[has_continuous_neg G]
{f : α → G}
{l : filter α}
{y : G}
(h : filter.tendsto f l (nhds y)) :
filter.tendsto (λ (x : α), -f x) l (nhds (-y))
@[continuity]
theorem
continuous.inv
{α : Type u}
{G : Type w}
[topological_space G]
[has_inv G]
[has_continuous_inv G]
[topological_space α]
{f : α → G}
(hf : continuous f) :
continuous (λ (x : α), (f x)⁻¹)
@[continuity]
theorem
continuous.neg
{α : Type u}
{G : Type w}
[topological_space G]
[has_neg G]
[has_continuous_neg G]
[topological_space α]
{f : α → G}
(hf : continuous f) :
continuous (λ (x : α), -f x)
theorem
continuous_at.neg
{α : Type u}
{G : Type w}
[topological_space G]
[has_neg G]
[has_continuous_neg 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]
[has_inv G]
[has_continuous_inv 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]
[has_inv G]
[has_continuous_inv 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]
[has_neg G]
[has_continuous_neg 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]
[has_inv G]
[has_continuous_inv 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]
[has_neg G]
[has_continuous_neg G]
[topological_space α]
{f : α → G}
{s : set α}
{x : α}
(hf : continuous_within_at f s x) :
continuous_within_at (λ (x : α), -f x) s x
@[protected, instance]
def
prod.has_continuous_neg
{G : Type w}
{H : Type x}
[topological_space G]
[has_neg G]
[has_continuous_neg G]
[topological_space H]
[has_neg H]
[has_continuous_neg H] :
has_continuous_neg (G × H)
@[protected, instance]
def
prod.has_continuous_inv
{G : Type w}
{H : Type x}
[topological_space G]
[has_inv G]
[has_continuous_inv G]
[topological_space H]
[has_inv H]
[has_continuous_inv H] :
has_continuous_inv (G × H)
@[protected, instance]
def
pi.has_continuous_inv
{ι : Type u_1}
{C : ι → Type u_2}
[Π (i : ι), topological_space (C i)]
[Π (i : ι), has_inv (C i)]
[∀ (i : ι), has_continuous_inv (C i)] :
has_continuous_inv (Π (i : ι), C i)
@[protected, instance]
def
pi.has_continuous_neg
{ι : Type u_1}
{C : ι → Type u_2}
[Π (i : ι), topological_space (C i)]
[Π (i : ι), has_neg (C i)]
[∀ (i : ι), has_continuous_neg (C i)] :
has_continuous_neg (Π (i : ι), C i)
@[protected, instance]
def
pi.has_continuous_neg'
{G : Type w}
[topological_space G]
[has_neg G]
[has_continuous_neg G]
{ι : Type u_1} :
has_continuous_neg (ι → G)
A version of pi.has_continuous_neg for non-dependent functions. It is needed
because sometimes Lean fails to use pi.has_continuous_neg for non-dependent functions.
@[protected, instance]
def
pi.has_continuous_inv'
{G : Type w}
[topological_space G]
[has_inv G]
[has_continuous_inv G]
{ι : Type u_1} :
has_continuous_inv (ι → G)
A version of pi.has_continuous_inv for non-dependent functions. It is needed because sometimes
Lean fails to use pi.has_continuous_inv for non-dependent functions.
@[protected, instance]
def
has_continuous_neg_of_discrete_topology
{H : Type x}
[topological_space H]
[has_neg H]
[discrete_topology H] :
@[protected, instance]
def
has_continuous_inv_of_discrete_topology
{H : Type x}
[topological_space H]
[has_inv H]
[discrete_topology H] :
theorem
is_closed_set_of_map_neg
(G₁ : Type u_2)
(G₂ : Type u_3)
[topological_space G₂]
[t2_space G₂]
[has_neg G₁]
[has_neg G₂]
[has_continuous_neg G₂] :
theorem
is_closed_set_of_map_inv
(G₁ : Type u_2)
(G₂ : Type u_3)
[topological_space G₂]
[t2_space G₂]
[has_inv G₁]
[has_inv G₂]
[has_continuous_inv G₂] :
@[protected, instance]
def
additive.has_continuous_neg
{H : Type x}
[h : topological_space H]
[has_inv H]
[has_continuous_inv H] :
@[protected, instance]
def
multiplicative.has_continuous_inv
{H : Type x}
[h : topological_space H]
[has_neg H]
[has_continuous_neg H] :
theorem
is_compact.neg
{G : Type w}
[topological_space G]
[has_involutive_neg G]
[has_continuous_neg G]
{s : set G}
(hs : is_compact s) :
is_compact (-s)
theorem
is_compact.inv
{G : Type w}
[topological_space G]
[has_involutive_inv G]
[has_continuous_inv G]
{s : set G}
(hs : is_compact s) :
@[protected]
def
homeomorph.neg
(G : Type u_1)
[topological_space G]
[has_involutive_neg G]
[has_continuous_neg 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]
def
homeomorph.inv
(G : Type u_1)
[topological_space G]
[has_involutive_inv G]
[has_continuous_inv G] :
G ≃ₜ G
Inversion in a topological group as a homeomorphism.
Equations
- homeomorph.inv G = {to_equiv := {to_fun := (equiv.inv G).to_fun, inv_fun := (equiv.inv G).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
theorem
is_open_map_neg
(G : Type w)
[topological_space G]
[has_involutive_neg G]
[has_continuous_neg G] :
theorem
is_open_map_inv
(G : Type w)
[topological_space G]
[has_involutive_inv G]
[has_continuous_inv G] :
theorem
is_closed_map_inv
(G : Type w)
[topological_space G]
[has_involutive_inv G]
[has_continuous_inv G] :
theorem
is_closed_map_neg
(G : Type w)
[topological_space G]
[has_involutive_neg G]
[has_continuous_neg G] :
theorem
is_open.inv
{G : Type w}
[topological_space G]
[has_involutive_inv G]
[has_continuous_inv G]
{s : set G}
(hs : is_open s) :
theorem
is_open.neg
{G : Type w}
[topological_space G]
[has_involutive_neg G]
[has_continuous_neg G]
{s : set G}
(hs : is_open s) :
theorem
is_closed.neg
{G : Type w}
[topological_space G]
[has_involutive_neg G]
[has_continuous_neg G]
{s : set G}
(hs : is_closed s) :
theorem
is_closed.inv
{G : Type w}
[topological_space G]
[has_involutive_inv G]
[has_continuous_inv G]
{s : set G}
(hs : is_closed s) :
theorem
neg_closure
{G : Type w}
[topological_space G]
[has_involutive_neg G]
[has_continuous_neg G]
(s : set G) :
theorem
inv_closure
{G : Type w}
[topological_space G]
[has_involutive_inv G]
[has_continuous_inv G]
(s : set G) :
theorem
has_continuous_neg_Inf
{G : Type w}
[has_neg G]
{ts : set (topological_space G)}
(h : ∀ (t : topological_space G), t ∈ ts → has_continuous_neg G) :
theorem
has_continuous_inv_Inf
{G : Type w}
[has_inv G]
{ts : set (topological_space G)}
(h : ∀ (t : topological_space G), t ∈ ts → has_continuous_inv G) :
theorem
has_continuous_inv_infi
{G : Type w}
{ι' : Sort u_1}
[has_inv G]
{ts' : ι' → topological_space G}
(h' : ∀ (i : ι'), has_continuous_inv G) :
theorem
has_continuous_neg_infi
{G : Type w}
{ι' : Sort u_1}
[has_neg G]
{ts' : ι' → topological_space G}
(h' : ∀ (i : ι'), has_continuous_neg G) :
theorem
has_continuous_inv_inf
{G : Type w}
[has_inv G]
{t₁ t₂ : topological_space G}
(h₁ : has_continuous_inv G)
(h₂ : has_continuous_inv G) :
theorem
has_continuous_neg_inf
{G : Type w}
[has_neg G]
{t₁ t₂ : topological_space G}
(h₁ : has_continuous_neg G)
(h₂ : has_continuous_neg G) :
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
- to_has_continuous_neg : has_continuous_neg G
A topological (additive) group is a group in which the addition and negation operations are continuous.
Instances of this typeclass
- 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_opposite.topological_add_group
- add_subgroup.topological_add_group
- add_subgroup.topological_closure_topological_add_group
- topological_add_group_quotient
- additive.topological_add_group
- add_units.topological_add_group
- real.topological_add_group
- submodule.topological_add_group
- submodule.topological_add_group_quotient
- rat.topological_add_group
- matrix.topological_add_group
- real.angle.topological_add_group
- continuous_map.topological_add_group
- weak_bilin.topological_add_group
- tangent_space.topological_add_group
@[class]
- to_has_continuous_mul : has_continuous_mul G
- to_has_continuous_inv : has_continuous_inv G
A topological group is a group in which the multiplication and inversion operations are continuous.
When you declare an instance that does not already have a uniform_space instance,
you should also provide an instance of uniform_space and uniform_group using
topological_group.to_uniform_space and topological_group_is_uniform.
Instances of this typeclass
- uniform_group.to_topological_group
- group_filter_basis.is_topological_group
- nonarchimedean_group.to_topological_group
- prod.topological_group
- pi.topological_group
- mul_opposite.topological_group
- subgroup.topological_group
- subgroup.topological_closure_topological_group
- topological_group_quotient
- multiplicative.topological_group
- units.topological_group
- continuous_map.topological_group
- metric.sphere.topological_group
- circle.topological_group
- alg_equiv.topological_group
- continuous_monoid_hom.topological_group
- pontryagin_dual.topological_group
@[protected, instance]
def
conj_act.units_has_continuous_const_smul
{M : Type u_1}
[monoid M]
[topological_space M]
[has_continuous_mul M] :
theorem
topological_group.continuous_conj_prod
{G : Type w}
[topological_space G]
[has_inv G]
[has_mul G]
[has_continuous_mul G]
[has_continuous_inv G] :
Conjugation is jointly continuous on G × G when both mul and inv are continuous.
theorem
topological_add_group.continuous_conj_sum
{G : Type w}
[topological_space G]
[has_neg G]
[has_add G]
[has_continuous_add G]
[has_continuous_neg G] :
Conjugation is jointly continuous on G × G when both mul and inv are
continuous.
theorem
topological_add_group.continuous_conj
{G : Type w}
[topological_space G]
[has_neg G]
[has_add G]
[has_continuous_add G]
(g : G) :
continuous (λ (h : G), g + h + -g)
Conjugation by a fixed element is continuous when add is continuous.
theorem
topological_group.continuous_conj
{G : Type w}
[topological_space G]
[has_inv G]
[has_mul G]
[has_continuous_mul G]
(g : G) :
continuous (λ (h : G), g * h * g⁻¹)
Conjugation by a fixed element is continuous when mul is continuous.
theorem
topological_add_group.continuous_conj'
{G : Type w}
[topological_space G]
[has_neg G]
[has_add G]
[has_continuous_add G]
[has_continuous_neg G]
(h : G) :
continuous (λ (g : G), g + h + -g)
Conjugation acting on fixed element of the additive group is continuous when both
add and neg are continuous.
theorem
topological_group.continuous_conj'
{G : Type w}
[topological_space G]
[has_inv G]
[has_mul G]
[has_continuous_mul G]
[has_continuous_inv G]
(h : G) :
continuous (λ (g : G), g * h * g⁻¹)
Conjugation acting on fixed element of the group is continuous when both mul and
inv are continuous.
@[continuity]
theorem
continuous_zpow
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
(z : ℤ) :
continuous (λ (a : G), a ^ z)
@[continuity]
theorem
continuous_zsmul
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
(z : ℤ) :
continuous (λ (a : G), z • a)
@[protected, instance]
def
add_group.has_continuous_const_smul_int
{A : Type u_1}
[add_group A]
[topological_space A]
[topological_add_group A] :
@[protected, instance]
def
add_group.has_continuous_smul_int
{A : Type u_1}
[add_group A]
[topological_space A]
[topological_add_group A] :
@[continuity]
theorem
continuous.zsmul
{α : Type u}
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
[topological_space α]
{f : α → G}
(h : continuous f)
(z : ℤ) :
continuous (λ (b : α), z • f b)
@[continuity]
theorem
continuous.zpow
{α : Type u}
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
[topological_space α]
{f : α → G}
(h : continuous f)
(z : ℤ) :
continuous (λ (b : α), f b ^ z)
theorem
continuous_on_zpow
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
{s : set G}
(z : ℤ) :
continuous_on (λ (x : G), x ^ z) s
theorem
continuous_on_zsmul
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
{s : set G}
(z : ℤ) :
continuous_on (λ (x : G), z • x) s
theorem
continuous_at_zsmul
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
(x : G)
(z : ℤ) :
continuous_at (λ (x : G), z • x) x
theorem
continuous_at_zpow
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
(x : G)
(z : ℤ) :
continuous_at (λ (x : G), x ^ z) x
theorem
filter.tendsto.zpow
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
{α : Type u_1}
{l : filter α}
{f : α → G}
{x : G}
(hf : filter.tendsto f l (nhds x))
(z : ℤ) :
filter.tendsto (λ (x : α), f x ^ z) l (nhds (x ^ z))
theorem
filter.tendsto.zsmul
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
{α : Type u_1}
{l : filter α}
{f : α → G}
{x : G}
(hf : filter.tendsto f l (nhds x))
(z : ℤ) :
filter.tendsto (λ (x : α), z • f x) l (nhds (z • x))
theorem
continuous_within_at.zpow
{α : Type u}
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
[topological_space α]
{f : α → G}
{x : α}
{s : set α}
(hf : continuous_within_at f s x)
(z : ℤ) :
continuous_within_at (λ (x : α), f x ^ z) s x
theorem
continuous_within_at.zsmul
{α : Type u}
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
[topological_space α]
{f : α → G}
{x : α}
{s : set α}
(hf : continuous_within_at f s x)
(z : ℤ) :
continuous_within_at (λ (x : α), z • f x) s x
theorem
continuous_at.zsmul
{α : 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)
(z : ℤ) :
continuous_at (λ (x : α), z • f x) x
theorem
continuous_at.zpow
{α : Type u}
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
[topological_space α]
{f : α → G}
{x : α}
(hf : continuous_at f x)
(z : ℤ) :
continuous_at (λ (x : α), f x ^ z) x
theorem
continuous_on.zsmul
{α : 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)
(z : ℤ) :
continuous_on (λ (x : α), z • f x) s
theorem
continuous_on.zpow
{α : Type u}
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
[topological_space α]
{f : α → G}
{s : set α}
(hf : continuous_on f s)
(z : ℤ) :
continuous_on (λ (x : α), f x ^ z) s
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 (nhds_within a (set.Ioi a)) (nhds_within a⁻¹ (set.Iio 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 (nhds_within a (set.Ioi a)) (nhds_within (-a) (set.Iio (-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 (nhds_within a (set.Iio a)) (nhds_within a⁻¹ (set.Ioi 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 (nhds_within a (set.Iio a)) (nhds_within (-a) (set.Ioi (-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 (nhds_within a⁻¹ (set.Ioi a⁻¹)) (nhds_within a (set.Iio 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 (nhds_within (-a) (set.Ioi (-a))) (nhds_within a (set.Iio 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 (nhds_within a⁻¹ (set.Iio a⁻¹)) (nhds_within a (set.Ioi 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 (nhds_within (-a) (set.Iio (-a))) (nhds_within a (set.Ioi 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 (nhds_within a (set.Ici a)) (nhds_within a⁻¹ (set.Iic 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 (nhds_within a (set.Ici a)) (nhds_within (-a) (set.Iic (-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 (nhds_within a (set.Iic a)) (nhds_within a⁻¹ (set.Ici 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 (nhds_within a (set.Iic a)) (nhds_within (-a) (set.Ici (-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 (nhds_within (-a) (set.Ici (-a))) (nhds_within a (set.Iic 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 (nhds_within a⁻¹ (set.Ici a⁻¹)) (nhds_within a (set.Iic 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 (nhds_within (-a) (set.Iic (-a))) (nhds_within a (set.Ici 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 (nhds_within a⁻¹ (set.Iic a⁻¹)) (nhds_within a (set.Ici 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, instance]
def
add_opposite.has_continuous_neg
{α : Type u}
[topological_space α]
[add_group α]
[has_continuous_neg α] :
@[protected, instance]
def
mul_opposite.has_continuous_inv
{α : Type u}
[topological_space α]
[group α]
[has_continuous_inv α] :
@[protected, instance]
def
add_opposite.topological_add_group
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α] :
If addition is continuous in α, then it also is in αᵃᵒᵖ.
@[protected, instance]
def
mul_opposite.topological_group
{α : Type u}
[topological_space α]
[group α]
[topological_group α] :
If multiplication is continuous in α, then it also is in αᵐᵒᵖ.
theorem
nhds_one_symm
(G : Type w)
[topological_space G]
[group G]
[topological_group G] :
filter.comap has_inv.inv (nhds 1) = nhds 1
theorem
nhds_zero_symm
(G : Type w)
[topological_space G]
[add_group G]
[topological_add_group G] :
filter.comap has_neg.neg (nhds 0) = nhds 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] :
@[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) :
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.
Equations
Instances for ↥subgroup.topological_closure
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.
Equations
Instances for ↥add_subgroup.topological_closure
@[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
add_subgroup.is_normal_topological_closure
{G : Type u_1}
[topological_space G]
[add_group G]
[topological_add_group G]
(N : add_subgroup G)
[N.normal] :
The topological closure of a normal additive subgroup is normal.
theorem
subgroup.is_normal_topological_closure
{G : Type u_1}
[topological_space G]
[group G]
[topological_group G]
(N : subgroup G)
[N.normal] :
The topological closure of a normal subgroup is normal.
theorem
mul_mem_connected_component_one
{G : Type u_1}
[topological_space G]
[mul_one_class G]
[has_continuous_mul G]
{g h : G}
(hg : g ∈ connected_component 1)
(hh : h ∈ connected_component 1) :
g * h ∈ connected_component 1
theorem
add_mem_connected_component_zero
{G : Type u_1}
[topological_space G]
[add_zero_class G]
[has_continuous_add G]
{g h : G}
(hg : g ∈ connected_component 0)
(hh : h ∈ connected_component 0) :
g + h ∈ connected_component 0
theorem
inv_mem_connected_component_one
{G : Type u_1}
[topological_space G]
[group G]
[topological_group G]
{g : G}
(hg : g ∈ connected_component 1) :
theorem
neg_mem_connected_component_zero
{G : Type u_1}
[topological_space G]
[add_group G]
[topological_add_group G]
{g : G}
(hg : g ∈ connected_component 0) :
def
subgroup.connected_component_of_one
(G : Type u_1)
[topological_space G]
[group G]
[topological_group G] :
subgroup G
The connected component of 1 is a subgroup of G.
Equations
- subgroup.connected_component_of_one G = {carrier := connected_component 1, mul_mem' := _, one_mem' := _, inv_mem' := _}
def
add_subgroup.connected_component_of_zero
(G : Type u_1)
[topological_space G]
[add_group G]
[topological_add_group G] :
The connected component of 0 is a subgroup of G.
Equations
- add_subgroup.connected_component_of_zero G = {carrier := connected_component 0, add_mem' := _, zero_mem' := _, neg_mem' := _}
def
subgroup.comm_group_topological_closure
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
[t2_space G]
(s : subgroup G)
(hs : ∀ (x y : ↥s), x * y = y * x) :
If a subgroup of a topological group is commutative, then so is its topological closure.
Equations
- s.comm_group_topological_closure hs = {mul := group.mul s.topological_closure.to_group, mul_assoc := _, one := group.one s.topological_closure.to_group, one_mul := _, mul_one := _, npow := group.npow s.topological_closure.to_group, npow_zero' := _, npow_succ' := _, inv := group.inv s.topological_closure.to_group, div := group.div s.topological_closure.to_group, div_eq_mul_inv := _, zpow := group.zpow s.topological_closure.to_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
def
add_subgroup.add_comm_group_topological_closure
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
[t2_space G]
(s : add_subgroup G)
(hs : ∀ (x y : ↥s), x + y = y + x) :
If a subgroup of an additive topological group is commutative, then so is its topological closure.
Equations
- s.add_comm_group_topological_closure hs = {add := add_group.add s.topological_closure.to_add_group, add_assoc := _, zero := add_group.zero s.topological_closure.to_add_group, zero_add := _, add_zero := _, nsmul := add_group.nsmul s.topological_closure.to_add_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg s.topological_closure.to_add_group, sub := add_group.sub s.topological_closure.to_add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul s.topological_closure.to_add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
theorem
exists_nhds_half_neg
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
{s : set G}
(hs : s ∈ nhds 0) :
theorem
exists_nhds_split_inv
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
{s : set G}
(hs : s ∈ nhds 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) (nhds y) = nhds (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) (nhds y) = nhds (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) (nhds 0) = nhds 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) (nhds 1) = nhds x
theorem
continuous_of_continuous_at_one
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
{M : Type u_1}
{hom : Type u_2}
[mul_one_class M]
[topological_space M]
[has_continuous_mul M]
[monoid_hom_class hom G M]
(f : hom)
(hf : continuous_at ⇑f 1) :
A monoid homomorphism (a bundled morphism of a type that implements monoid_hom_class) from a
topological group to a topological monoid is continuous provided that it is continuous at one. See
also uniform_continuous_of_continuous_at_one.
theorem
continuous_of_continuous_at_zero
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
{M : Type u_1}
{hom : Type u_2}
[add_zero_class M]
[topological_space M]
[has_continuous_add M]
[add_monoid_hom_class hom G M]
(f : hom)
(hf : continuous_at ⇑f 0) :
An additive monoid homomorphism (a bundled morphism of a type that implements
add_monoid_hom_class) from an additive topological group to an additive topological monoid is
continuous provided that it is continuous at zero. See also
uniform_continuous_of_continuous_at_zero.
theorem
topological_group.ext
{G : Type u_1}
[group G]
{t t' : topological_space G}
(tg : topological_group G)
(tg' : topological_group G)
(h : nhds 1 = nhds 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 : nhds 0 = nhds 0) :
t = t'
theorem
topological_group.of_nhds_aux
{G : Type u_1}
[group G]
[topological_space G]
(hinv : filter.tendsto (λ (x : G), x⁻¹) (nhds 1) (nhds 1))
(hleft : ∀ (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ * x) (nhds 1))
(hconj : ∀ (x₀ : G), filter.map (λ (x : G), x₀ * x * x₀⁻¹) (nhds 1) ≤ nhds 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) (nhds 0) (nhds 0))
(hleft : ∀ (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ + x) (nhds 0))
(hconj : ∀ (x₀ : G), filter.map (λ (x : G), x₀ + x + -x₀) (nhds 0) ≤ nhds 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) ((nhds 1).prod (nhds 1)) (nhds 1))
(hinv : filter.tendsto (λ (x : G), x⁻¹) (nhds 1) (nhds 1))
(hleft : ∀ (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ * x) (nhds 1))
(hright : ∀ (x₀ : G), nhds x₀ = filter.map (λ (x : G), x * x₀) (nhds 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) ((nhds 0).prod (nhds 0)) (nhds 0))
(hinv : filter.tendsto (λ (x : G), -x) (nhds 0) (nhds 0))
(hleft : ∀ (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ + x) (nhds 0))
(hright : ∀ (x₀ : G), nhds x₀ = filter.map (λ (x : G), x + x₀) (nhds 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) ((nhds 0).prod (nhds 0)) (nhds 0))
(hinv : filter.tendsto (λ (x : G), -x) (nhds 0) (nhds 0))
(hleft : ∀ (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ + x) (nhds 0))
(hconj : ∀ (x₀ : G), filter.tendsto (λ (x : G), x₀ + x + -x₀) (nhds 0) (nhds 0)) :
theorem
topological_group.of_nhds_one
{G : Type u}
[group G]
[topological_space G]
(hmul : filter.tendsto (function.uncurry has_mul.mul) ((nhds 1).prod (nhds 1)) (nhds 1))
(hinv : filter.tendsto (λ (x : G), x⁻¹) (nhds 1) (nhds 1))
(hleft : ∀ (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ * x) (nhds 1))
(hconj : ∀ (x₀ : G), filter.tendsto (λ (x : G), x₀ * x * x₀⁻¹) (nhds 1) (nhds 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) ((nhds 0).prod (nhds 0)) (nhds 0))
(hinv : filter.tendsto (λ (x : G), -x) (nhds 0) (nhds 0))
(hleft : ∀ (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ + x) (nhds 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) ((nhds 1).prod (nhds 1)) (nhds 1))
(hinv : filter.tendsto (λ (x : G), x⁻¹) (nhds 1) (nhds 1))
(hleft : ∀ (x₀ : G), nhds x₀ = filter.map (λ (x : G), x₀ * x) (nhds 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.
Instances of this typeclass
@[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 of this typeclass
@[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 (nhds a))
(hg : filter.tendsto g l (nhds b)) :
filter.tendsto (λ (x : α), f x / g x) l (nhds (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 (nhds a))
(hg : filter.tendsto g l (nhds b)) :
filter.tendsto (λ (x : α), f x - g x) l (nhds (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 (nhds c)) :
filter.tendsto (λ (k : α), b - f k) l (nhds (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 (nhds c)) :
filter.tendsto (λ (k : α), b / f k) l (nhds (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 (nhds c)) :
filter.tendsto (λ (k : α), f k / b) l (nhds (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 (nhds c)) :
filter.tendsto (λ (k : α), f k - b) l (nhds (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
@[simp]
theorem
homeomorph.sub_left_symm_apply
{G : Type w}
[add_group G]
[topological_space G]
[topological_add_group G]
(x ᾰ : G) :
def
homeomorph.div_left
{G : Type w}
[group G]
[topological_space G]
[topological_group G]
(x : G) :
G ≃ₜ G
A version of homeomorph.mul_left a b⁻¹ that is defeq to a / b.
Equations
- homeomorph.div_left x = {to_equiv := {to_fun := (equiv.div_left x).to_fun, inv_fun := (equiv.div_left x).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
def
homeomorph.sub_left
{G : Type w}
[add_group G]
[topological_space G]
[topological_add_group G]
(x : G) :
G ≃ₜ G
A version of homeomorph.add_left a (-b) that is defeq to a - b.
Equations
- homeomorph.sub_left x = {to_equiv := {to_fun := (equiv.sub_left x).to_fun, inv_fun := (equiv.sub_left x).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
homeomorph.div_left_symm_apply
{G : Type w}
[group G]
[topological_space G]
[topological_group G]
(x ᾰ : G) :
@[simp]
theorem
homeomorph.sub_left_apply
{G : Type w}
[add_group G]
[topological_space G]
[topological_add_group G]
(x ᾰ : G) :
⇑(homeomorph.sub_left x) ᾰ = x - ᾰ
@[simp]
theorem
homeomorph.div_left_apply
{G : Type w}
[group G]
[topological_space G]
[topological_group G]
(x ᾰ : G) :
⇑(homeomorph.div_left x) ᾰ = x / ᾰ
theorem
is_open_map_div_left
{G : Type w}
[group G]
[topological_space G]
[topological_group G]
(a : G) :
theorem
is_open_map_sub_left
{G : Type w}
[add_group G]
[topological_space G]
[topological_add_group G]
(a : G) :
theorem
is_closed_map_div_left
{G : Type w}
[group G]
[topological_space G]
[topological_group G]
(a : G) :
theorem
is_closed_map_sub_left
{G : Type w}
[add_group G]
[topological_space G]
[topological_add_group G]
(a : G) :
@[simp]
theorem
homeomorph.sub_right_symm_apply
{G : Type w}
[add_group G]
[topological_space G]
[topological_add_group G]
(x ᾰ : G) :
⇑((homeomorph.sub_right x).symm) ᾰ = ᾰ + x
@[simp]
theorem
homeomorph.div_right_symm_apply
{G : Type w}
[group G]
[topological_space G]
[topological_group G]
(x ᾰ : G) :
⇑((homeomorph.div_right x).symm) ᾰ = ᾰ * x
@[simp]
theorem
homeomorph.sub_right_apply
{G : Type w}
[add_group G]
[topological_space G]
[topological_add_group G]
(x ᾰ : G) :
⇑(homeomorph.sub_right x) ᾰ = ᾰ - x
@[simp]
theorem
homeomorph.div_right_apply
{G : Type w}
[group G]
[topological_space G]
[topological_group G]
(x ᾰ : G) :
⇑(homeomorph.div_right x) ᾰ = ᾰ / x
def
homeomorph.div_right
{G : Type w}
[group G]
[topological_space G]
[topological_group G]
(x : G) :
G ≃ₜ G
A version of homeomorph.mul_right a⁻¹ b that is defeq to b / a.
Equations
- homeomorph.div_right x = {to_equiv := {to_fun := (equiv.div_right x).to_fun, inv_fun := (equiv.div_right x).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
def
homeomorph.sub_right
{G : Type w}
[add_group G]
[topological_space G]
[topological_add_group G]
(x : G) :
G ≃ₜ G
A version of homeomorph.add_right (-a) b that is defeq to b - a.
Equations
- homeomorph.sub_right x = {to_equiv := {to_fun := (equiv.sub_right x).to_fun, inv_fun := (equiv.sub_right x).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
theorem
is_open_map_sub_right
{G : Type w}
[add_group G]
[topological_space G]
[topological_add_group G]
(a : G) :
is_open_map (λ (x : G), x - a)
theorem
is_open_map_div_right
{G : Type w}
[group G]
[topological_space G]
[topological_group G]
(a : G) :
is_open_map (λ (x : G), x / a)
theorem
is_closed_map_sub_right
{G : Type w}
[add_group G]
[topological_space G]
[topological_add_group G]
(a : G) :
is_closed_map (λ (x : G), x - a)
theorem
is_closed_map_div_right
{G : Type w}
[group G]
[topological_space G]
[topological_group G]
(a : G) :
is_closed_map (λ (x : G), x / a)
theorem
tendsto_div_nhds_one_iff
{G : Type w}
[group G]
[topological_space G]
[topological_group G]
{α : Type u_1}
{l : filter α}
{x : G}
{u : α → G} :
filter.tendsto (λ (n : α), u n / x) l (nhds 1) ↔ filter.tendsto u l (nhds x)
theorem
tendsto_sub_nhds_zero_iff
{G : Type w}
[add_group G]
[topological_space G]
[topological_add_group G]
{α : Type u_1}
{l : filter α}
{x : G}
{u : α → G} :
filter.tendsto (λ (n : α), u n - x) l (nhds 0) ↔ filter.tendsto u l (nhds x)
theorem
nhds_translation_div
{G : Type w}
[group G]
[topological_space G]
[topological_group G]
(x : G) :
filter.comap (λ (_x : G), _x / x) (nhds 1) = nhds x
theorem
nhds_translation_sub
{G : Type w}
[add_group G]
[topological_space G]
[topological_add_group G]
(x : G) :
filter.comap (λ (_x : G), _x - x) (nhds 0) = nhds x
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 α} :
theorem
is_open.div_left
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
{s t : set α}
(ht : is_open t) :
theorem
is_open.sub_left
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
{s t : set α}
(ht : is_open t) :
theorem
is_open.div_right
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
{s t : set α}
(hs : is_open s) :
theorem
is_open.sub_right
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
{s t : set α}
(hs : is_open s) :
theorem
subset_interior_div_left
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
{s t : set α} :
theorem
subset_interior_sub_left
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
{s t : set α} :
theorem
subset_interior_sub_right
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
{s t : set α} :
theorem
subset_interior_div_right
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
{s t : set α} :
theorem
subset_interior_sub
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
{s t : set α} :
theorem
subset_interior_div
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
{s t : set α} :
theorem
is_open.mul_closure
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
{s : set α}
(hs : is_open s)
(t : set α) :
theorem
is_open.add_closure
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
{s : set α}
(hs : is_open s)
(t : set α) :
theorem
is_open.closure_add
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
{t : set α}
(ht : is_open t)
(s : set α) :
theorem
is_open.closure_mul
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
{t : set α}
(ht : is_open t)
(s : set α) :
theorem
is_open.sub_closure
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
{s : set α}
(hs : is_open s)
(t : set α) :
theorem
is_open.div_closure
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
{s : set α}
(hs : is_open s)
(t : set α) :
theorem
is_open.closure_div
{α : Type u}
[topological_space α]
[group α]
[topological_group α]
{t : set α}
(ht : is_open t)
(s : set α) :
theorem
is_open.closure_sub
{α : Type u}
[topological_space α]
[add_group α]
[topological_add_group α]
{t : set α}
(ht : is_open t)
(s : set α) :
@[class]
- to_add_comm_group : add_comm_group G
- Z : filter G
- zero_Z : has_pure.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).prod (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.
Instances for add_group_with_zero_nhd
- add_group_with_zero_nhd.has_sizeof_inst
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
@[protected, instance]
def
subgroup.regular_quotient_of_is_closed
{G : Type w}
[topological_space G]
[group G]
[topological_group G]
(S : subgroup G)
[S.normal]
[is_closed ↑S] :
regular_space (G ⧸ S)
@[protected, instance]
def
add_subgroup.regular_quotient_of_is_closed
{G : Type w}
[topological_space G]
[add_group G]
[topological_add_group G]
(S : add_subgroup G)
[S.normal]
[is_closed ↑S] :
regular_space (G ⧸ S)
Some results about an open set containing the product of two sets in a topological group.
theorem
compact_open_separated_add_right
{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_right
{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 K * V ⊆ U.
theorem
compact_open_separated_add_left
{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 V + K ⊆ U.
theorem
compact_open_separated_mul_left
{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 V * K ⊆ 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 = nhds 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 = nhds 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
quotient_group.has_continuous_const_smul
{G : Type w}
[group G]
[topological_space G]
[topological_group G]
{Γ : subgroup G} :
has_continuous_const_smul G (G ⧸ Γ)
@[protected, instance]
def
quotient_add_group.has_continuous_const_vadd
{G : Type w}
[add_group G]
[topological_space G]
[topological_add_group G]
{Γ : add_subgroup G} :
has_continuous_const_vadd G (G ⧸ Γ)
theorem
quotient_add_group.continuous_smul₁
{G : Type w}
[add_group G]
[topological_space G]
[topological_add_group G]
{Γ : add_subgroup G}
(x : G ⧸ Γ) :
continuous (λ (g : G), g +ᵥ x)
theorem
quotient_group.continuous_smul₁
{G : Type w}
[group G]
[topological_space G]
[topological_group G]
{Γ : subgroup G}
(x : G ⧸ Γ) :
continuous (λ (g : G), g • x)
@[protected, instance]
def
quotient_add_group.has_continuous_vadd
{G : Type w}
[add_group G]
[topological_space G]
[topological_add_group G]
{Γ : add_subgroup G}
[locally_compact_space G] :
has_continuous_vadd G (G ⧸ Γ)
@[protected, instance]
def
quotient_group.has_continuous_smul
{G : Type w}
[group G]
[topological_space G]
[topological_group G]
{Γ : subgroup G}
[locally_compact_space G] :
has_continuous_smul G (G ⧸ Γ)
@[protected, instance]
def
add_units.topological_add_group
{α : Type u}
[add_monoid α]
[topological_space α]
[has_continuous_add α] :
@[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 := _}
theorem
topological_group_Inf
{G : Type w}
[group G]
{ts : set (topological_space G)}
(h : ∀ (t : topological_space G), t ∈ ts → topological_group G) :
theorem
topological_add_group_Inf
{G : Type w}
[add_group G]
{ts : set (topological_space G)}
(h : ∀ (t : topological_space G), t ∈ ts → topological_add_group G) :
theorem
topological_add_group_infi
{G : Type w}
{ι : Sort u_1}
[add_group G]
{ts' : ι → topological_space G}
(h' : ∀ (i : ι), topological_add_group G) :
theorem
topological_group_infi
{G : Type w}
{ι : Sort u_1}
[group G]
{ts' : ι → topological_space G}
(h' : ∀ (i : ι), topological_group G) :
theorem
topological_group_inf
{G : Type w}
[group G]
{t₁ t₂ : topological_space G}
(h₁ : topological_group G)
(h₂ : topological_group G) :
theorem
topological_add_group_inf
{G : Type w}
[add_group G]
{t₁ t₂ : topological_space G}
(h₁ : topological_add_group G)
(h₂ : topological_add_group G) :
theorem
topological_group_induced
{G : Type w}
{H : Type x}
[group G]
[group H]
{t : topological_space H}
[topological_group H]
{F : Type u_2}
[monoid_hom_class F G H]
(f : F) :
theorem
topological_add_group_induced
{G : Type w}
{H : Type x}
[add_group G]
[add_group H]
{t : topological_space H}
[topological_add_group H]
{F : Type u_2}
[add_monoid_hom_class F G H]
(f : F) :
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.
Instances for group_topology
- group_topology.has_sizeof_inst
- group_topology.partial_order
- group_topology.has_top
- group_topology.has_bot
- group_topology.bounded_order
- group_topology.has_inf
- group_topology.semilattice_inf
- group_topology.inhabited
- group_topology.has_Inf
- group_topology.complete_semilattice_Inf
- group_topology.complete_lattice
- 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.
Instances for add_group_topology
- add_group_topology.has_sizeof_inst
- add_group_topology.partial_order
- add_group_topology.has_top
- add_group_topology.has_bot
- add_group_topology.bounded_order
- add_group_topology.has_inf
- add_group_topology.semilattice_inf
- add_group_topology.inhabited
- add_group_topology.has_Inf
- add_group_topology.complete_semilattice_Inf
- add_group_topology.complete_lattice
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 := has_Inf.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 := has_Inf.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 := has_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 := has_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
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 : α → β) :