The index of multiplication on a finitely generated abelian group

This file is a narrow port of the finitely-generated-abelian-group part of Michael Stoll's EllipticCurves/Mathlib/SelmerGroup.lean, commit 3f8c39c0fc4c0fd0a40e693aa2a9bbda08d9ee1f.

It extends AddSubgroup.index_range_nsmul, which treats a finite free ℤ-module, to a finitely generated commutative group with torsion. The result will let a curve-specific two-descent turn a bound on E(ℚ) / 2 E(ℚ) into a bound on the Mordell--Weil rank.

theorem AddMonoidHom.card_ker_mul_card_range {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (φ : G →+ H) : Nat.card ↥φ.ker * Nat.card ↥φ.range = Nat.card G

First-isomorphism counting: the cardinality of an additive group is the cardinality of the kernel times the cardinality of the range of a homomorphism.

theorem AddMonoidHom.index_range_eq_card_ker {G : Type u_1} [AddGroup G] [Finite G] (φ : G →+ G) : φ.range.index = Nat.card ↥φ.ker

On a finite additive group, the index of the range of an endomorphism equals the cardinality of its kernel.

theorem AddEquiv.map_ker_nsmulAddMonoidHom {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] (e : M ≃+ N) (n : ℕ) : AddSubgroup.map e.toAddMonoidHom (nsmulAddMonoidHom n).ker = (nsmulAddMonoidHom n).ker

An additive equivalence maps the kernel of multiplication by n onto the corresponding kernel.

theorem nsmulAddMonoidHom_range_prod (A : Type u_1) (B : Type u_2) [AddCommGroup A] [AddCommGroup B] (n : ℕ) : (nsmulAddMonoidHom n).range = (nsmulAddMonoidHom n).range.prod (nsmulAddMonoidHom n).range

Multiplication by n on a product has the product of the two ranges as its range.

theorem nsmulAddMonoidHom_ker_prod (A : Type u_1) (B : Type u_2) [AddCommGroup A] [AddCommGroup B] (n : ℕ) : (nsmulAddMonoidHom n).ker = (nsmulAddMonoidHom n).ker.prod (nsmulAddMonoidHom n).ker

Multiplication by n on a product has the product of the two kernels as its kernel.

theorem Module.rank_eq_zero_of_finite (R : Type u_1) (M : Type u_2) [Ring R] [CharZero R] [AddCommGroup M] [Module R M] [Finite M] : Module.rank R M = 0

A finite module over a characteristic-zero ring has rank zero.

theorem AddSubgroup.index_range_nsmul_of_fg (G : Type u_1) [AddCommGroup G] [AddGroup.FG G] {n : ℕ} (hn : n ≠ 0) : (nsmulAddMonoidHom n).range.index = n ^ Module.finrank ℤ G * Nat.card ↥(nsmulAddMonoidHom n).ker

The index of nG in a finitely generated commutative group G is n ^ rank(G) times the cardinality of its n-torsion subgroup.