Power classes of a commutative group under equivalences and products

The group of n-th power classes of a commutative group G is the quotient G ⧸ (powMonoidHom n).range, the spelling Mathlib.RingTheory.DedekindDomain.SelmerGroup uses. This file transports that quotient along a multiplicative equivalence, and identifies the power classes of the units of a product with the product of the power classes of the units of the factors.

Main definitions

• QuotientGroup.congrRangePowMonoidHom: an equivalence G ≃* H induces G ⧸ (powMonoidHom n).range ≃* H ⧸ (powMonoidHom n).range.
• Units.modPowPiEquiv: taking n-th power classes of units commutes with products.

Main results

• QuotientGroup.pow_eq_one_quotient_range_powMonoidHom: every n-th power class is killed by n.

Provenance

Adapted, with the author's proofs, from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, pinned by TauCetiRoadmap/EllipticCurves/README.md at 66889eada51a), EllipticCurves/Mathlib/Basic.lean, section modPow, where the two are stated for the source's Units.modPow abbreviation. Mathlib's QuotientGroup.mulEquivPiModRangePowMonoidHom and MulEquiv.piUnits do the work of the source's Units.modPow.piEquiv; what is left here is the transport along an equivalence and the composition of those two. The source is written against Lean v4.32.0; this is a forward port. QuotientGroup.pow_eq_one_quotient_range_powMonoidHom is not from the source.

Roadmap

TauCetiRoadmap/EllipticCurves/README.md, Layer 6 (Mordell–Weil): the 2-descent map of the weak Mordell–Weil theorem lands in the square classes of an étale algebra and is controlled one field factor at a time, which is Units.modPowPiEquiv composed with the Chinese Remainder decomposition of that algebra (TauCeti.RingTheory.AdjoinRoot.Factors). Nothing here mentions a polynomial or a curve.

def QuotientGroup.congrRangePowMonoidHom {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] (e : G ≃* H) (n : ℕ) : G ⧸ (powMonoidHom n).range ≃* H ⧸ (powMonoidHom n).range

A multiplicative equivalence of commutative groups induces one on the quotients by the subgroups of n-th powers.

Equations

• QuotientGroup.congrRangePowMonoidHom e n = QuotientGroup.congr (powMonoidHom n).range (powMonoidHom n).range e ⋯

@[simp]

theorem QuotientGroup.congrRangePowMonoidHom_mk {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] (e : G ≃* H) (n : ℕ) (g : G) : (congrRangePowMonoidHom e n) ↑g = ↑(e g)

@[simp]

theorem QuotientGroup.pow_eq_one_quotient_range_powMonoidHom {G : Type u_1} [CommGroup G] (n : ℕ) (x : G ⧸ (powMonoidHom n).range) : x ^ n = 1

Every class modulo the subgroup of n-th powers is killed by n.

noncomputable def Units.modPowPiEquiv {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → CommMonoid (α i)] (n : ℕ) : ((i : ι) → α i)ˣ ⧸ (powMonoidHom n).range ≃* ((i : ι) → (α i)ˣ ⧸ (powMonoidHom n).range)

Taking n-th power classes of units commutes with products.

Equations

• Units.modPowPiEquiv α n = (QuotientGroup.congrRangePowMonoidHom MulEquiv.piUnits n).trans (QuotientGroup.mulEquivPiModRangePowMonoidHom (fun (i : ι) => (α i)ˣ) n)

@[simp]

theorem Units.modPowPiEquiv_mk {ι : Type u_1} (α : ι → Type u_2) [(i : ι) → CommMonoid (α i)] (n : ℕ) (u : ((i : ι) → α i)ˣ) (i : ι) : (modPowPiEquiv α n) (↑u) i = ↑(MulEquiv.piUnits u i)

On the class of a unit, Units.modPowPiEquiv is componentwise projection to the factors.