The image index before and after quotienting

For a homomorphism f : A →* B and a normal subgroup S ≤ B, the order-index formula relates the image index to its index after quotienting the target by S:

[B : f(A)] · #f⁻¹(S) = [B/S : image(f)] · #S · #ker(f).

In particular, when f reflects torsion and the source torsion is finite, this computes the correction between the cokernel on the whole group and the cokernel modulo torsion. The latter is the index of the image on the free quotients of finitely generated abelian groups.

The proof uses Mathlib's order-index formula Subgroup.card_ker_mul_card_range and Tau Ceti's image-index factorization Subgroup.index_map_mul_relIndex_ker.

theorem TauCeti.index_range_mul_card_comap_mul {A : Type u_1} {B : Type u_2} [Group A] [Group B] {f : A →* B} {S : Subgroup B} [S.Normal] : f.range.index * Nat.card ↥(Subgroup.comap f S) = (Subgroup.map (QuotientGroup.mk' S) f.range).index * Nat.card ↥S * Nat.card ↥f.ker

The order-index formula relating a homomorphism's image index to its image after quotienting the target by a normal subgroup. No finiteness is required for this cross-multiplied identity: infinite orders and indices are read as 0.

theorem TauCeti.index_range_mul_card_comap {A : Type u_1} {B : Type u_2} [AddGroup A] [AddGroup B] {f : A →+ B} {S : AddSubgroup B} [S.Normal] : f.range.index * Nat.card ↥(AddSubgroup.comap f S) = (AddSubgroup.map (QuotientAddGroup.mk' S) f.range).index * Nat.card ↥S * Nat.card ↥f.ker

The order-index formula relating an additive homomorphism's image index to its image after quotienting the target by a normal subgroup. No finiteness is required: infinite orders and indices are read as 0.