Quotients of topological groups by subgroups

Generic facts about quotients by subgroups of topological groups. Most results use [IsTopologicalGroup G]; forward translation of a fixed coset needs only [SeparatelyContinuousMul G]. The inverse-translation results additionally require [DiscreteTopology (G ⧸ U)]. Neither compactness nor total disconnectedness is needed.

Main definitions

• TauCeti.quotientOpenSubgroup: the image of an open subgroup of G in G ⧸ N, as an open subgroup.
• TauCeti.quotientOpenSubgroupMap: the quotient homomorphism restricted to an open subgroup.
• TauCeti.quotientSubgroupOfEquivMap: for an open normal subgroup V, the quotient W ⧸ V.subgroupOf W is isomorphic, as a topological group, to the image of W in G ⧸ V.
• TauCeti.quotientQuotientContinuousMulEquiv: for an open normal subgroup V contained in a normal subgroup W, the third isomorphism theorem (G ⧸ V) ⧸ W.map (mk' V) ≃ₜ* G ⧸ W.

Main results

• Subgroup.continuous_smul_const: translation of a fixed coset is continuous.
• Subgroup.continuous_inv_smul_const: inverse translation of a fixed coset is continuous when the quotient is discrete.
• Subgroup.continuous_inv_smul: inverse translation is jointly continuous when the quotient is discrete.
• QuotientGroup.instDiscreteTopology: the quotient of a discrete group by any subgroup is discrete.
• QuotientGroup.continuous_mapOfLE: the quotient homomorphism G ⧸ V →* G ⧸ U for normal subgroups V ≤ U is continuous.
• QuotientGroup.isClopen_image_mk: the image of an open subgroup of G under the quotient map G → G ⧸ N is clopen.
• QuotientGroup.comapMk'OpenNormalOrderIso: open normal subgroups of G ⧸ N correspond, as lattices, to the open normal subgroups of G containing N.
• TauCeti.quotientOpenSubgroup_index: quotienting by a subgroup of U preserves the index of U.

theorem Subgroup.continuous_smul_const {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (U : Subgroup G) (u : G ⧸ U) : Continuous fun (γ : G) => γ • u

Translation of a fixed left coset is continuous under separate continuity of multiplication.

theorem Subgroup.continuous_inv_smul_const {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (U : Subgroup G) [DiscreteTopology (G ⧸ U)] (u : G ⧸ U) : Continuous fun (γ : G) => γ⁻¹ • u

Inverse translation of a fixed coset is continuous when the coset quotient is discrete.

theorem Subgroup.continuous_inv_smul {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (U : Subgroup G) [DiscreteTopology (G ⧸ U)] : Continuous fun (p : G × G ⧸ U) => p.1⁻¹ • p.2

Inverse translation on a discrete coset quotient is jointly continuous.

instance TauCeti.QuotientGroup.instDiscreteTopology {G : Type u_1} [Group G] [TopologicalSpace G] [DiscreteTopology G] (H : Subgroup G) : DiscreteTopology (G ⧸ H)

The quotient of a discrete group by any subgroup is discrete. This is Mathlib's QuotientGroup.discreteTopology read as an instance: in a discrete group every subgroup is open.

instance TauCeti.QuotientAddGroup.instDiscreteTopology {G : Type u_1} [AddGroup G] [TopologicalSpace G] [DiscreteTopology G] (H : AddSubgroup G) : DiscreteTopology (G ⧸ H)

The quotient of a discrete additive group by any additive subgroup is discrete. This is Mathlib's QuotientAddGroup.discreteTopology read as an instance: in a discrete additive group every additive subgroup is open.

theorem TauCeti.QuotientGroup.continuous_mapOfLE {G : Type u_1} [Group G] [TopologicalSpace G] {U V : Subgroup G} [U.Normal] [V.Normal] (hVU : V ≤ U) : Continuous ⇑(mapOfLE hVU)

The quotient homomorphism G ⧸ V →* G ⧸ U for normal subgroups V ≤ U of a topological group is continuous: composed with the quotient map of G modulo V it is the quotient map modulo U, and G ⧸ V carries the quotient topology.

theorem TauCeti.QuotientGroup.isClopen_image_mk {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] (U : OpenSubgroup G) : IsClopen (QuotientGroup.mk '' ↑U)

The image of an open subgroup of G in the quotient by a normal subgroup N is clopen: it is open because the quotient map is open, and closed because it is an open subgroup of the topological group G ⧸ N.

def TauCeti.QuotientGroup.comapMk'OpenNormalOrderIso {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] : OpenNormalSubgroup (G ⧸ N) ≃o { U : OpenNormalSubgroup G // N ≤ ↑U.toOpenSubgroup }

The correspondence theorem for open normal subgroups: the open normal subgroups of G ⧸ N correspond, as lattices, to the open normal subgroups of G containing N.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.QuotientGroup.comapMk'OpenNormalOrderIso_apply_toSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] (U : OpenNormalSubgroup (G ⧸ N)) : ↑(↑((comapMk'OpenNormalOrderIso N) U)).toOpenSubgroup = Subgroup.comap (QuotientGroup.mk' N) ↑U.toOpenSubgroup

@[simp]

theorem TauCeti.QuotientGroup.comapMk'OpenNormalOrderIso_symm_apply_toSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {N : Subgroup G} [N.Normal] (U : { V : OpenNormalSubgroup G // N ≤ ↑V.toOpenSubgroup }) : ↑((comapMk'OpenNormalOrderIso N).symm U).toOpenSubgroup = Subgroup.map (QuotientGroup.mk' N) ↑(↑U).toOpenSubgroup

def TauCeti.quotientOpenSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (U : OpenSubgroup G) : OpenSubgroup (G ⧸ N)

The image of an open subgroup U in G / N, as an open subgroup.

Equations

• TauCeti.quotientOpenSubgroup N U = { toSubgroup := Subgroup.map (QuotientGroup.mk' N) ↑U, isOpen' := ⋯ }

theorem TauCeti.toSubgroup_quotientOpenSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (U : OpenSubgroup G) : ↑(quotientOpenSubgroup N U) = Subgroup.map (QuotientGroup.mk' N) ↑U

The subgroup underlying quotientOpenSubgroup is the image subgroup.

@[simp]

theorem TauCeti.mem_quotientOpenSubgroup_mk_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (U : OpenSubgroup G) (hNU : N ≤ ↑U) (g : G) : ↑g ∈ quotientOpenSubgroup N U ↔ g ∈ U

Membership in U / N pulls back to membership in U when N ≤ U.

@[simp]

theorem TauCeti.quotientOpenSubgroup_index {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (U : OpenSubgroup G) (hNU : N ≤ ↑U) : (↑(quotientOpenSubgroup N U)).index = (↑U).index

Passing from U to its image in G / N preserves the index when N ≤ U.

def TauCeti.quotientOpenSubgroupMap {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (U : OpenSubgroup G) : ↥↑U →* ↥↑(quotientOpenSubgroup N U)

The quotient homomorphism restricted from U to its image in G / N.

Equations

• TauCeti.quotientOpenSubgroupMap N U = ((QuotientGroup.mk' N).comp (↑U).subtype).codRestrict ↑(TauCeti.quotientOpenSubgroup N U) ⋯

@[simp]

theorem TauCeti.coe_quotientOpenSubgroupMap {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (U : OpenSubgroup G) (u : ↥↑U) : ↑((quotientOpenSubgroupMap N U) u) = ↑↑u

The restricted quotient homomorphism has the expected value in G / N.

theorem TauCeti.quotientOpenSubgroupMap_surjective {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (U : OpenSubgroup G) : Function.Surjective ⇑(quotientOpenSubgroupMap N U)

The restricted quotient homomorphism is surjective: every element of the image of U in G / N is the image of an element of U.

theorem TauCeti.continuous_quotientOpenSubgroupMap {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] (U : OpenSubgroup G) : Continuous ⇑(quotientOpenSubgroupMap N U)

The restricted quotient homomorphism is continuous.

noncomputable def TauCeti.quotientSubgroupOfEquivMap {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V W : Subgroup G) [V.Normal] (hV : IsOpen ↑V) : ↥W ⧸ V.subgroupOf W ≃ₜ* ↥(Subgroup.map (QuotientGroup.mk' V) W)

For an open normal subgroup V and any subgroup W of G, the quotient W ⧸ V.subgroupOf W is isomorphic, as a topological group, to the image W.map (mk' V) of W in G ⧸ V. This is Noether's first isomorphism theorem for the composite W → G → G ⧸ V, whose kernel is V.subgroupOf W; both groups are discrete because V is open.

Equations

• TauCeti.quotientSubgroupOfEquivMap V W hV = { toMulEquiv := QuotientGroup.liftEquiv (V.subgroupOf W) ⋯ ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.coe_quotientSubgroupOfEquivMap_mk {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V W : Subgroup G) [V.Normal] (hV : IsOpen ↑V) (w : ↥W) : ↑((quotientSubgroupOfEquivMap V W hV) ↑w) = ↑↑w

quotientSubgroupOfEquivMap sends the class of w : W to the class of w in G ⧸ V.

noncomputable def TauCeti.quotientQuotientContinuousMulEquiv {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V W : Subgroup G) [V.Normal] [W.Normal] (hVW : V ≤ W) (hV : IsOpen ↑V) : (G ⧸ V) ⧸ Subgroup.map (QuotientGroup.mk' V) W ≃ₜ* G ⧸ W

For an open normal subgroup V contained in a normal subgroup W, the third isomorphism theorem (G ⧸ V) ⧸ W.map (mk' V) ≃* G ⧸ W is an isomorphism of topological groups, both groups being discrete.

Equations

• TauCeti.quotientQuotientContinuousMulEquiv V W hVW hV = { toMulEquiv := QuotientGroup.quotientQuotientEquivQuotient V W hVW, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.quotientQuotientContinuousMulEquiv_mk {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V W : Subgroup G) [V.Normal] [W.Normal] (hVW : V ≤ W) (hV : IsOpen ↑V) (g : G) : (quotientQuotientContinuousMulEquiv V W hVW hV) ↑↑g = ↑g

quotientQuotientContinuousMulEquiv sends the class of the class of g to the class of g.