The subgroup of nth powers

Facts about Gⁿ, the range of the nth-power homomorphism of a commutative group G, and about Mathlib's subgroup of squares G², which is the case n = 2.

When is a class trivial? For a unit group G = Mˣ, the class of u in Mˣ ⧸ (Mˣ)ⁿ is trivial exactly when u is an nth power in M. The side of the witness is the content: triviality of the class hands back an nth root that is itself a unit, while call sites naturally produce a root that is a bare element of M.

How large is the index? In a commutative group generated by a finite set S, the range of the nth-power homomorphism has index at most n ^ S.card when n is nonzero. In particular, the range of the squaring homomorphism has index at most 2 ^ S.card.

How does it move along homomorphisms? A homomorphism carries squares to squares, so G² lands inside the preimage of H². This is the side condition that descends a homomorphism to the quotients by squares.

Main results

• TauCeti.powMonoidHom_range_mk_eq_one_iff_exists_pow: the class of a unit in Mˣ ⧸ (Mˣ)ⁿ is trivial iff the unit is an nth power in M.
• TauCeti.square_eq_range_powMonoidHom: G² is the range of the squaring homomorphism.
• MonoidHom.square_le_comap: G² ≤ (H²).comap f for a homomorphism f : G →* H.
• TauCeti.index_square_le_of_closure_eq_top: [G : G²] ≤ 2 ^ S.card.

Provenance

The index argument is migrated from kim-em/erdos-unit-distance, where it was an abstract step towards bounding the index of squares in the unit group of a number field.

powMonoidHom_range_mk_eq_one_iff_exists_pow generalises the 2-descent's square-class criterion, which it replaces: that was stated only for the étale algebra of an elliptic curve, as WeierstrassCurve.Affine.M.mk_eq_one_iff in MordellWeil/XSubT.lean. The argument is Michael Stoll's, from EllipticCurves/Mathlib/Basic.lean lines 93-99 and 145-147 (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, pinned by TauCetiRoadmap/EllipticCurves/README.md at 66889eada51a), where it is split between IsUnit.exists_pow_eq_unit_iff and Units.modPow.unit_eq_one_iff; the two are one statement here.

theorem TauCeti.powMonoidHom_range_mk_eq_one_iff_exists_pow {M : Type u_1} [CommMonoid M] (n : ℕ) (u : Mˣ) : ↑u = 1 ↔ ∃ (z : M), z ^ n = ↑u

A class in Mˣ ⧸ (Mˣ)ⁿ is trivial exactly when its representative is an nth power in M. Triviality of the class means u = v ^ n for a unit v, and the useful form asks only for a root z : M; the two agree because an nth root of a unit is a unit once n ≠ 0, and at n = 0 both sides say u = 1. No hypothesis on n is needed, although the proof splits on it.

theorem TauCeti.square_eq_range_powMonoidHom {G : Type u_1} [CommGroup G] : Subgroup.square G = (powMonoidHom 2).range

In a commutative group, Mathlib's subgroup of squares agrees with the range of the squaring homomorphism.

theorem MonoidHom.square_le_comap {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] (f : G →* H) : Subgroup.square G ≤ Subgroup.comap f (Subgroup.square H)

A monoid homomorphism of commutative groups carries squares to squares, so the subgroup of squares of the source lands inside the preimage of the subgroup of squares of the target. This is the side condition needed to descend f to a map of the quotients by squares.

theorem TauCeti.index_square_le_of_closure_eq_top {G : Type u_1} [CommGroup G] {S : Finset G} (hS : Subgroup.closure ↑S = ⊤) : (Subgroup.square G).index ≤ 2 ^ S.card

In a commutative group generated by a finite set S, the subgroup of squares has index at most 2 ^ S.card. The quotient by the squares is an elementary abelian 2-group spanned by the image of S.