Supplementary results for open normal subgroups

@[simp]

theorem OpenNormalSubgroup.coe_toOpenSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenNormalSubgroup G} : ↑U.toOpenSubgroup = ↑U

@[simp]

theorem OpenNormalAddSubgroup.coe_toOpenAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenNormalAddSubgroup G} : ↑U.toOpenAddSubgroup = ↑U

theorem OpenNormalSubgroup.coe_toSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenNormalSubgroup G} : ↑↑U.toOpenSubgroup = ↑U

theorem OpenNormalAddSubgroup.coe_toAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenNormalAddSubgroup G} : ↑↑U.toOpenAddSubgroup = ↑U

@[simp]

theorem OpenNormalSubgroup.mem_toOpenSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenNormalSubgroup G} {g : G} : g ∈ U.toOpenSubgroup ↔ g ∈ U

@[simp]

theorem OpenNormalAddSubgroup.mem_toOpenAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenNormalAddSubgroup G} {g : G} : g ∈ U.toOpenAddSubgroup ↔ g ∈ U

theorem OpenNormalSubgroup.mem_toSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] {U : OpenNormalSubgroup G} {g : G} : g ∈ ↑U.toOpenSubgroup ↔ g ∈ U

theorem OpenNormalAddSubgroup.mem_toAddSubgroup {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U : OpenNormalAddSubgroup G} {g : G} : g ∈ ↑U.toOpenAddSubgroup ↔ g ∈ U

instance OpenNormalSubgroup.instTop {G : Type u_1} [Group G] [TopologicalSpace G] : Top (OpenNormalSubgroup G)

Equations

• OpenNormalSubgroup.instTop = { top := { toOpenSubgroup := ⊤, isNormal' := ⋯ } }

instance OpenNormalAddSubgroup.instTop {G : Type u_1} [AddGroup G] [TopologicalSpace G] : Top (OpenNormalAddSubgroup G)

Equations

• OpenNormalAddSubgroup.instTop = { top := { toOpenAddSubgroup := ⊤, isNormal' := ⋯ } }

@[simp]

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

@[simp]

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

@[simp]

theorem OpenNormalSubgroup.coe_top {G : Type u_1} [Group G] [TopologicalSpace G] : ↑⊤ = Set.univ

@[simp]

theorem OpenNormalAddSubgroup.coe_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] : ↑⊤ = Set.univ

@[simp]

theorem OpenNormalSubgroup.toOpenSubgroup_top {G : Type u_1} [Group G] [TopologicalSpace G] : ⊤.toOpenSubgroup = ⊤

@[simp]

theorem OpenNormalAddSubgroup.toOpenAddSubgroup_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] : ⊤.toOpenAddSubgroup = ⊤

theorem OpenNormalSubgroup.toSubgroup_top {G : Type u_1} [Group G] [TopologicalSpace G] : ↑⊤.toOpenSubgroup = ⊤

theorem OpenNormalAddSubgroup.toAddSubgroup_top {G : Type u_1} [AddGroup G] [TopologicalSpace G] : ↑⊤.toOpenAddSubgroup = ⊤

instance OpenNormalSubgroup.instInhabited {G : Type u_1} [Group G] [TopologicalSpace G] : Inhabited (OpenNormalSubgroup G)

Equations

• OpenNormalSubgroup.instInhabited = { default := ⊤ }

instance OpenNormalAddSubgroup.instInhabited {G : Type u_1} [AddGroup G] [TopologicalSpace G] : Inhabited (OpenNormalAddSubgroup G)

Equations

• OpenNormalAddSubgroup.instInhabited = { default := ⊤ }

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

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

Equations

• U.prod V = { toOpenSubgroup := U.prod V.toOpenSubgroup, isNormal' := ⋯ }

def OpenNormalAddSubgroup.prod {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] (U : OpenNormalAddSubgroup G) (V : OpenNormalAddSubgroup H) : OpenNormalAddSubgroup (G × H)

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

Equations

• U.prod V = { toOpenAddSubgroup := U.prod V.toOpenAddSubgroup, isNormal' := ⋯ }

@[simp]

theorem OpenNormalSubgroup.coe_prod {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] (U : OpenNormalSubgroup G) (V : OpenNormalSubgroup H) : ↑(U.prod V) = ↑U ×ˢ ↑V

@[simp]

theorem OpenNormalAddSubgroup.coe_prod {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] (U : OpenNormalAddSubgroup G) (V : OpenNormalAddSubgroup H) : ↑(U.prod V) = ↑U ×ˢ ↑V

@[simp]

theorem OpenNormalSubgroup.toOpenSubgroup_prod {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] (U : OpenNormalSubgroup G) (V : OpenNormalSubgroup H) : (U.prod V).toOpenSubgroup = U.prod V.toOpenSubgroup

@[simp]

theorem OpenNormalAddSubgroup.toOpenAddSubgroup_prod {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] (U : OpenNormalAddSubgroup G) (V : OpenNormalAddSubgroup H) : (U.prod V).toOpenAddSubgroup = U.prod V.toOpenAddSubgroup

theorem OpenNormalSubgroup.toSubgroup_prod {G : Type u_1} [Group G] [TopologicalSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] (U : OpenNormalSubgroup G) (V : OpenNormalSubgroup H) : ↑(U.prod V).toOpenSubgroup = (↑U.toOpenSubgroup).prod ↑V.toOpenSubgroup

theorem OpenNormalAddSubgroup.toAddSubgroup_prod {G : Type u_1} [AddGroup G] [TopologicalSpace G] {H : Type u_2} [AddGroup H] [TopologicalSpace H] (U : OpenNormalAddSubgroup G) (V : OpenNormalAddSubgroup H) : ↑(U.prod V).toOpenAddSubgroup = (↑U.toOpenAddSubgroup).prod ↑V.toOpenAddSubgroup

instance OpenNormalSubgroup.instOrderTop {G : Type u_1} [Group G] [TopologicalSpace G] : OrderTop (OpenNormalSubgroup G)

Equations

• OpenNormalSubgroup.instOrderTop = { toTop := OpenNormalSubgroup.instTop, le_top := ⋯ }

instance OpenNormalAddSubgroup.instOrderTop {G : Type u_1} [AddGroup G] [TopologicalSpace G] : OrderTop (OpenNormalAddSubgroup G)

Equations

• OpenNormalAddSubgroup.instOrderTop = { toTop := OpenNormalAddSubgroup.instTop, le_top := ⋯ }

@[simp]

theorem OpenNormalSubgroup.toOpenSubgroup_le {G : Type u_1} [Group G] [TopologicalSpace G] {U V : OpenNormalSubgroup G} : U.toOpenSubgroup ≤ V.toOpenSubgroup ↔ U ≤ V

@[simp]

theorem OpenNormalAddSubgroup.toOpenAddSubgroup_le {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U V : OpenNormalAddSubgroup G} : U.toOpenAddSubgroup ≤ V.toOpenAddSubgroup ↔ U ≤ V

theorem OpenNormalSubgroup.toSubgroup_le {G : Type u_1} [Group G] [TopologicalSpace G] {U V : OpenNormalSubgroup G} : ↑U.toOpenSubgroup ≤ ↑V.toOpenSubgroup ↔ U ≤ V

theorem OpenNormalAddSubgroup.toAddSubgroup_le {G : Type u_1} [AddGroup G] [TopologicalSpace G] {U V : OpenNormalAddSubgroup G} : ↑U.toOpenAddSubgroup ≤ ↑V.toOpenAddSubgroup ↔ U ≤ V

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

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

Equations

• OpenNormalSubgroup.comap f hf H = { toOpenSubgroup := OpenSubgroup.comap f hf H.toOpenSubgroup, isNormal' := ⋯ }

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

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

Equations

• OpenNormalAddSubgroup.comap f hf H = { toOpenAddSubgroup := OpenAddSubgroup.comap f hf H.toOpenAddSubgroup, isNormal' := ⋯ }

@[simp]

theorem OpenNormalSubgroup.coe_comap {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] (H : OpenNormalSubgroup N) (f : G →* N) (hf : Continuous ⇑f) : ↑(comap f hf H) = ⇑f ⁻¹' ↑H

@[simp]

theorem OpenNormalAddSubgroup.coe_comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] (H : OpenNormalAddSubgroup N) (f : G →+ N) (hf : Continuous ⇑f) : ↑(comap f hf H) = ⇑f ⁻¹' ↑H

@[simp]

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

@[simp]

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

theorem OpenNormalSubgroup.toSubgroup_comap {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] (H : OpenNormalSubgroup N) (f : G →* N) (hf : Continuous ⇑f) : ↑(comap f hf H).toOpenSubgroup = Subgroup.comap f ↑H.toOpenSubgroup

theorem OpenNormalAddSubgroup.toAddSubgroup_comap {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] (H : OpenNormalAddSubgroup N) (f : G →+ N) (hf : Continuous ⇑f) : ↑(comap f hf H).toOpenAddSubgroup = AddSubgroup.comap f ↑H.toOpenAddSubgroup

@[simp]

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

@[simp]

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

theorem OpenNormalSubgroup.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 : OpenNormalSubgroup P) (f₂ : N →* P) (hf₂ : Continuous ⇑f₂) (f₁ : G →* N) (hf₁ : Continuous ⇑f₁) : comap f₁ hf₁ (comap f₂ hf₂ K) = comap (f₂.comp f₁) ⋯ K

theorem OpenNormalAddSubgroup.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 : OpenNormalAddSubgroup P) (f₂ : N →+ P) (hf₂ : Continuous ⇑f₂) (f₁ : G →+ N) (hf₁ : Continuous ⇑f₁) : comap f₁ hf₁ (comap f₂ hf₂ K) = comap (f₂.comp f₁) ⋯ K