mathlib documentation

topology.algebra.open_subgroup

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.

def open_subgroup.to_subgroup {G : Type u_1} [group G] [topological_space G] (s : open_subgroup G) :

Reinterpret an open_subgroup as a subgroup.

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

The type of open subgroups of a topological group.

@[instance]
Equations
@[instance]
def open_subgroup.has_mem {G : Type u_1} [group G] [topological_space G] :
Equations
@[instance]
@[simp]
theorem open_subgroup.mem_coe {G : Type u_1} [group G] [topological_space G] {U : open_subgroup G} {g : G} :
g U g U
@[simp]
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
@[simp]
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
@[simp]
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
@[simp]
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
@[simp]
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
@[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
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
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
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
theorem open_subgroup.is_open {G : Type u_1} [group G] [topological_space G] (U : open_subgroup G) :
theorem open_subgroup.one_mem {G : Type u_1} [group G] [topological_space G] (U : open_subgroup G) :
1 U
theorem open_add_subgroup.zero_mem {G : Type u_1} [add_group G] [topological_space G] (U : open_add_subgroup G) :
0 U
theorem open_subgroup.inv_mem {G : Type u_1} [group G] [topological_space G] (U : open_subgroup G) {g : G} (h : g U) :
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
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
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
theorem open_subgroup.mem_nhds_one {G : Type u_1} [group G] [topological_space G] (U : open_subgroup G) :
@[instance]
Equations
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) :

The product of two open subgroups as an open subgroup of the product group.

Equations
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) :

The product of two open subgroups as an open subgroup of the product group.

@[simp]
theorem open_subgroup.coe_inf {G : Type u_1} [group G] [topological_space G] {U V : open_subgroup G} :
(U V) = U V
@[simp]
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
@[simp]
theorem open_subgroup.coe_subset {G : Type u_1} [group G] [topological_space G] {U V : open_subgroup G} :
U V U V
@[simp]
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
@[simp]
@[simp]
theorem open_subgroup.coe_subgroup_le {G : Type u_1} [group G] [topological_space G] {U V : open_subgroup G} :
U V U V
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.

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
@[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) :
@[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) :
@[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} :
@[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} :
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₁) :
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) :
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) :
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 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) :