Indices in quotient groups

This file records how the index of the image of a subgroup in a quotient group is computed in the original group. It is the Nat.card shadow of the coset-space bijection QuotientGroup.quotientQuotientEquivQuotientSup, and is read off it.

Main results

• Subgroup.index_map_mk'_eq_index_sup: the index of the image of H in G ⧸ N is the index of H ⊔ N in G.

@[simp]

theorem Subgroup.index_map_mk'_eq_index_sup {G : Type u_1} [Group G] (H N : Subgroup G) [N.Normal] : (map (QuotientGroup.mk' N) H).index = (H ⊔ N).index

The index of the image of a subgroup in a quotient is the index of its join with the quotienting subgroup: the two coset spaces are in bijection, by QuotientGroup.quotientQuotientEquivQuotientSup.

@[simp]

theorem AddSubgroup.index_map_mk'_eq_index_sup {G : Type u_1} [AddGroup G] (H N : AddSubgroup G) [N.Normal] : (map (QuotientAddGroup.mk' N) H).index = (H ⊔ N).index