Index of the image of a subgroup

Under a surjective homomorphism, the index of a subgroup factors into the index of its image and its relative index in the kernel. This counts the contribution lost on passing to a quotient, for instance the contribution of principal ideles to an idele-class index.

Main results

• Subgroup.index_map_mul_relIndex_ker: the image-index factorization for groups.
• AddSubgroup.index_map_mul_relIndex_ker: the same factorization for additive groups.

For a subgroup H and a surjective homomorphism f with proof hf, use H.index_map_mul_relIndex_ker f hf. The same dot notation works for additive subgroups.

theorem Subgroup.index_map_mul_relIndex_ker {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (H : Subgroup G) (f : G →* G') (hf : Function.Surjective ⇑f) : (map f H).index * H.relIndex f.ker = H.index

The index of a subgroup under a surjection factors into the image index and the relative index in the kernel. Infinite indices have the usual value zero.

theorem AddSubgroup.index_map_mul_relIndex_ker {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G →+ G') (hf : Function.Surjective ⇑f) : (map f H).index * H.relIndex f.ker = H.index

The index of an additive subgroup under a surjection factors into the image index and the relative index in the kernel. Infinite indices have the usual value zero.