mathlib docs: topology.algebra.open

source

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

Type u_1

carrier : set G
zero_mem' : 0 ∈ c.carrier
add_mem' : ∀ {a b : G}, a ∈ c.carrier → b ∈ c.carrier → a + b ∈ c.carrier
neg_mem' : ∀ {x : G}, x ∈ c.carrier → -x ∈ c.carrier
is_open' : is_open c.carrier

The type of open subgroups of a topological additive group.

source

def open_add_subgroup.to_add_subgroup {G : Type u_1} [add_group G] [topological_space G] (s : open_add_subgroup G) :

add_subgroup G

Reinterpret an open_add_subgroup as an add_subgroup.

source

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

subgroup G

Reinterpret an open_subgroup as a subgroup.

source

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

Type u_1

carrier : set G
one_mem' : 1 ∈ c.carrier
mul_mem' : ∀ {a b : G}, a ∈ c.carrier → b ∈ c.carrier → a * b ∈ c.carrier
inv_mem' : ∀ {x : G}, x ∈ c.carrier → x⁻¹ ∈ c.carrier
is_open' : is_open c.carrier

The type of open subgroups of a topological group.

source

@[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)

source

@[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

open_subgroup.has_coe_set = {coe := λ (U : open_subgroup G), U.carrier}

source

@[instance]

def open_subgroup.has_mem {G : Type u_1} [group G] [topological_space G] :

has_mem G (open_subgroup G)

Equations

open_subgroup.has_mem = {mem := λ (g : G) (U : open_subgroup G), g ∈ ↑U}

source

@[instance]

def open_add_subgroup.has_mem {G : Type u_1} [add_group G] [topological_space G] :

has_mem G (open_add_subgroup G)

source

@[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}

source

@[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)

source

@[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

open_subgroup.has_coe_opens = {coe := λ (U : open_subgroup G), ⟨↑U, _⟩}

source

@[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)

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

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

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

theorem open_subgroup.is_open {G : Type u_1} [group G] [topological_space G] (U : open_subgroup G) :

is_open ↑U

source

theorem open_subgroup.one_mem {G : Type u_1} [group G] [topological_space G] (U : open_subgroup G) :

1 ∈ U

source

theorem open_add_subgroup.zero_mem {G : Type u_1} [add_group G] [topological_space G] (U : open_add_subgroup G) :

0 ∈ U

source

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

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

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

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

@[instance]

def open_subgroup.has_top {G : Type u_1} [group G] [topological_space G] :

has_top (open_subgroup G)

Equations

open_subgroup.has_top = {top := {carrier := ⊤.carrier, one_mem' := _, mul_mem' := _, inv_mem' := _, is_open' := _}}

source

@[instance]

def open_add_subgroup.has_top {G : Type u_1} [add_group G] [topological_space G] :

has_top (open_add_subgroup G)

source

@[instance]

def open_subgroup.inhabited {G : Type u_1} [group G] [topological_space G] :

inhabited (open_subgroup G)

Equations

open_subgroup.inhabited = {default := ⊤}

source

@[instance]

def open_add_subgroup.inhabited {G : Type u_1} [add_group G] [topological_space G] :

inhabited (open_add_subgroup G)

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)

Equations

U.prod V = {carrier := ↑U.prod ↑V, one_mem' := _, mul_mem' := _, inv_mem' := _, is_open' := _}

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)

source

@[instance]

def open_subgroup.partial_order {G : Type u_1} [group G] [topological_space G] :

partial_order (open_subgroup G)

Equations

open_subgroup.partial_order = {le := λ (U V : open_subgroup G), ∀ ⦃x : G⦄, x ∈ U → x ∈ V, lt := partial_order.lt (partial_order.lift coe open_subgroup.coe_injective), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

@[instance]

def open_add_subgroup.partial_order {G : Type u_1} [add_group G] [topological_space G] :

partial_order (open_add_subgroup G)

source

@[instance]

def open_add_subgroup.semilattice_inf_top {G : Type u_1} [add_group G] [topological_space G] :

semilattice_inf_top (open_add_subgroup G)

source

@[instance]

def open_subgroup.semilattice_inf_top {G : Type u_1} [group G] [topological_space G] :

semilattice_inf_top (open_subgroup G)

Equations

open_subgroup.semilattice_inf_top = {top := ⊤, le := partial_order.le open_subgroup.partial_order, lt := partial_order.lt open_subgroup.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, inf := λ (U V : open_subgroup G), {carrier := (↑U ⊓ ↑V).carrier, one_mem' := _, mul_mem' := _, inv_mem' := _, is_open' := _}, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[simp]

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]

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]

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]

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]

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]

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

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.carrier ≤ ↑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.carrier ≤ ↑H) :

is_open ↑H

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

@[instance]

def open_subgroup.semilattice_sup_top {G : Type u_1} [group G] [topological_space G] [has_continuous_mul G] :

semilattice_sup_top (open_subgroup G)

Equations

open_subgroup.semilattice_sup_top = {top := semilattice_inf_top.top open_subgroup.semilattice_inf_top, le := semilattice_inf_top.le open_subgroup.semilattice_inf_top, lt := semilattice_inf_top.lt open_subgroup.semilattice_inf_top, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _, sup := λ (U V : open_subgroup G), {carrier := (↑U ⊔ ↑V).carrier, one_mem' := _, mul_mem' := _, inv_mem' := _, is_open' := _}, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[instance]

def open_add_subgroup.semilattice_sup_top {G : Type u_1} [add_group G] [topological_space G] [has_continuous_add G] :

semilattice_sup_top (open_add_subgroup G)

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