Open subgroups of a topological groups #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This files builds the lattice open_subgroup G of open subgroups in a topological group G,
and its additive version open_add_subgroup. This lattice has a top element, the subgroup of all
elements, but no bottom element in general. The trivial subgroup which is the natural candidate
bottom has no reason to be open (this happens only in discrete groups).
Note that this notion is especially relevant in a non-archimedean context, for instance for
p-adic groups.
Main declarations #
open_subgroup.is_closed: An open subgroup is automatically closed.subgroup.is_open_mono: A subgroup containing an open subgroup is open. There are also versions for additive groups, submodules and ideals.open_subgroup.comap: Open subgroups can be pulled back by a continuous group morphism.
TODO #
- Prove that the identity component of a locally path connected group is an open subgroup. Up to now this file is really geared towards non-archimedean algebra, not Lie groups.
- to_add_subgroup : add_subgroup G
- is_open' : is_open self.to_add_subgroup.carrier
The type of open subgroups of a topological additive group.
Instances for open_add_subgroup
- open_add_subgroup.has_sizeof_inst
- open_add_subgroup.has_coe_add_subgroup
- open_add_subgroup.set_like
- open_add_subgroup.add_subgroup_class
- open_add_subgroup.has_coe_opens
- open_add_subgroup.has_top
- open_add_subgroup.inhabited
- open_add_subgroup.has_inf
- open_add_subgroup.semilattice_inf
- open_add_subgroup.order_top
- open_add_subgroup.has_sup
- open_add_subgroup.lattice
- to_subgroup : subgroup G
- is_open' : is_open self.to_subgroup.carrier
The type of open subgroups of a topological group.
Instances for open_subgroup
- open_subgroup.has_sizeof_inst
- open_subgroup.has_coe_subgroup
- open_subgroup.set_like
- open_subgroup.subgroup_class
- open_subgroup.has_coe_opens
- open_subgroup.has_top
- open_subgroup.inhabited
- open_subgroup.has_inf
- open_subgroup.semilattice_inf
- open_subgroup.order_top
- open_subgroup.has_sup
- open_subgroup.lattice
@[protected, instance]
def
open_subgroup.has_coe_subgroup
{G : Type u_1}
[group G]
[topological_space G] :
has_coe_t (open_subgroup G) (subgroup G)
Equations
- open_subgroup.has_coe_subgroup = {coe := open_subgroup.to_subgroup _inst_2}
@[protected, instance]
def
open_add_subgroup.has_coe_add_subgroup
{G : Type u_1}
[add_group G]
[topological_space G] :
has_coe_t (open_add_subgroup G) (add_subgroup G)
Equations
theorem
open_add_subgroup.coe_add_subgroup_injective
{G : Type u_1}
[add_group G]
[topological_space G] :
@[protected, instance]
def
open_subgroup.set_like
{G : Type u_1}
[group G]
[topological_space G] :
set_like (open_subgroup G) G
Equations
- open_subgroup.set_like = {coe := λ (U : open_subgroup G), ↑(U.to_subgroup), coe_injective' := _}
@[protected, instance]
def
open_add_subgroup.set_like
{G : Type u_1}
[add_group G]
[topological_space G] :
set_like (open_add_subgroup G) G
Equations
- open_add_subgroup.set_like = {coe := λ (U : open_add_subgroup G), ↑(U.to_add_subgroup), coe_injective' := _}
@[protected, instance]
def
open_subgroup.subgroup_class
{G : Type u_1}
[group G]
[topological_space G] :
subgroup_class (open_subgroup G) G
@[protected, instance]
@[protected, instance]
Equations
- open_subgroup.has_coe_opens = {coe := λ (U : open_subgroup G), {carrier := ↑U, is_open' := _}}
@[protected, instance]
Equations
- open_add_subgroup.has_coe_opens = {coe := λ (U : open_add_subgroup G), {carrier := ↑U, is_open' := _}}
@[simp, norm_cast]
theorem
open_add_subgroup.coe_coe_opens
{G : Type u_1}
[add_group G]
[topological_space G]
{U : open_add_subgroup G} :
@[simp, norm_cast]
theorem
open_subgroup.coe_coe_opens
{G : Type u_1}
[group G]
[topological_space G]
{U : open_subgroup G} :
@[simp, norm_cast]
theorem
open_subgroup.coe_coe_subgroup
{G : Type u_1}
[group G]
[topological_space G]
{U : open_subgroup G} :
@[simp, norm_cast]
theorem
open_add_subgroup.coe_coe_add_subgroup
{G : Type u_1}
[add_group G]
[topological_space G]
{U : open_add_subgroup G} :
@[simp, norm_cast]
theorem
open_add_subgroup.mem_coe_opens
{G : Type u_1}
[add_group G]
[topological_space G]
{U : open_add_subgroup G}
{g : G} :
@[simp, norm_cast]
theorem
open_subgroup.mem_coe_opens
{G : Type u_1}
[group G]
[topological_space G]
{U : open_subgroup G}
{g : G} :
@[simp, norm_cast]
theorem
open_add_subgroup.mem_coe_add_subgroup
{G : Type u_1}
[add_group G]
[topological_space G]
{U : open_add_subgroup G}
{g : G} :
@[simp, norm_cast]
theorem
open_subgroup.mem_coe_subgroup
{G : Type u_1}
[group G]
[topological_space G]
{U : open_subgroup G}
{g : G} :
@[ext]
theorem
open_subgroup.ext
{G : Type u_1}
[group G]
[topological_space G]
{U V : open_subgroup G}
(h : ∀ (x : G), x ∈ U ↔ x ∈ V) :
U = V
@[ext]
theorem
open_add_subgroup.ext
{G : Type u_1}
[add_group G]
[topological_space G]
{U V : open_add_subgroup G}
(h : ∀ (x : G), x ∈ U ↔ x ∈ V) :
U = V
@[protected]
theorem
open_add_subgroup.is_open
{G : Type u_1}
[add_group G]
[topological_space G]
(U : open_add_subgroup G) :
@[protected]
theorem
open_subgroup.is_open
{G : Type u_1}
[group G]
[topological_space G]
(U : open_subgroup G) :
theorem
open_subgroup.mem_nhds_one
{G : Type u_1}
[group G]
[topological_space G]
(U : open_subgroup G) :
theorem
open_add_subgroup.mem_nhds_zero
{G : Type u_1}
[add_group G]
[topological_space G]
(U : open_add_subgroup G) :
@[protected, instance]
def
open_subgroup.has_top
{G : Type u_1}
[group G]
[topological_space G] :
has_top (open_subgroup G)
@[protected, instance]
@[simp]
@[simp]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem
open_subgroup.is_closed
{G : Type u_1}
[group G]
[topological_space G]
[has_continuous_mul G]
(U : open_subgroup G) :
theorem
open_add_subgroup.is_closed
{G : Type u_1}
[add_group G]
[topological_space G]
[has_continuous_add G]
(U : open_add_subgroup G) :
theorem
open_subgroup.is_clopen
{G : Type u_1}
[group G]
[topological_space G]
[has_continuous_mul G]
(U : open_subgroup G) :
theorem
open_add_subgroup.is_clopen
{G : Type u_1}
[add_group G]
[topological_space G]
[has_continuous_add G]
(U : open_add_subgroup G) :
def
open_subgroup.prod
{G : Type u_1}
[group G]
[topological_space G]
{H : Type u_2}
[group H]
[topological_space H]
(U : open_subgroup G)
(V : open_subgroup H) :
open_subgroup (G × H)
The product of two open subgroups as an open subgroup of the product group.
def
open_add_subgroup.sum
{G : Type u_1}
[add_group G]
[topological_space G]
{H : Type u_2}
[add_group H]
[topological_space H]
(U : open_add_subgroup G)
(V : open_add_subgroup H) :
open_add_subgroup (G × H)
The product of two open subgroups as an open subgroup of the product group.
@[simp, norm_cast]
theorem
open_add_subgroup.coe_sum
{G : Type u_1}
[add_group G]
[topological_space G]
{H : Type u_2}
[add_group H]
[topological_space H]
(U : open_add_subgroup G)
(V : open_add_subgroup H) :
@[simp, norm_cast]
theorem
open_subgroup.coe_prod
{G : Type u_1}
[group G]
[topological_space G]
{H : Type u_2}
[group H]
[topological_space H]
(U : open_subgroup G)
(V : open_subgroup H) :
@[simp, norm_cast]
theorem
open_add_subgroup.coe_add_subgroup_sum
{G : Type u_1}
[add_group G]
[topological_space G]
{H : Type u_2}
[add_group H]
[topological_space H]
(U : open_add_subgroup G)
(V : open_add_subgroup H) :
@[simp, norm_cast]
theorem
open_subgroup.coe_subgroup_prod
{G : Type u_1}
[group G]
[topological_space G]
{H : Type u_2}
[group H]
[topological_space H]
(U : open_subgroup G)
(V : open_subgroup H) :
@[protected, instance]
def
open_subgroup.has_inf
{G : Type u_1}
[group G]
[topological_space G] :
has_inf (open_subgroup G)
Equations
- open_subgroup.has_inf = {inf := λ (U V : open_subgroup G), {to_subgroup := ↑U ⊓ ↑V, is_open' := _}}
@[protected, instance]
Equations
- open_add_subgroup.has_inf = {inf := λ (U V : open_add_subgroup G), {to_add_subgroup := ↑U ⊓ ↑V, is_open' := _}}
@[simp, norm_cast]
theorem
open_subgroup.coe_inf
{G : Type u_1}
[group G]
[topological_space G]
{U V : open_subgroup G} :
@[simp, norm_cast]
theorem
open_add_subgroup.coe_inf
{G : Type u_1}
[add_group G]
[topological_space G]
{U V : open_add_subgroup G} :
@[simp, norm_cast]
theorem
open_add_subgroup.coe_add_subgroup_inf
{G : Type u_1}
[add_group G]
[topological_space G]
{U V : open_add_subgroup G} :
@[simp, norm_cast]
theorem
open_subgroup.coe_subgroup_inf
{G : Type u_1}
[group G]
[topological_space G]
{U V : open_subgroup G} :
@[simp, norm_cast]
theorem
open_subgroup.coe_opens_inf
{G : Type u_1}
[group G]
[topological_space G]
{U V : open_subgroup G} :
@[simp, norm_cast]
theorem
open_add_subgroup.coe_opens_inf
{G : Type u_1}
[add_group G]
[topological_space G]
{U V : open_add_subgroup G} :
@[simp]
theorem
open_subgroup.mem_inf
{G : Type u_1}
[group G]
[topological_space G]
{U V : open_subgroup G}
{x : G} :
@[simp]
theorem
open_add_subgroup.mem_inf
{G : Type u_1}
[add_group G]
[topological_space G]
{U V : open_add_subgroup G}
{x : G} :
@[protected, instance]
Equations
- open_add_subgroup.semilattice_inf = {inf := semilattice_inf.inf (function.injective.semilattice_inf coe open_add_subgroup.semilattice_inf._proof_1 open_add_subgroup.semilattice_inf._proof_2), le := partial_order.le set_like.partial_order, lt := partial_order.lt set_like.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}
@[protected, instance]
Equations
- open_subgroup.semilattice_inf = {inf := semilattice_inf.inf (function.injective.semilattice_inf coe open_subgroup.semilattice_inf._proof_1 open_subgroup.semilattice_inf._proof_2), le := partial_order.le set_like.partial_order, lt := partial_order.lt set_like.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}
@[protected, instance]
@[protected, instance]
@[simp, norm_cast]
theorem
open_add_subgroup.coe_add_subgroup_le
{G : Type u_1}
[add_group G]
[topological_space G]
{U V : open_add_subgroup G} :
@[simp, norm_cast]
theorem
open_subgroup.coe_subgroup_le
{G : Type u_1}
[group G]
[topological_space G]
{U V : open_subgroup G} :
def
open_add_subgroup.comap
{G : Type u_1}
[add_group G]
[topological_space G]
{N : Type u_2}
[add_group N]
[topological_space N]
(f : G →+ N)
(hf : continuous ⇑f)
(H : open_add_subgroup N) :
The preimage of an open_add_subgroup along a continuous add_monoid homomorphism
is an open_add_subgroup.
Equations
- open_add_subgroup.comap f hf H = {to_add_subgroup := {carrier := (add_subgroup.comap f ↑H).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}, is_open' := _}
def
open_subgroup.comap
{G : Type u_1}
[group G]
[topological_space G]
{N : Type u_2}
[group N]
[topological_space N]
(f : G →* N)
(hf : continuous ⇑f)
(H : open_subgroup N) :
The preimage of an open_subgroup along a continuous monoid homomorphism
is an open_subgroup.
Equations
- open_subgroup.comap f hf H = {to_subgroup := {carrier := (subgroup.comap f ↑H).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}, is_open' := _}
@[simp, norm_cast]
theorem
open_add_subgroup.coe_comap
{G : Type u_1}
[add_group G]
[topological_space G]
{N : Type u_2}
[add_group N]
[topological_space N]
(H : open_add_subgroup N)
(f : G →+ N)
(hf : continuous ⇑f) :
@[simp, norm_cast]
theorem
open_subgroup.coe_comap
{G : Type u_1}
[group G]
[topological_space G]
{N : Type u_2}
[group N]
[topological_space N]
(H : open_subgroup N)
(f : G →* N)
(hf : continuous ⇑f) :
@[simp, norm_cast]
theorem
open_subgroup.coe_subgroup_comap
{G : Type u_1}
[group G]
[topological_space G]
{N : Type u_2}
[group N]
[topological_space N]
(H : open_subgroup N)
(f : G →* N)
(hf : continuous ⇑f) :
↑(open_subgroup.comap f hf H) = subgroup.comap f ↑H
@[simp, norm_cast]
theorem
open_add_subgroup.coe_add_subgroup_comap
{G : Type u_1}
[add_group G]
[topological_space G]
{N : Type u_2}
[add_group N]
[topological_space N]
(H : open_add_subgroup N)
(f : G →+ N)
(hf : continuous ⇑f) :
↑(open_add_subgroup.comap f hf H) = add_subgroup.comap f ↑H
@[simp]
theorem
open_subgroup.mem_comap
{G : Type u_1}
[group G]
[topological_space G]
{N : Type u_2}
[group N]
[topological_space N]
{H : open_subgroup N}
{f : G →* N}
{hf : continuous ⇑f}
{x : G} :
x ∈ open_subgroup.comap f hf H ↔ ⇑f x ∈ H
@[simp]
theorem
open_add_subgroup.mem_comap
{G : Type u_1}
[add_group G]
[topological_space G]
{N : Type u_2}
[add_group N]
[topological_space N]
{H : open_add_subgroup N}
{f : G →+ N}
{hf : continuous ⇑f}
{x : G} :
x ∈ open_add_subgroup.comap f hf H ↔ ⇑f x ∈ H
theorem
open_subgroup.comap_comap
{G : Type u_1}
[group G]
[topological_space G]
{N : Type u_2}
[group N]
[topological_space N]
{P : Type u_3}
[group P]
[topological_space P]
(K : open_subgroup P)
(f₂ : N →* P)
(hf₂ : continuous ⇑f₂)
(f₁ : G →* N)
(hf₁ : continuous ⇑f₁) :
open_subgroup.comap f₁ hf₁ (open_subgroup.comap f₂ hf₂ K) = open_subgroup.comap (f₂.comp f₁) _ K
theorem
open_add_subgroup.comap_comap
{G : Type u_1}
[add_group G]
[topological_space G]
{N : Type u_2}
[add_group N]
[topological_space N]
{P : Type u_3}
[add_group P]
[topological_space P]
(K : open_add_subgroup P)
(f₂ : N →+ P)
(hf₂ : continuous ⇑f₂)
(f₁ : G →+ N)
(hf₁ : continuous ⇑f₁) :
open_add_subgroup.comap f₁ hf₁ (open_add_subgroup.comap f₂ hf₂ K) = open_add_subgroup.comap (f₂.comp f₁) _ K
theorem
subgroup.is_open_of_mem_nhds
{G : Type u_1}
[group G]
[topological_space G]
[has_continuous_mul G]
(H : subgroup G)
{g : G}
(hg : ↑H ∈ nhds g) :
theorem
add_subgroup.is_open_of_mem_nhds
{G : Type u_1}
[add_group G]
[topological_space G]
[has_continuous_add G]
(H : add_subgroup G)
{g : G}
(hg : ↑H ∈ nhds g) :
theorem
subgroup.is_open_mono
{G : Type u_1}
[group G]
[topological_space G]
[has_continuous_mul G]
{H₁ H₂ : subgroup G}
(h : H₁ ≤ H₂)
(h₁ : is_open ↑H₁) :
theorem
add_subgroup.is_open_mono
{G : Type u_1}
[add_group G]
[topological_space G]
[has_continuous_add G]
{H₁ H₂ : add_subgroup G}
(h : H₁ ≤ H₂)
(h₁ : is_open ↑H₁) :
theorem
subgroup.is_open_of_open_subgroup
{G : Type u_1}
[group G]
[topological_space G]
[has_continuous_mul G]
(H : subgroup G)
{U : open_subgroup G}
(h : ↑U ≤ H) :
theorem
add_subgroup.is_open_of_open_add_subgroup
{G : Type u_1}
[add_group G]
[topological_space G]
[has_continuous_add G]
(H : add_subgroup G)
{U : open_add_subgroup G}
(h : ↑U ≤ H) :
theorem
add_subgroup.is_open_of_zero_mem_interior
{G : Type u_1}
[add_group G]
[topological_space G]
[has_continuous_add G]
(H : add_subgroup G)
(h_1_int : 0 ∈ interior ↑H) :
If a subgroup of an additive topological group has 0 in its interior, then it is
open.
theorem
subgroup.is_open_of_one_mem_interior
{G : Type u_1}
[group G]
[topological_space G]
[has_continuous_mul G]
(H : subgroup G)
(h_1_int : 1 ∈ interior ↑H) :
If a subgroup of a topological group has 1 in its interior, then it is open.
@[protected, instance]
def
open_subgroup.has_sup
{G : Type u_1}
[group G]
[topological_space G]
[has_continuous_mul G] :
has_sup (open_subgroup G)
Equations
- open_subgroup.has_sup = {sup := λ (U V : open_subgroup G), {to_subgroup := ↑U ⊔ ↑V, is_open' := _}}
@[protected, instance]
def
open_add_subgroup.has_sup
{G : Type u_1}
[add_group G]
[topological_space G]
[has_continuous_add G] :
Equations
- open_add_subgroup.has_sup = {sup := λ (U V : open_add_subgroup G), {to_add_subgroup := ↑U ⊔ ↑V, is_open' := _}}
@[simp, norm_cast]
theorem
open_add_subgroup.coe_add_subgroup_sup
{G : Type u_1}
[add_group G]
[topological_space G]
[has_continuous_add G]
(U V : open_add_subgroup G) :
@[simp, norm_cast]
theorem
open_subgroup.coe_subgroup_sup
{G : Type u_1}
[group G]
[topological_space G]
[has_continuous_mul G]
(U V : open_subgroup G) :
@[protected, instance]
def
open_subgroup.lattice
{G : Type u_1}
[group G]
[topological_space G]
[has_continuous_mul G] :
lattice (open_subgroup G)
Equations
- open_subgroup.lattice = {sup := semilattice_sup.sup (function.injective.semilattice_sup coe open_subgroup.coe_subgroup_injective open_subgroup.lattice._proof_1), le := semilattice_inf.le open_subgroup.semilattice_inf, lt := semilattice_inf.lt open_subgroup.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf open_subgroup.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
@[protected, instance]
def
open_add_subgroup.lattice
{G : Type u_1}
[add_group G]
[topological_space G]
[has_continuous_add G] :
Equations
- open_add_subgroup.lattice = {sup := semilattice_sup.sup (function.injective.semilattice_sup coe open_add_subgroup.coe_add_subgroup_injective open_add_subgroup.lattice._proof_1), le := semilattice_inf.le open_add_subgroup.semilattice_inf, lt := semilattice_inf.lt open_add_subgroup.semilattice_inf, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf open_add_subgroup.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}
theorem
submodule.is_open_mono
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[topological_space M]
[topological_add_group M]
[module R M]
{U P : submodule R M}
(h : U ≤ P)
(hU : is_open ↑U) :
theorem
ideal.is_open_of_open_subideal
{R : Type u_1}
[comm_ring R]
[topological_space R]
[topological_ring R]
{U I : ideal R}
(h : U ≤ I)
(hU : is_open ↑U) :