Documentation

Mathlib.Topology.Algebra.OpenSubgroup

Open subgroups of a topological groups #

This files builds the lattice OpenSubgroup G of open subgroups in a topological group G, and its additive version OpenAddSubgroup. 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 #

OpenSubgroup.isClosed: An open subgroup is automatically closed.
Subgroup.isOpen_mono: A subgroup containing an open subgroup is open. There are also versions for additive groups, submodules and ideals.
OpenSubgroup.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.

structure OpenAddSubgroup (G : Type u_1) [AddGroup G] [TopologicalSpace G] extends AddSubgroup :

Type u_1

The type of open subgroups of a topological additive group.

carrier : Set G
add_mem' : ∀ {a b : G}, a ∈ (↑self).carrier → b ∈ (↑self).carrier → a + b ∈ (↑self).carrier
zero_mem' : 0 ∈ (↑self).carrier
neg_mem' : ∀ {x : G}, x ∈ (↑self).carrier → -x ∈ (↑self).carrier
isOpen' : IsOpen (↑self).carrier

Instances For

theorem OpenAddSubgroup.isOpen' {G : Type u_1} [AddGroup G] [TopologicalSpace G] (self : OpenAddSubgroup G) :

IsOpen (↑self).carrier

structure OpenSubgroup (G : Type u_1) [Group G] [TopologicalSpace G] extends Subgroup :

Type u_1

The type of open subgroups of a topological group.

carrier : Set G
mul_mem' : ∀ {a b : G}, a ∈ (↑self).carrier → b ∈ (↑self).carrier → a * b ∈ (↑self).carrier
one_mem' : 1 ∈ (↑self).carrier
inv_mem' : ∀ {x : G}, x ∈ (↑self).carrier → x⁻¹ ∈ (↑self).carrier
isOpen' : IsOpen (↑self).carrier

Instances For

theorem OpenSubgroup.isOpen' {G : Type u_1} [Group G] [TopologicalSpace G] (self : OpenSubgroup G) :

IsOpen (↑self).carrier

instance OpenAddSubgroup.hasCoeAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] :

CoeTC (OpenAddSubgroup G) (AddSubgroup G)

Equations

OpenAddSubgroup.hasCoeAddSubgroup = { coe := OpenAddSubgroup.toAddSubgroup }

instance OpenSubgroup.hasCoeSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] :

CoeTC (OpenSubgroup G) (Subgroup G)

Equations

OpenSubgroup.hasCoeSubgroup = { coe := OpenSubgroup.toSubgroup }

theorem OpenAddSubgroup.toAddSubgroup_injective {G : Type u_1} [AddGroup G] [TopologicalSpace G] :

Function.Injective OpenAddSubgroup.toAddSubgroup

theorem OpenSubgroup.toSubgroup_injective {G : Type u_1} [Group G] [TopologicalSpace G] :

Function.Injective OpenSubgroup.toSubgroup

instance OpenAddSubgroup.instSetLike {G : Type u_1} [AddGroup G] [TopologicalSpace G] :

SetLike (OpenAddSubgroup G) G

Equations

OpenAddSubgroup.instSetLike = { coe := fun (U : OpenAddSubgroup G) => ↑↑U, coe_injective' := ⋯ }

instance OpenSubgroup.instSetLike {G : Type u_1} [Group G] [TopologicalSpace G] :

SetLike (OpenSubgroup G) G

Equations

OpenSubgroup.instSetLike = { coe := fun (U : OpenSubgroup G) => ↑↑U, coe_injective' := ⋯ }

instance OpenAddSubgroup.instAddSubgroupClass {G : Type u_1} [AddGroup G] [TopologicalSpace G] :

AddSubgroupClass (OpenAddSubgroup G) G

Equations

⋯ = ⋯

instance OpenSubgroup.instSubgroupClass {G : Type u_1} [Group G] [TopologicalSpace G] :

SubgroupClass (OpenSubgroup G) G

Equations

⋯ = ⋯

def OpenAddSubgroup.toOpens {G : Type u_1} [AddGroup G] [TopologicalSpace G] (U : OpenAddSubgroup G) :

TopologicalSpace.Opens G

Coercion from OpenAddSubgroup G to Opens G.

Equations

↑U = { carrier := ↑U, is_open' := ⋯ }

Instances For

def OpenSubgroup.toOpens {G : Type u_1} [Group G] [TopologicalSpace G] (U : OpenSubgroup G) :

TopologicalSpace.Opens G

Coercion from OpenSubgroup G to Opens G.

Equations

↑U = { carrier := ↑U, is_open' := ⋯ }

Instances For

instance OpenAddSubgroup.hasCoeOpens {G : Type u_1} [AddGroup G] [TopologicalSpace G] :

CoeTC (OpenAddSubgroup G) (TopologicalSpace.Opens G)

Equations

OpenAddSubgroup.hasCoeOpens = { coe := OpenAddSubgroup.toOpens }

instance OpenSubgroup.hasCoeOpens {G : Type u_1} [Group G] [TopologicalSpace G] :

CoeTC (OpenSubgroup G) (TopologicalSpace.Opens G)

Equations

OpenSubgroup.hasCoeOpens = { coe := OpenSubgroup.toOpens }

@[simp]

theorem OpenAddSubgroup.coe_toOpens {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} :

↑↑U = ↑U

@[simp]

theorem OpenSubgroup.coe_toOpens {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} :

↑↑U = ↑U

@[simp]

theorem OpenAddSubgroup.coe_toAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} :

↑↑U = ↑U

@[simp]

theorem OpenSubgroup.coe_toSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} :

↑↑U = ↑U

@[simp]

theorem OpenAddSubgroup.mem_toOpens {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {g : G} :

g ∈ ↑U ↔ g ∈ U

@[simp]

theorem OpenSubgroup.mem_toOpens {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {g : G} :

g ∈ ↑U ↔ g ∈ U

@[simp]

theorem OpenAddSubgroup.mem_toAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {g : G} :

g ∈ ↑U ↔ g ∈ U

@[simp]

theorem OpenSubgroup.mem_toSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {g : G} :

g ∈ ↑U ↔ g ∈ U

theorem OpenAddSubgroup.ext {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {V : OpenAddSubgroup G} (h : ∀ (x : G), x ∈ U ↔ x ∈ V) :

U = V

theorem OpenAddSubgroup.ext_iff {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {V : OpenAddSubgroup G} :

U = V ↔ ∀ (x : G), x ∈ U ↔ x ∈ V

theorem OpenSubgroup.ext_iff {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {V : OpenSubgroup G} :

U = V ↔ ∀ (x : G), x ∈ U ↔ x ∈ V

theorem OpenSubgroup.ext {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {V : OpenSubgroup G} (h : ∀ (x : G), x ∈ U ↔ x ∈ V) :

U = V

theorem OpenAddSubgroup.isOpen {G : Type u_1} [AddGroup G] [TopologicalSpace G] (U : OpenAddSubgroup G) :

theorem OpenSubgroup.isOpen {G : Type u_1} [Group G] [TopologicalSpace G] (U : OpenSubgroup G) :

theorem OpenAddSubgroup.mem_nhds_zero {G : Type u_1} [AddGroup G] [TopologicalSpace G] (U : OpenAddSubgroup G) :

↑U ∈ nhds 0

theorem OpenSubgroup.mem_nhds_one {G : Type u_1} [Group G] [TopologicalSpace G] (U : OpenSubgroup G) :

↑U ∈ nhds 1

instance OpenAddSubgroup.instTop {G : Type u_1} [AddGroup G] [TopologicalSpace G] :

Top (OpenAddSubgroup G)

Equations

OpenAddSubgroup.instTop = { top := { toAddSubgroup := ⊤, isOpen' := ⋯ } }

instance OpenSubgroup.instTop {G : Type u_1} [Group G] [TopologicalSpace G] :

Top (OpenSubgroup G)

Equations

OpenSubgroup.instTop = { top := { toSubgroup := ⊤, isOpen' := ⋯ } }

@[simp]

theorem OpenAddSubgroup.mem_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] (x : G) :

@[simp]

theorem OpenSubgroup.mem_top {G : Type u_1} [Group G] [TopologicalSpace G] (x : G) :

@[simp]

theorem OpenAddSubgroup.coe_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] :

↑⊤ = Set.univ

@[simp]

theorem OpenSubgroup.coe_top {G : Type u_1} [Group G] [TopologicalSpace G] :

↑⊤ = Set.univ

@[simp]

theorem OpenAddSubgroup.toAddSubgroup_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] :

@[simp]

theorem OpenSubgroup.toSubgroup_top {G : Type u_1} [Group G] [TopologicalSpace G] :

@[simp]

theorem OpenAddSubgroup.toOpens_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] :

@[simp]

theorem OpenSubgroup.toOpens_top {G : Type u_1} [Group G] [TopologicalSpace G] :

instance OpenAddSubgroup.instInhabited {G : Type u_1} [AddGroup G] [TopologicalSpace G] :

Inhabited (OpenAddSubgroup G)

Equations

OpenAddSubgroup.instInhabited = { default := ⊤ }

instance OpenSubgroup.instInhabited {G : Type u_1} [Group G] [TopologicalSpace G] :

Inhabited (OpenSubgroup G)

Equations

OpenSubgroup.instInhabited = { default := ⊤ }

theorem OpenAddSubgroup.isClosed {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (U : OpenAddSubgroup G) :

theorem OpenSubgroup.isClosed {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (U : OpenSubgroup G) :

theorem OpenAddSubgroup.isClopen {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (U : OpenAddSubgroup G) :

theorem OpenSubgroup.isClopen {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (U : OpenSubgroup G) :

def OpenAddSubgroup.sum {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] (U : OpenAddSubgroup G) (V : OpenAddSubgroup H) :

OpenAddSubgroup (G × H)

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

Equations

U.sum V = { toAddSubgroup := (↑U).prod ↑V, isOpen' := ⋯ }

Instances For

def OpenSubgroup.prod {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] (U : OpenSubgroup G) (V : OpenSubgroup H) :

OpenSubgroup (G × H)

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

Equations

U.prod V = { toSubgroup := (↑U).prod ↑V, isOpen' := ⋯ }

Instances For

@[simp]

theorem OpenAddSubgroup.coe_sum {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] (U : OpenAddSubgroup G) (V : OpenAddSubgroup H) :

↑(U.sum V) = ↑U ×ˢ ↑V

@[simp]

theorem OpenSubgroup.coe_prod {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] (U : OpenSubgroup G) (V : OpenSubgroup H) :

↑(U.prod V) = ↑U ×ˢ ↑V

@[simp]

theorem OpenAddSubgroup.toAddSubgroup_sum {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] (U : OpenAddSubgroup G) (V : OpenAddSubgroup H) :

↑(U.sum V) = (↑U).prod ↑V

@[simp]

theorem OpenSubgroup.toSubgroup_prod {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] (U : OpenSubgroup G) (V : OpenSubgroup H) :

↑(U.prod V) = (↑U).prod ↑V

instance OpenAddSubgroup.instInfOpenAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] :

Inf (OpenAddSubgroup G)

Equations

OpenAddSubgroup.instInfOpenAddSubgroup = { inf := fun (U V : OpenAddSubgroup G) => { toAddSubgroup := ↑U ⊓ ↑V, isOpen' := ⋯ } }

instance OpenSubgroup.instInfOpenSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] :

Inf (OpenSubgroup G)

Equations

OpenSubgroup.instInfOpenSubgroup = { inf := fun (U V : OpenSubgroup G) => { toSubgroup := ↑U ⊓ ↑V, isOpen' := ⋯ } }

@[simp]

theorem OpenAddSubgroup.coe_inf {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {V : OpenAddSubgroup G} :

↑(U ⊓ V) = ↑U ∩ ↑V

@[simp]

theorem OpenSubgroup.coe_inf {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {V : OpenSubgroup G} :

↑(U ⊓ V) = ↑U ∩ ↑V

@[simp]

theorem OpenAddSubgroup.toAddSubgroup_inf {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {V : OpenAddSubgroup G} :

↑(U ⊓ V) = ↑U ⊓ ↑V

@[simp]

theorem OpenSubgroup.toSubgroup_inf {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {V : OpenSubgroup G} :

↑(U ⊓ V) = ↑U ⊓ ↑V

@[simp]

theorem OpenAddSubgroup.toOpens_inf {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {V : OpenAddSubgroup G} :

↑(U ⊓ V) = ↑U ⊓ ↑V

@[simp]

theorem OpenSubgroup.toOpens_inf {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {V : OpenSubgroup G} :

↑(U ⊓ V) = ↑U ⊓ ↑V

@[simp]

theorem OpenAddSubgroup.mem_inf {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {V : OpenAddSubgroup G} {x : G} :

x ∈ U ⊓ V ↔ x ∈ U ∧ x ∈ V

@[simp]

theorem OpenSubgroup.mem_inf {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {V : OpenSubgroup G} {x : G} :

x ∈ U ⊓ V ↔ x ∈ U ∧ x ∈ V

instance OpenAddSubgroup.instPartialOrderOpenAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] :

PartialOrder (OpenAddSubgroup G)

Equations

OpenAddSubgroup.instPartialOrderOpenAddSubgroup = inferInstance

instance OpenSubgroup.instPartialOrderOpenSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] :

PartialOrder (OpenSubgroup G)

Equations

OpenSubgroup.instPartialOrderOpenSubgroup = inferInstance

instance OpenAddSubgroup.instSemilatticeInfOpenAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] :

SemilatticeInf (OpenAddSubgroup G)

Equations

OpenAddSubgroup.instSemilatticeInfOpenAddSubgroup = SemilatticeInf.mk ⋯ ⋯ ⋯

instance OpenSubgroup.instSemilatticeInfOpenSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] :

SemilatticeInf (OpenSubgroup G)

Equations

OpenSubgroup.instSemilatticeInfOpenSubgroup = SemilatticeInf.mk ⋯ ⋯ ⋯

instance OpenAddSubgroup.instOrderTop {G : Type u_1} [AddGroup G] [TopologicalSpace G] :

OrderTop (OpenAddSubgroup G)

Equations

OpenAddSubgroup.instOrderTop = OrderTop.mk ⋯

instance OpenSubgroup.instOrderTop {G : Type u_1} [Group G] [TopologicalSpace G] :

OrderTop (OpenSubgroup G)

Equations

OpenSubgroup.instOrderTop = OrderTop.mk ⋯

@[simp]

theorem OpenAddSubgroup.toAddSubgroup_le {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenAddSubgroup G} {V : OpenAddSubgroup G} :

↑U ≤ ↑V ↔ U ≤ V

@[simp]

theorem OpenSubgroup.toSubgroup_le {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenSubgroup G} {V : OpenSubgroup G} :

↑U ≤ ↑V ↔ U ≤ V

def OpenAddSubgroup.comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] (f : G →+ N) (hf : Continuous ⇑f) (H : OpenAddSubgroup N) :

OpenAddSubgroup G

The preimage of an OpenAddSubgroup along a continuous AddMonoid homomorphism is an OpenAddSubgroup.

Equations

OpenAddSubgroup.comap f hf H = { toAddSubgroup := AddSubgroup.comap f ↑H, isOpen' := ⋯ }

Instances For

def OpenSubgroup.comap {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] (f : G →* N) (hf : Continuous ⇑f) (H : OpenSubgroup N) :

The preimage of an OpenSubgroup along a continuous Monoid homomorphism is an OpenSubgroup.

Equations

OpenSubgroup.comap f hf H = { toSubgroup := Subgroup.comap f ↑H, isOpen' := ⋯ }

Instances For

@[simp]

theorem OpenAddSubgroup.coe_comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] (H : OpenAddSubgroup N) (f : G →+ N) (hf : Continuous ⇑f) :

↑(OpenAddSubgroup.comap f hf H) = ⇑f ⁻¹' ↑H

@[simp]

theorem OpenSubgroup.coe_comap {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] (H : OpenSubgroup N) (f : G →* N) (hf : Continuous ⇑f) :

↑(OpenSubgroup.comap f hf H) = ⇑f ⁻¹' ↑H

@[simp]

theorem OpenAddSubgroup.toAddSubgroup_comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] (H : OpenAddSubgroup N) (f : G →+ N) (hf : Continuous ⇑f) :

↑(OpenAddSubgroup.comap f hf H) = AddSubgroup.comap f ↑H

@[simp]

theorem OpenSubgroup.toSubgroup_comap {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] (H : OpenSubgroup N) (f : G →* N) (hf : Continuous ⇑f) :

↑(OpenSubgroup.comap f hf H) = Subgroup.comap f ↑H

@[simp]

theorem OpenAddSubgroup.mem_comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] {H : OpenAddSubgroup N} {f : G →+ N} {hf : Continuous ⇑f} {x : G} :

x ∈ OpenAddSubgroup.comap f hf H ↔ f x ∈ H

@[simp]

theorem OpenSubgroup.mem_comap {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] {H : OpenSubgroup N} {f : G →* N} {hf : Continuous ⇑f} {x : G} :

x ∈ OpenSubgroup.comap f hf H ↔ f x ∈ H

theorem OpenAddSubgroup.comap_comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] {P : Type u_3} [AddGroup P] [TopologicalSpace P] (K : OpenAddSubgroup P) (f₂ : N →+ P) (hf₂ : Continuous ⇑f₂) (f₁ : G →+ N) (hf₁ : Continuous ⇑f₁) :

OpenAddSubgroup.comap f₁ hf₁ (OpenAddSubgroup.comap f₂ hf₂ K) = OpenAddSubgroup.comap (f₂.comp f₁) ⋯ K

theorem OpenSubgroup.comap_comap {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] {P : Type u_3} [Group P] [TopologicalSpace P] (K : OpenSubgroup P) (f₂ : N →* P) (hf₂ : Continuous ⇑f₂) (f₁ : G →* N) (hf₁ : Continuous ⇑f₁) :

OpenSubgroup.comap f₁ hf₁ (OpenSubgroup.comap f₂ hf₂ K) = OpenSubgroup.comap (f₂.comp f₁) ⋯ K

theorem AddSubgroup.isOpen_of_mem_nhds {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (H : AddSubgroup G) {g : G} (hg : ↑H ∈ nhds g) :

theorem Subgroup.isOpen_of_mem_nhds {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (H : Subgroup G) {g : G} (hg : ↑H ∈ nhds g) :

theorem AddSubgroup.isOpen_mono {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] {H₁ : AddSubgroup G} {H₂ : AddSubgroup G} (h : H₁ ≤ H₂) (h₁ : IsOpen ↑H₁) :

IsOpen ↑H₂

theorem Subgroup.isOpen_mono {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] {H₁ : Subgroup G} {H₂ : Subgroup G} (h : H₁ ≤ H₂) (h₁ : IsOpen ↑H₁) :

IsOpen ↑H₂

theorem AddSubgroup.isOpen_of_openAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (H : AddSubgroup G) {U : OpenAddSubgroup G} (h : ↑U ≤ H) :

theorem Subgroup.isOpen_of_openSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (H : Subgroup G) {U : OpenSubgroup G} (h : ↑U ≤ H) :

theorem AddSubgroup.isOpen_of_zero_mem_interior {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (H : AddSubgroup 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.isOpen_of_one_mem_interior {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul 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.

theorem AddSubgroup.isClosed_of_isOpen {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (U : AddSubgroup G) (h : IsOpen ↑U) :

theorem Subgroup.isClosed_of_isOpen {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (U : Subgroup G) (h : IsOpen ↑U) :

theorem AddSubgroup.addSubgroupOf_isOpen {G : Type u_1} [AddGroup G] [TopologicalSpace G] (U : AddSubgroup G) (K : AddSubgroup G) (h : IsOpen ↑K) :

IsOpen ↑(K.addSubgroupOf U)

theorem Subgroup.subgroupOf_isOpen {G : Type u_1} [Group G] [TopologicalSpace G] (U : Subgroup G) (K : Subgroup G) (h : IsOpen ↑K) :

IsOpen ↑(K.subgroupOf U)

theorem AddSubgroup.discreteTopology {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (U : AddSubgroup G) (h : IsOpen ↑U) :

DiscreteTopology (G ⧸ U)

theorem Subgroup.discreteTopology {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (U : Subgroup G) (h : IsOpen ↑U) :

DiscreteTopology (G ⧸ U)

instance AddSubgroup.instDiscreteTopologyQuotientOfContinuousAdd {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (U : OpenAddSubgroup G) :

DiscreteTopology (G ⧸ ↑U)

Equations

⋯ = ⋯

instance Subgroup.instDiscreteTopologyQuotientOfContinuousMul {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (U : OpenSubgroup G) :

DiscreteTopology (G ⧸ ↑U)

Equations

⋯ = ⋯

theorem AddSubgroup.quotient_finite_of_isOpen {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] [CompactSpace G] (U : AddSubgroup G) (h : IsOpen ↑U) :

Finite (G ⧸ U)

theorem Subgroup.quotient_finite_of_isOpen {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] [CompactSpace G] (U : Subgroup G) (h : IsOpen ↑U) :

Finite (G ⧸ U)

instance AddSubgroup.instFiniteQuotientOfContinuousAddOfCompactSpace {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] [CompactSpace G] (U : OpenAddSubgroup G) :

Finite (G ⧸ ↑U)

Equations

⋯ = ⋯

instance Subgroup.instFiniteQuotientOfContinuousMulOfCompactSpace {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] [CompactSpace G] (U : OpenSubgroup G) :

Finite (G ⧸ ↑U)

Equations

⋯ = ⋯

theorem AddSubgroup.quotient_finite_of_isOpen' {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [CompactSpace G] (U : AddSubgroup G) (K : AddSubgroup ↥U) (hUopen : IsOpen ↑U) (hKopen : IsOpen ↑K) :

Finite (↥U ⧸ K)

theorem Subgroup.quotient_finite_of_isOpen' {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] (U : Subgroup G) (K : Subgroup ↥U) (hUopen : IsOpen ↑U) (hKopen : IsOpen ↑K) :

Finite (↥U ⧸ K)

instance AddSubgroup.instFiniteQuotientSubtypeMemOpenAddSubgroupOfTopologicalAddGroupOfCompactSpace {G : Type u_1} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [CompactSpace G] (U : OpenAddSubgroup G) (K : OpenAddSubgroup ↥U) :

Finite (↥U ⧸ ↑K)

Equations

⋯ = ⋯

instance Subgroup.instFiniteQuotientSubtypeMemOpenSubgroupOfTopologicalGroupOfCompactSpace {G : Type u_1} [Group G] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] (U : OpenSubgroup G) (K : OpenSubgroup ↥U) :

Finite (↥U ⧸ ↑K)

Equations

⋯ = ⋯

instance OpenAddSubgroup.instSup {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] :

Sup (OpenAddSubgroup G)

Equations

OpenAddSubgroup.instSup = { sup := fun (U V : OpenAddSubgroup G) => { toAddSubgroup := ↑U ⊔ ↑V, isOpen' := ⋯ } }

instance OpenSubgroup.instSup {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] :

Sup (OpenSubgroup G)

Equations

OpenSubgroup.instSup = { sup := fun (U V : OpenSubgroup G) => { toSubgroup := ↑U ⊔ ↑V, isOpen' := ⋯ } }

@[simp]

theorem OpenAddSubgroup.toAddSubgroup_sup {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] (U : OpenAddSubgroup G) (V : OpenAddSubgroup G) :

↑(U ⊔ V) = ↑U ⊔ ↑V

@[simp]

theorem OpenSubgroup.toSubgroup_sup {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] (U : OpenSubgroup G) (V : OpenSubgroup G) :

↑(U ⊔ V) = ↑U ⊔ ↑V

instance OpenAddSubgroup.instLattice {G : Type u_1} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] :

Lattice (OpenAddSubgroup G)

Equations

OpenAddSubgroup.instLattice = Lattice.mk ⋯ ⋯ ⋯

instance OpenSubgroup.instLattice {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousMul G] :

Lattice (OpenSubgroup G)

Equations

OpenSubgroup.instLattice = Lattice.mk ⋯ ⋯ ⋯

theorem Submodule.isOpen_mono {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [TopologicalSpace M] [TopologicalAddGroup M] [Module R M] {U : Submodule R M} {P : Submodule R M} (h : U ≤ P) (hU : IsOpen ↑U) :

theorem Ideal.isOpen_of_isOpen_subideal {R : Type u_1} [CommRing R] [TopologicalSpace R] [TopologicalRing R] {U : Ideal R} {I : Ideal R} (h : U ≤ I) (hU : IsOpen ↑U) :

Open normal subgroups of a topological group #

This section builds the lattice OpenNormalSubgroup G of open subgroups in a topological group G, and its additive version OpenNormalAddSubgroup.

theorem OpenNormalSubgroup.ext_iff {G : Type u} :

∀ {inst : Group G} {inst_1 : TopologicalSpace G} {x y : OpenNormalSubgroup G}, x = y ↔ (↑x.toOpenSubgroup).carrier = (↑y.toOpenSubgroup).carrier

theorem OpenNormalSubgroup.ext {G : Type u} :

∀ {inst : Group G} {inst_1 : TopologicalSpace G} {x y : OpenNormalSubgroup G}, (↑x.toOpenSubgroup).carrier = (↑y.toOpenSubgroup).carrier → x = y

structure OpenNormalSubgroup (G : Type u) [Group G] [TopologicalSpace G] extends OpenSubgroup :

The type of open normal subgroups of a topological group.

carrier : Set G
mul_mem' : ∀ {a b : G}, a ∈ (↑self.toOpenSubgroup).carrier → b ∈ (↑self.toOpenSubgroup).carrier → a * b ∈ (↑self.toOpenSubgroup).carrier
one_mem' : 1 ∈ (↑self.toOpenSubgroup).carrier
inv_mem' : ∀ {x : G}, x ∈ (↑self.toOpenSubgroup).carrier → x⁻¹ ∈ (↑self.toOpenSubgroup).carrier
isOpen' : IsOpen (↑self.toOpenSubgroup).carrier
isNormal' : (↑self.toOpenSubgroup).Normal

Instances For

theorem OpenNormalSubgroup.isNormal' {G : Type u} [Group G] [TopologicalSpace G] (self : OpenNormalSubgroup G) :

(↑self.toOpenSubgroup).Normal

theorem OpenNormalAddSubgroup.ext {G : Type u} :

∀ {inst : AddGroup G} {inst_1 : TopologicalSpace G} {x y : OpenNormalAddSubgroup G}, (↑x.toOpenAddSubgroup).carrier = (↑y.toOpenAddSubgroup).carrier → x = y

theorem OpenNormalAddSubgroup.ext_iff {G : Type u} :

∀ {inst : AddGroup G} {inst_1 : TopologicalSpace G} {x y : OpenNormalAddSubgroup G}, x = y ↔ (↑x.toOpenAddSubgroup).carrier = (↑y.toOpenAddSubgroup).carrier

structure OpenNormalAddSubgroup (G : Type u) [AddGroup G] [TopologicalSpace G] extends OpenAddSubgroup :

The type of open normal subgroups of a topological additive group.

carrier : Set G
add_mem' : ∀ {a b : G}, a ∈ (↑self.toOpenAddSubgroup).carrier → b ∈ (↑self.toOpenAddSubgroup).carrier → a + b ∈ (↑self.toOpenAddSubgroup).carrier
zero_mem' : 0 ∈ (↑self.toOpenAddSubgroup).carrier
neg_mem' : ∀ {x : G}, x ∈ (↑self.toOpenAddSubgroup).carrier → -x ∈ (↑self.toOpenAddSubgroup).carrier
isOpen' : IsOpen (↑self.toOpenAddSubgroup).carrier
isNormal' : (↑self.toOpenAddSubgroup).Normal

Instances For

theorem OpenNormalAddSubgroup.isNormal' {G : Type u} [AddGroup G] [TopologicalSpace G] (self : OpenNormalAddSubgroup G) :

(↑self.toOpenAddSubgroup).Normal

instance OpenNormalAddSubgroup.instNormal {G : Type u} [AddGroup G] [TopologicalSpace G] (H : OpenNormalAddSubgroup G) :

(↑H.toOpenAddSubgroup).Normal

Equations

⋯ = ⋯

instance OpenNormalSubgroup.instNormal {G : Type u} [Group G] [TopologicalSpace G] (H : OpenNormalSubgroup G) :

(↑H.toOpenSubgroup).Normal

Equations

⋯ = ⋯

theorem OpenNormalAddSubgroup.toAddSubgroup_injective {G : Type u} [AddGroup G] [TopologicalSpace G] :

Function.Injective fun (H : OpenNormalAddSubgroup G) => ↑H.toOpenAddSubgroup

theorem OpenNormalSubgroup.toSubgroup_injective {G : Type u} [Group G] [TopologicalSpace G] :

Function.Injective fun (H : OpenNormalSubgroup G) => ↑H.toOpenSubgroup

instance OpenNormalAddSubgroup.instSetLike {G : Type u} [AddGroup G] [TopologicalSpace G] :

SetLike (OpenNormalAddSubgroup G) G

Equations

OpenNormalAddSubgroup.instSetLike = { coe := fun (U : OpenNormalAddSubgroup G) => ↑U.toOpenAddSubgroup, coe_injective' := ⋯ }

instance OpenNormalSubgroup.instSetLike {G : Type u} [Group G] [TopologicalSpace G] :

SetLike (OpenNormalSubgroup G) G

Equations

OpenNormalSubgroup.instSetLike = { coe := fun (U : OpenNormalSubgroup G) => ↑U.toOpenSubgroup, coe_injective' := ⋯ }

instance OpenNormalAddSubgroup.instAddSubgroupClass {G : Type u} [AddGroup G] [TopologicalSpace G] :

AddSubgroupClass (OpenNormalAddSubgroup G) G

Equations

⋯ = ⋯

instance OpenNormalSubgroup.instSubgroupClass {G : Type u} [Group G] [TopologicalSpace G] :

SubgroupClass (OpenNormalSubgroup G) G

Equations

⋯ = ⋯

instance OpenNormalAddSubgroup.instCoeAddSubgroup {G : Type u} [AddGroup G] [TopologicalSpace G] :

Coe (OpenNormalAddSubgroup G) (AddSubgroup G)

Equations

OpenNormalAddSubgroup.instCoeAddSubgroup = { coe := fun (H : OpenNormalAddSubgroup G) => ↑H.toOpenAddSubgroup }

instance OpenNormalSubgroup.instCoeSubgroup {G : Type u} [Group G] [TopologicalSpace G] :

Coe (OpenNormalSubgroup G) (Subgroup G)

Equations

OpenNormalSubgroup.instCoeSubgroup = { coe := fun (H : OpenNormalSubgroup G) => ↑H.toOpenSubgroup }

instance OpenNormalAddSubgroup.instPartialOrderOpenNormalAddSubgroup {G : Type u} [AddGroup G] [TopologicalSpace G] :

PartialOrder (OpenNormalAddSubgroup G)

Equations

OpenNormalAddSubgroup.instPartialOrderOpenNormalAddSubgroup = inferInstance

instance OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup {G : Type u} [Group G] [TopologicalSpace G] :

PartialOrder (OpenNormalSubgroup G)

Equations

OpenNormalSubgroup.instPartialOrderOpenNormalSubgroup = inferInstance

instance OpenNormalAddSubgroup.instInfOpenNormalAddSubgroup {G : Type u} [AddGroup G] [TopologicalSpace G] :

Inf (OpenNormalAddSubgroup G)

Equations

OpenNormalAddSubgroup.instInfOpenNormalAddSubgroup = { inf := fun (U V : OpenNormalAddSubgroup G) => { toOpenAddSubgroup := U.toOpenAddSubgroup ⊓ V.toOpenAddSubgroup, isNormal' := ⋯ } }

instance OpenNormalSubgroup.instInfOpenNormalSubgroup {G : Type u} [Group G] [TopologicalSpace G] :

Inf (OpenNormalSubgroup G)

Equations

OpenNormalSubgroup.instInfOpenNormalSubgroup = { inf := fun (U V : OpenNormalSubgroup G) => { toOpenSubgroup := U.toOpenSubgroup ⊓ V.toOpenSubgroup, isNormal' := ⋯ } }

instance OpenNormalAddSubgroup.instSemilatticeInfOpenNormalAddSubgroup {G : Type u} [AddGroup G] [TopologicalSpace G] :

SemilatticeInf (OpenNormalAddSubgroup G)

Equations

OpenNormalAddSubgroup.instSemilatticeInfOpenNormalAddSubgroup = Function.Injective.semilatticeInf SetLike.coe ⋯ ⋯

instance OpenNormalSubgroup.instSemilatticeInfOpenNormalSubgroup {G : Type u} [Group G] [TopologicalSpace G] :

SemilatticeInf (OpenNormalSubgroup G)

Equations

OpenNormalSubgroup.instSemilatticeInfOpenNormalSubgroup = Function.Injective.semilatticeInf SetLike.coe ⋯ ⋯

instance OpenNormalAddSubgroup.instSupOfContinuousAdd {G : Type u} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] :

Sup (OpenNormalAddSubgroup G)

Equations

OpenNormalAddSubgroup.instSupOfContinuousAdd = { sup := fun (U V : OpenNormalAddSubgroup G) => { toOpenAddSubgroup := U.toOpenAddSubgroup ⊔ V.toOpenAddSubgroup, isNormal' := ⋯ } }

instance OpenNormalSubgroup.instSupOfContinuousMul {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] :

Sup (OpenNormalSubgroup G)

Equations

OpenNormalSubgroup.instSupOfContinuousMul = { sup := fun (U V : OpenNormalSubgroup G) => { toOpenSubgroup := U.toOpenSubgroup ⊔ V.toOpenSubgroup, isNormal' := ⋯ } }

instance OpenNormalAddSubgroup.instSemilatticeSupOpenNormalAddSubgroup {G : Type u} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] :

SemilatticeSup (OpenNormalAddSubgroup G)

Equations

OpenNormalAddSubgroup.instSemilatticeSupOpenNormalAddSubgroup = Function.Injective.semilatticeSup (fun (H : OpenNormalAddSubgroup G) => ↑H.toOpenAddSubgroup) ⋯ ⋯

instance OpenNormalSubgroup.instSemilatticeSupOpenNormalSubgroup {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] :

SemilatticeSup (OpenNormalSubgroup G)

Equations

OpenNormalSubgroup.instSemilatticeSupOpenNormalSubgroup = Function.Injective.semilatticeSup (fun (H : OpenNormalSubgroup G) => ↑H.toOpenSubgroup) ⋯ ⋯

instance OpenNormalAddSubgroup.instLatticeOfContinuousAdd {G : Type u} [AddGroup G] [TopologicalSpace G] [ContinuousAdd G] :

Lattice (OpenNormalAddSubgroup G)

Equations

OpenNormalAddSubgroup.instLatticeOfContinuousAdd = Lattice.mk ⋯ ⋯ ⋯

instance OpenNormalSubgroup.instLatticeOfContinuousMul {G : Type u} [Group G] [TopologicalSpace G] [ContinuousMul G] :

Lattice (OpenNormalSubgroup G)

Equations

OpenNormalSubgroup.instLatticeOfContinuousMul = Lattice.mk ⋯ ⋯ ⋯

Existence of an open subgroup in any clopen neighborhood of the neutral element #

This section proves the lemma TopologicalGroup.exist_openSubgroup_sub_clopen_nhd_of_one, which states that in a compact topological group, for any clopen neighborhood of 1, there exists an open subgroup contained within it.

structure TopologicalAddGroup.addNegClosureNhd {G : Type u_1} [TopologicalSpace G] (T : Set G) (W : Set G) [AddGroup G] :

For a set W, T is a neighborhood of 0 which is open, stable under negation and satisfies T + W ⊆ W.

nhd : T ∈ nhds 0
neg : -T = T
isOpen : IsOpen T
add : W + T ⊆ W

Instances For

theorem TopologicalAddGroup.addNegClosureNhd.nhd {G : Type u_1} [TopologicalSpace G] {T : Set G} {W : Set G} [AddGroup G] (self : TopologicalAddGroup.addNegClosureNhd T W) :

theorem TopologicalAddGroup.addNegClosureNhd.neg {G : Type u_1} [TopologicalSpace G] {T : Set G} {W : Set G} [AddGroup G] (self : TopologicalAddGroup.addNegClosureNhd T W) :

-T = T

theorem TopologicalAddGroup.addNegClosureNhd.isOpen {G : Type u_1} [TopologicalSpace G] {T : Set G} {W : Set G} [AddGroup G] (self : TopologicalAddGroup.addNegClosureNhd T W) :

theorem TopologicalAddGroup.addNegClosureNhd.add {G : Type u_1} [TopologicalSpace G] {T : Set G} {W : Set G} [AddGroup G] (self : TopologicalAddGroup.addNegClosureNhd T W) :

W + T ⊆ W

structure TopologicalGroup.mulInvClosureNhd {G : Type u_1} [TopologicalSpace G] (T : Set G) (W : Set G) [Group G] :

For a set W, T is a neighborhood of 1 which is open, statble under inverse and satisfies T * W ⊆ W.

nhd : T ∈ nhds 1
inv : T⁻¹ = T
isOpen : IsOpen T
mul : W * T ⊆ W

Instances For

theorem TopologicalGroup.mulInvClosureNhd.nhd {G : Type u_1} [TopologicalSpace G] {T : Set G} {W : Set G} [Group G] (self : TopologicalGroup.mulInvClosureNhd T W) :

theorem TopologicalGroup.mulInvClosureNhd.inv {G : Type u_1} [TopologicalSpace G] {T : Set G} {W : Set G} [Group G] (self : TopologicalGroup.mulInvClosureNhd T W) :

theorem TopologicalGroup.mulInvClosureNhd.isOpen {G : Type u_1} [TopologicalSpace G] {T : Set G} {W : Set G} [Group G] (self : TopologicalGroup.mulInvClosureNhd T W) :

theorem TopologicalGroup.mulInvClosureNhd.mul {G : Type u_1} [TopologicalSpace G] {T : Set G} {W : Set G} [Group G] (self : TopologicalGroup.mulInvClosureNhd T W) :

W * T ⊆ W

theorem TopologicalAddGroup.exist_add_closure_nhd {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [CompactSpace G] {W : Set G} (WClopen : IsClopen W) :

∃ T ∈ nhds 0, W + T ⊆ W

theorem TopologicalGroup.exist_mul_closure_nhd {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [CompactSpace G] {W : Set G} (WClopen : IsClopen W) :

∃ T ∈ nhds 1, W * T ⊆ W

theorem TopologicalAddGroup.exists_addNegClosureNhd {G : Type u_1} [TopologicalSpace G] [AddGroup G] [TopologicalAddGroup G] [CompactSpace G] {W : Set G} (WClopen : IsClopen W) :

∃ (T : Set G), TopologicalAddGroup.addNegClosureNhd T W

theorem TopologicalGroup.exists_mulInvClosureNhd {G : Type u_1} [TopologicalSpace G] [Group G] [TopologicalGroup G] [CompactSpace G] {W : Set G} (WClopen : IsClopen W) :

∃ (T : Set G), TopologicalGroup.mulInvClosureNhd T W

theorem TopologicalAddGroup.exist_openAddSubgroup_sub_clopen_nhd_of_zero {G : Type u_2} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [CompactSpace G] {W : Set G} (WClopen : IsClopen W) (einW : 0 ∈ W) :

∃ (H : OpenAddSubgroup G), ↑H ⊆ W

theorem TopologicalGroup.exist_openSubgroup_sub_clopen_nhd_of_one {G : Type u_2} [Group G] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] {W : Set G} (WClopen : IsClopen W) (einW : 1 ∈ W) :

∃ (H : OpenSubgroup G), ↑H ⊆ W