Documentation

TauCeti.GroupTheory.Index.NSmul

The index of n • G in a finitely generated commutative group #

Mathlib's Mathlib/GroupTheory/IndexNSmul.lean computes the index of the image of the multiplication-by-n map nsmulAddMonoidHom n on a group that is free and finitely generated as a ℤ-module: AddSubgroup.index_range_nsmul gives n ^ finrank ℤ M. This file drops freeness.

Main results #

What the descent needs here is the exact count, not merely finiteness of the index. TauCetiRoadmap/EllipticCurves/README.md §Layer 6 makes explicit 2-descent a target in its own right, naming "the theorem converting its cardinality into a Mordell–Weil rank bound" and taking an explicit rank computation as its acceptance test. That conversion is this formula solved for the rank: from (G : nG) = n ^ finrank ℤ G * Nat.card G[n], a bound on the Selmer cardinality gives a bound on finrank ℤ G. Finiteness of the index alone carries no rank information — Mathlib's Subgroup.finiteIndex_range_powMonoidHom_of_fg, recorded below as already available, supplies exactly that and no more — so the free-case theorem this file generalises cannot be substituted for it either. The same formula is in turn the group-theoretic input to the finiteness of the Selmer group K(S,n) that the layer's weak Mordell–Weil bullet names, for the finitely generated — not free — group of S-units.

Everything here is adapted from Michael Stoll's elliptic-curves formalisation (github.com/MichaelStollBayreuth/EllipticCurves, EllipticCurves/Mathlib/SelmerGroup.lean at the roadmap's pin 66889eada51a, Apache 2.0, by Michael Stoll). Following this repository's convention for adapted material, the upstream authorship is credited here rather than in the copyright header, and each declaration carries its source name.

Not ported from that file, because Mathlib or this repository already has them: its Module.finite_int_additive and Group.fg_of_module_finite_int (Mathlib's AddMonoid.FG.to_moduleFinite_int and Module.Finite.iff_addGroup_fg composed with AddGroup.fg_iff_mul_fg), finite_of_fg_of_pow_eq_one (CommGroup.finite_of_fg_isMulTorsion), finite_modPow (Subgroup.finiteIndex_range_powMonoidHom_of_fg), card_ker_mul_card_range and index_range_eq_card_ker (AddSubgroup.index_range, which needs only FiniteIndex on the kernel rather than a finite ambient group, so the counting lemma that derived it is unnecessary), ker_nsmulAddMonoidHom (AddSubgroup.nsmulAddMonoidHom_injective_of_isTorsionFree through AddMonoidHom.ker_eq_bot_iff), its nsmulAddMonoidHom_range_prod and nsmulAddMonoidHom_ker_prod (AddMonoidHom.range_prodMap and AddMonoidHom.ker_prodMap, which apply once multiplication by n on a product is identified with the componentwise AddMonoidHom.prodMap, a step the proof below takes directly), and its Subgroup.fg_of_commGroup_fg and Group.fg_of_fg_ker_of_fg_range (both in TauCeti/GroupTheory/Finiteness.lean). Its Module.rank_eq_zero_of_finite has no Mathlib counterpart but is a three-line consequence of rank_eq_zero_iff used exactly once, so it is inlined at that use site rather than given a name. The source predates those additions, several of which its own author upstreamed, so check Mathlib again before porting anything further from it.

Its AddMonoidHom.range_nsmulAddMonoidHom, which identifies the range of multiplication by n on a commutative ring with the ideal generated by n, is a statement about rings rather than a step in this index computation, which nowhere uses it. It belongs with the ring-theoretic development that first needs it, not here.

source
theorem Subgroup.index_range_pow_mul_card_ker {G : Type u_1} [CommGroup G] (U : Subgroup G) [U.FiniteIndex] (n : ℕ) :
(powMonoidHom n).range.index * Nat.card ↥(powMonoidHom n).ker = Nat.card ↥(powMonoidHom n).ker * (powMonoidHom n).range.index

For a subgroup U of finite index in a commutative group G and any n, (G : Gⁿ) * #U[n] = #G[n] * (U : Uⁿ), where Gⁿ is the subgroup of n-th powers and G[n] the n-torsion subgroup. This is the cross-multiplied form of "(G : Gⁿ) / #G[n] is unchanged on passing to a finite-index subgroup"; it is the product, not the quotient statement, that holds at this generality, since with G[n] not assumed finite Nat.card and Subgroup.index may both be 0 and neither ratio need be defined.

source
theorem AddSubgroup.index_range_nsmul_add_card_ker {G : Type u_1} [AddCommGroup G] (U : AddSubgroup G) [U.FiniteIndex] (n : ℕ) :
(nsmulAddMonoidHom n).range.index * Nat.card ↥(nsmulAddMonoidHom n).ker = Nat.card ↥(nsmulAddMonoidHom n).ker * (nsmulAddMonoidHom n).range.index

For a subgroup U of finite index in a commutative group G and any n, (G : nG) * #U[n] = #G[n] * (U : nU). This is the cross-multiplied form of "(G : nG) / #G[n] is unchanged on passing to a finite-index subgroup"; it is the product, not the quotient statement, that holds at this generality, since with G[n] not assumed finite Nat.card and AddSubgroup.index may both be 0 and neither ratio need be defined.

source
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 M[n] to N[n]. This is the kernel counterpart of Mathlib's AddEquiv.map_range_nsmulAddMonoidHom.

source
theorem AddEquiv.index_range_nsmulAddMonoidHom {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] (e : M ≃+ N) (n : ℕ) :
(nsmulAddMonoidHom n).range.index = (nsmulAddMonoidHom n).range.index

The index of n • M is invariant under additive equivalence.

source
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 n • G in a finitely generated commutative group G is n ^ finrank ℤ G * #G[n], where G[n] is the n-torsion subgroup.

This extends Mathlib's AddSubgroup.index_range_nsmul, which is the free case: there the torsion subgroup is trivial and the second factor is 1.