mathlib documentation

topology.algebra.open_subgroup

Open subgroups of a topological groups #

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 #

TODO #

source
structure open_add_subgroup (G : Type u_1) [add_group G] [topological_space G] :
Type u_1

The type of open subgroups of a topological additive group.

source
structure open_subgroup (G : Type u_1) [group G] [topological_space G] :
Type u_1

The type of open subgroups of a topological group.

source
@[protected, instance]
def open_add_subgroup.has_coe_set {G : Type u_1} [add_group G] [topological_space G] :
has_coe_t (open_add_subgroup G) (set G)
Equations
source
@[protected, instance]
def open_subgroup.has_coe_set {G : Type u_1} [group G] [topological_space G] :
has_coe_t (open_subgroup G) (set G)
Equations
source
@[protected, instance]
def open_subgroup.has_mem {G : Type u_1} [group G] [topological_space G] :
has_mem G (open_subgroup G)
Equations
source
@[protected, instance]
def open_add_subgroup.has_mem {G : Type u_1} [add_group G] [topological_space G] :
has_mem G (open_add_subgroup G)
Equations
source
@[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
source
@[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
source
@[protected, instance]
def open_subgroup.has_coe_opens {G : Type u_1} [group G] [topological_space G] :
has_coe_t (open_subgroup G) (topological_space.opens G)
Equations
source
@[protected, instance]
def open_add_subgroup.has_coe_opens {G : Type u_1} [add_group G] [topological_space G] :
has_coe_t (open_add_subgroup G) (topological_space.opens G)
Equations
source
@[simp, norm_cast]
theorem open_subgroup.mem_coe {G : Type u_1} [group G] [topological_space G] {U : open_subgroup G} {g : G} :
g ∈ ↑U ↔ g ∈ U
source
@[simp, norm_cast]
theorem open_add_subgroup.mem_coe {G : Type u_1} [add_group G] [topological_space G] {U : open_add_subgroup G} {g : G} :
g ∈ ↑U ↔ g ∈ U
source
@[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} :
g ∈ ↑U ↔ g ∈ U
source
@[simp, norm_cast]
theorem open_subgroup.mem_coe_opens {G : Type u_1} [group G] [topological_space G] {U : open_subgroup G} {g : G} :
g ∈ ↑U ↔ g ∈ U
source
@[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} :
g ∈ ↑U ↔ g ∈ U
source
@[simp, norm_cast]
theorem open_subgroup.mem_coe_subgroup {G : Type u_1} [group G] [topological_space G] {U : open_subgroup G} {g : G} :
g ∈ ↑U ↔ g ∈ U
source
theorem open_add_subgroup.coe_injective {G : Type u_1} [add_group G] [topological_space G] :
function.injective coe
source
theorem open_subgroup.coe_injective {G : Type u_1} [group G] [topological_space G] :
function.injective coe
source
@[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
source
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
source
theorem open_subgroup.ext_iff {G : Type u_1} [group G] [topological_space G] {U V : open_subgroup G} :
U = V ↔ ∀ (x : G), x ∈ U ↔ x ∈ V
source
theorem open_add_subgroup.ext_iff {G : Type u_1} [add_group G] [topological_space G] {U V : open_add_subgroup G} :
U = V ↔ ∀ (x : G), x ∈ U ↔ x ∈ V
source
@[protected]
theorem open_add_subgroup.is_open {G : Type u_1} [add_group G] [topological_space G] (U : open_add_subgroup G) :
is_open ↑U
source
@[protected]
theorem open_subgroup.is_open {G : Type u_1} [group G] [topological_space G] (U : open_subgroup G) :
is_open ↑U
source
@[protected]
theorem open_subgroup.one_mem {G : Type u_1} [group G] [topological_space G] (U : open_subgroup G) :
1 ∈ U
source
@[protected]
theorem open_add_subgroup.zero_mem {G : Type u_1} [add_group G] [topological_space G] (U : open_add_subgroup G) :
0 ∈ U
source
@[protected]
theorem open_subgroup.inv_mem {G : Type u_1} [group G] [topological_space G] (U : open_subgroup G) {g : G} (h : g ∈ U) :
g⁻¹ ∈ U
source
@[protected]
theorem open_add_subgroup.neg_mem {G : Type u_1} [add_group G] [topological_space G] (U : open_add_subgroup G) {g : G} (h : g ∈ U) :
-g ∈ U
source
@[protected]
theorem open_add_subgroup.add_mem {G : Type u_1} [add_group G] [topological_space G] (U : open_add_subgroup G) {g₁ g₂ : G} (h₁ : g₁ ∈ U) (h₂ : g₂ ∈ U) :
g₁ + g₂ ∈ U
source
@[protected]
theorem open_subgroup.mul_mem {G : Type u_1} [group G] [topological_space G] (U : open_subgroup G) {g₁ g₂ : G} (h₁ : g₁ ∈ U) (h₂ : g₂ ∈ U) :
g₁ * g₂ ∈ U
source
theorem open_subgroup.mem_nhds_one {G : Type u_1} [group G] [topological_space G] (U : open_subgroup G) :
↑U ∈ 𝓝 1
source
theorem open_add_subgroup.mem_nhds_zero {G : Type u_1} [add_group G] [topological_space G] (U : open_add_subgroup G) :
↑U ∈ 𝓝 0
source
@[protected, instance]
def open_subgroup.has_top {G : Type u_1} [group G] [topological_space G] :
has_top (open_subgroup G)
Equations
source
@[protected, instance]
def open_add_subgroup.has_top {G : Type u_1} [add_group G] [topological_space G] :
has_top (open_add_subgroup G)
Equations
source
@[protected, instance]
def open_subgroup.inhabited {G : Type u_1} [group G] [topological_space G] :
inhabited (open_subgroup G)
Equations
source
@[protected, instance]
def open_add_subgroup.inhabited {G : Type u_1} [add_group G] [topological_space G] :
inhabited (open_add_subgroup G)
Equations
source
theorem open_subgroup.is_closed {G : Type u_1} [group G] [topological_space G] [has_continuous_mul G] (U : open_subgroup G) :
is_closed ↑U
source
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) :
is_closed ↑U
source
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.

Equations
source
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.

Equations
source
@[protected, instance]
def open_subgroup.partial_order {G : Type u_1} [group G] [topological_space G] :
partial_order (open_subgroup G)
Equations
source
@[protected, instance]
def open_add_subgroup.partial_order {G : Type u_1} [add_group G] [topological_space G] :
partial_order (open_add_subgroup G)
Equations
source
@[protected, instance]
def open_add_subgroup.semilattice_inf {G : Type u_1} [add_group G] [topological_space G] :
semilattice_inf (open_add_subgroup G)
Equations
source
@[protected, instance]
def open_subgroup.semilattice_inf {G : Type u_1} [group G] [topological_space G] :
semilattice_inf (open_subgroup G)
Equations
source
@[protected, instance]
def open_subgroup.order_top {G : Type u_1} [group G] [topological_space G] :
order_top (open_subgroup G)
Equations
source
@[protected, instance]
def open_add_subgroup.order_top {G : Type u_1} [add_group G] [topological_space G] :
order_top (open_add_subgroup G)
Equations
source
@[simp, norm_cast]
theorem open_subgroup.coe_inf {G : Type u_1} [group G] [topological_space G] {U V : open_subgroup G} :
↑(U ⊓ V) = ↑U ∩ ↑V
source
@[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} :
↑(U ⊓ V) = ↑U ∩ ↑V
source
@[simp, norm_cast]
theorem open_subgroup.coe_subset {G : Type u_1} [group G] [topological_space G] {U V : open_subgroup G} :
↑U ⊆ ↑V ↔ U ≤ V
source
@[simp, norm_cast]
theorem open_add_subgroup.coe_subset {G : Type u_1} [add_group G] [topological_space G] {U V : open_add_subgroup G} :
↑U ⊆ ↑V ↔ U ≤ V
source
@[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} :
↑U ≤ ↑V ↔ U ≤ V
source
@[simp, norm_cast]
theorem open_subgroup.coe_subgroup_le {G : Type u_1} [group G] [topological_space G] {U V : open_subgroup G} :
↑U ≤ ↑V ↔ U ≤ V
source
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) :
open_add_subgroup G

The preimage of an open_add_subgroup along a continuous add_monoid homomorphism is an open_add_subgroup.

Equations
source
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) :
open_subgroup G

The preimage of an open_subgroup along a continuous monoid homomorphism is an open_subgroup.

Equations
source
@[simp]
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) :
↑(open_add_subgroup.comap f hf H) = ⇑f ⁻¹' ↑H
source
@[simp]
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) :
↑(open_subgroup.comap f hf H) = ⇑f ⁻¹' ↑H
source
@[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
source
@[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
source
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
source
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
source
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 ∈ 𝓝 g) :
is_open ↑H
source
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 ∈ 𝓝 g) :
is_open ↑H
source
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.to_subgroup ≤ H) :
is_open ↑H
source
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.to_add_subgroup ≤ H) :
is_open ↑H
source
theorem add_subgroup.is_open_of_zero_mem_interior {G : Type u_1} [add_group G] [topological_space G] [topological_add_group G] {H : add_subgroup G} (h_1_int : 0 ∈ interior ↑H) :
is_open ↑H

If a subgroup of an additive topological group has 0 in its interior, then it is open.

source
theorem subgroup.is_open_of_one_mem_interior {G : Type u_1} [group G] [topological_space G] [topological_group G] {H : subgroup G} (h_1_int : 1 ∈ interior ↑H) :
is_open ↑H

If a subgroup of a topological group has 1 in its interior, then it is open.

source
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₁) :
is_open ↑H₂
source
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₁) :
is_open ↑H₂
source
@[protected, instance]
def open_subgroup.semilattice_sup {G : Type u_1} [group G] [topological_space G] [has_continuous_mul G] :
semilattice_sup (open_subgroup G)
Equations
source
@[protected, instance]
def open_add_subgroup.semilattice_sup {G : Type u_1} [add_group G] [topological_space G] [has_continuous_add G] :
semilattice_sup (open_add_subgroup G)
Equations
source
@[protected, instance]
def open_subgroup.lattice {G : Type u_1} [group G] [topological_space G] [has_continuous_mul G] :
lattice (open_subgroup G)
Equations
source
@[protected, instance]
def open_add_subgroup.lattice {G : Type u_1} [add_group G] [topological_space G] [has_continuous_add G] :
lattice (open_add_subgroup G)
Equations
source
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) :
is_open ↑P
source
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) :
is_open ↑I