Kernels and cokernels of a composite

For homomorphisms f : A →* B and g : B →* C of arbitrary groups, this file proves the cross-multiplied index identity

[C : gf(A)] · #ker(f) · #ker(g) = [C : g(B)] · [B : f(A)] · #ker(g ∘ f),

where [B : f(A)] is the cardinality of the coset space B ⧸ f(A). It needs no finiteness hypothesis: infinite orders and indices are read as 0, and either both sides are 0 or all six quantities are finite. The images need not be normal.

When the kernels and indices are finite, write z(f) = [B : f(A)] / #ker(f). Dividing out gives z(g ∘ f) = z(g) · z(f). For abelian groups the indices are the orders of the cokernels, and this is the count along the kernel–cokernel exact sequence

0 → ker f → ker (g ∘ f) → ker g → coker f → coker (g ∘ f) → coker g → 0.

For an isogeny φ : E → E' with dual φ̂, the composite φ̂ ∘ φ is multiplication by deg φ, so on the points over a field this gives z([deg φ]) = z(φ̂) · z(φ) whenever the kernels and cokernels involved are finite. Ratios of this kind over local fields are the local factors in Cassels' proof that the Birch–Swinnerton-Dyer quotient is an isogeny invariant.

Main results

• MonoidHom.index_range_comp_mul_card_ker_mul_card_ker and its additive form AddMonoidHom.index_range_comp_mul_card_ker_mul_card_ker: the cross-multiplied index identity for a composite.

References

• J. W. S. Cassels, Arithmetic on curves of genus 1. VIII. On conjectures of Birch and Swinnerton-Dyer, J. Reine Angew. Math. 217 (1965), 180–199.
• J. S. Milne, Arithmetic Duality Theorems, 2nd ed., I.7.

theorem MonoidHom.index_range_comp_mul_card_ker_mul_card_ker {A : Type u_1} {B : Type u_2} {C : Type u_3} [Group A] [Group B] [Group C] (f : A →* B) (g : B →* C) : (g.comp f).range.index * (Nat.card ↥f.ker * Nat.card ↥g.ker) = g.range.index * f.range.index * Nat.card ↥(g.comp f).ker

The index identity for a composite: for f : A →* B and g : B →* C, [C : gf(A)] · #ker(f) · #ker(g) = [C : g(B)] · [B : f(A)] · #ker(g ∘ f), with subgroup indices counting cosets. No finiteness is required: infinite orders and indices are read as 0. When all of them are finite, this says [B : f(A)] / #ker(f) is multiplicative along the composite.

theorem AddMonoidHom.index_range_comp_mul_card_ker_mul_card_ker {A : Type u_1} {B : Type u_2} {C : Type u_3} [AddGroup A] [AddGroup B] [AddGroup C] (f : A →+ B) (g : B →+ C) : (g.comp f).range.index * (Nat.card ↥f.ker * Nat.card ↥g.ker) = g.range.index * f.range.index * Nat.card ↥(g.comp f).ker

The index identity for a composite: for f : A →+ B and g : B →+ C, [C : gf(A)] · #ker(f) · #ker(g) = [C : g(B)] · [B : f(A)] · #ker(g ∘ f), with subgroup indices counting cosets. No finiteness is required: infinite orders and indices are read as 0. When all of them are finite, this says [B : f(A)] / #ker(f) is multiplicative along the composite.