The third isomorphism theorem for coset spaces

For a normal subgroup N of G and an arbitrary subgroup H, the cosets of the image H·N/N in G ⧸ N are the cosets of H ⊔ N in G. This is Noether's third isomorphism theorem with the normality of the upper subgroup dropped: H is unconstrained, so neither (G ⧸ N) ⧸ H·N/N nor G ⧸ (H ⊔ N) need carry a group structure, and what remains is a bijection of coset spaces. Mathlib's QuotientGroup.quotientQuotientEquivQuotient is the group isomorphism this generalises, stated for N ≤ M with M normal.

The bijection is what a family or a sum indexed by cosets needs. The corresponding index equality, Subgroup.index_map_mk'_eq_index_sup, records only that the two coset spaces have equal Nat.card — the same finite cardinality when they are finite, and jointly 0 when they are infinite, whatever their cardinalities. It supplies no correspondence between the cosets themselves, so it cannot reindex a family.

Main results

• QuotientGroup.quotientQuotientEquivQuotientSup: the bijection (G ⧸ N) ⧸ H.map (mk' N) ≃ G ⧸ (H ⊔ N), sending the class of g to the class of g.

def QuotientGroup.quotientQuotientEquivQuotientSup {G : Type u_1} [Group G] (H N : Subgroup G) [N.Normal] : (G ⧸ N) ⧸ Subgroup.map (mk' N) H ≃ G ⧸ H ⊔ N

The third isomorphism theorem for coset spaces. For a normal N and an arbitrary subgroup H, the cosets of the image of H in G ⧸ N are the cosets of H ⊔ N in G, both directions sending the class of g to the class of g.

Mathlib's QuotientGroup.quotientQuotientEquivQuotient is the group isomorphism this generalises: it asks for N ≤ M with M normal, so that both sides are groups and the map is a homomorphism. Here neither side need be a group — H is unconstrained — and what survives is the bijection of coset spaces, which is what a coset-indexed sum or family needs.

Equations

• QuotientGroup.quotientQuotientEquivQuotientSup H N = { toFun := Quotient.lift (Subgroup.quotientMapOfLE ⋯) ⋯, invFun := Quotient.lift (fun (g : G) => ↑↑g) ⋯, left_inv := ⋯, right_inv := ⋯ }

def QuotientAddGroup.quotientQuotientEquivQuotientSup {G : Type u_1} [AddGroup G] (H N : AddSubgroup G) [N.Normal] : (G ⧸ N) ⧸ AddSubgroup.map (mk' N) H ≃ G ⧸ H ⊔ N

The third isomorphism theorem for coset spaces, additive version: for a normal N and an arbitrary subgroup H, the cosets of the image of H in G ⧸ N are the cosets of H ⊔ N in G.

Equations

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

@[simp]

theorem QuotientGroup.quotientQuotientEquivQuotientSup_mk_mk {G : Type u_1} [Group G] (H N : Subgroup G) [N.Normal] (g : G) : (quotientQuotientEquivQuotientSup H N) ↑↑g = ↑g

The equivalence sends the nested class of g to the class of g.

@[simp]

theorem QuotientAddGroup.quotientQuotientEquivQuotientSup_mk_mk {G : Type u_1} [AddGroup G] (H N : AddSubgroup G) [N.Normal] (g : G) : (quotientQuotientEquivQuotientSup H N) ↑↑g = ↑g

The equivalence sends the nested class of g to the class of g.

@[simp]

theorem QuotientGroup.quotientQuotientEquivQuotientSup_symm_mk {G : Type u_1} [Group G] (H N : Subgroup G) [N.Normal] (g : G) : (quotientQuotientEquivQuotientSup H N).symm ↑g = ↑↑g

The inverse equivalence sends the class of g to the nested class of g.

@[simp]

theorem QuotientAddGroup.quotientQuotientEquivQuotientSup_symm_mk {G : Type u_1} [AddGroup G] (H N : AddSubgroup G) [N.Normal] (g : G) : (quotientQuotientEquivQuotientSup H N).symm ↑g = ↑↑g

The inverse equivalence sends the class of g to the nested class of g.