Constructions of open normal subgroups

Bundled constructions of OpenNormalSubgroup that Mathlib provides for OpenSubgroup but not for its normal variant: the preimage under a continuous group homomorphism, the product of two open normal subgroups, the trivial subgroup of a group with the discrete topology, and the whole group. All are stated for an arbitrary topological space structure on a group; no continuity of the group operations is required.

Two continuity criteria for maps into the discrete quotients by open normal subgroups are recorded as well: a map into the quotient by an intersection is continuous when its composites with the two quotient maps are, and a map into the quotient by a preimage is continuous when its composite with the homomorphism followed by the quotient map is. Separate continuity of multiplication makes the relevant quotients discrete; the preimage criterion needs it only on the target group.

Main definitions

• OpenNormalSubgroup.comap: the preimage of an open normal subgroup under a continuous group homomorphism.
• OpenNormalSubgroup.prod: the product of two open normal subgroups, as an open normal subgroup of the product group.
• TauCeti.openNormalSubgroupBot: the trivial subgroup of a group with the discrete topology, as an open normal subgroup.
• TauCeti.openNormalSubgroupTop: the whole group, as an open normal subgroup.

Main results

• OpenNormalSubgroup.toSubgroup_inf, OpenNormalSubgroup.toSubgroup_sup: the lattice operations on open normal subgroups are those of the underlying subgroups.
• OpenNormalSubgroup.continuous_mk_inf, OpenNormalSubgroup.continuous_mk_comap: continuity of a map into the quotient by an intersection, and by a preimage, of open normal subgroups.
• TauCeti.mem_openNormalSubgroupBot: the trivial open normal subgroup contains only the identity.
• TauCeti.openNormalSubgroupBot_le: the trivial open normal subgroup lies below every open normal subgroup.

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

Open normal subgroups compare through their underlying subgroups.

@[simp]

theorem OpenNormalSubgroup.toSubgroup_inf {G : Type u_1} [Group G] [TopologicalSpace G] (U V : OpenNormalSubgroup G) : ↑(U ⊓ V).toOpenSubgroup = ↑U.toOpenSubgroup ⊓ ↑V.toOpenSubgroup

The underlying subgroup of the intersection of two open normal subgroups is the intersection of the underlying subgroups.

@[simp]

theorem OpenNormalSubgroup.toSubgroup_sup {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (U V : OpenNormalSubgroup G) : ↑(U ⊔ V).toOpenSubgroup = ↑U.toOpenSubgroup ⊔ ↑V.toOpenSubgroup

The underlying subgroup of the join of two open normal subgroups is the join of the underlying subgroups.

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

The preimage of an open normal subgroup under a continuous group homomorphism.

Equations

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

@[simp]

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

The preimage of an open normal subgroup as a set.

@[simp]

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

The underlying subgroup of the preimage of an open normal subgroup.

@[simp]

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

Membership in the preimage of an open normal subgroup.

theorem OpenNormalSubgroup.comap_comap {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] {K : Type u_3} [Group K] [TopologicalSpace K] (U : OpenNormalSubgroup K) (f₂ : H →* K) (hf₂ : Continuous ⇑f₂) (f₁ : G →* H) (hf₁ : Continuous ⇑f₁) : (U.comap f₂ hf₂).comap f₁ hf₁ = U.comap (f₂.comp f₁) ⋯

Taking the preimage of an open normal subgroup twice is the preimage under the composite.

def OpenNormalSubgroup.prod {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [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' := ⋯ }

@[simp]

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

The product of two open normal subgroups as a set.

@[simp]

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

The underlying subgroup of the product of two open normal subgroups.

@[simp]

theorem OpenNormalSubgroup.mem_prod {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] {U : OpenNormalSubgroup G} {V : OpenNormalSubgroup H} {x : G × H} : x ∈ U.prod V ↔ x.1 ∈ U ∧ x.2 ∈ V

Membership in the product of two open normal subgroups.

theorem OpenNormalSubgroup.continuous_mk_inf {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {X : Type u_3} [TopologicalSpace X] {U V : OpenNormalSubgroup G} {g : X → G} (hU : Continuous fun (x : X) => ↑(g x)) (hV : Continuous fun (x : X) => ↑(g x)) : Continuous fun (x : X) => ↑(g x)

A map into the quotient by the intersection of two open normal subgroups is continuous as soon as its composites with the two quotient maps are.

theorem OpenNormalSubgroup.continuous_mk_comap {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] [SeparatelyContinuousMul H] {X : Type u_3} [TopologicalSpace X] (U : OpenNormalSubgroup H) (f : G →* H) (hf : Continuous ⇑f) {g : X → G} (hg : Continuous fun (x : X) => ↑(f (g x))) : Continuous fun (x : X) => ↑(g x)

A map into the quotient by the preimage of an open normal subgroup under a continuous homomorphism is continuous as soon as its composite with the homomorphism followed by the quotient map is. No continuity of the group operations on the source group is required.

def TauCeti.openNormalSubgroupBot (G : Type u_1) [Group G] [TopologicalSpace G] [DiscreteTopology G] : OpenNormalSubgroup G

The trivial subgroup of a group with the discrete topology, as an open normal subgroup.

Equations

• TauCeti.openNormalSubgroupBot G = { toSubgroup := ⊥, isOpen' := ⋯, isNormal' := ⋯ }

@[simp]

theorem TauCeti.openNormalSubgroupBot_toSubgroup (G : Type u_1) [Group G] [TopologicalSpace G] [DiscreteTopology G] : ↑(openNormalSubgroupBot G).toOpenSubgroup = ⊥

The underlying subgroup of openNormalSubgroupBot is ⊥.

@[simp]

theorem TauCeti.mem_openNormalSubgroupBot {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] {x : G} : x ∈ openNormalSubgroupBot G ↔ x = 1

The trivial open normal subgroup contains only the identity.

theorem TauCeti.openNormalSubgroupBot_le {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] {U : OpenNormalSubgroup G} : openNormalSubgroupBot G ≤ U

The trivial open normal subgroup of a discrete group lies below every open normal subgroup.

def TauCeti.openNormalSubgroupTop (G : Type u_1) [Group G] [TopologicalSpace G] : OpenNormalSubgroup G

The whole group, as an open normal subgroup. It is the greatest element of OpenNormalSubgroup G, and in particular witnesses that this type is nonempty.

Equations

• TauCeti.openNormalSubgroupTop G = { toOpenSubgroup := ⊤, isNormal' := ⋯ }

@[simp]

theorem TauCeti.openNormalSubgroupTop_toSubgroup (G : Type u_1) [Group G] [TopologicalSpace G] : ↑(openNormalSubgroupTop G).toOpenSubgroup = ⊤

The underlying subgroup of openNormalSubgroupTop is ⊤.