theorem squarefree_dvd_B_of_descent (A B r ℓ m σ : ℤ) (hr_sq : Squarefree r) (hcop : IsCoprime ℓ m) (heq : r ^ 2 * ℓ ^ 4 + A * r * ℓ ^ 2 * m ^ 2 + B * m ^ 4 = r * m ^ 4 * σ ^ 2) : r ∣ B

Descent divisibility: if $r$ is squarefree, $\gcd(\ell, m) = 1$, and $r^2\ell^4 + Ar\ell^2 m^2 + Bm^4 = rm^4\sigma^2$, then $r \mid B$.

theorem lemma_25_5 (A B : ℤ) (hB : B ≠ 0) : {r : ℤ | Squarefree r ∧ ∃ (ℓ : ℤ) (m : ℤ) (σ : ℤ), IsCoprime ℓ m ∧ r ^ 2 * ℓ ^ 4 + A * r * ℓ ^ 2 * m ^ 2 + B * m ^ 4 = r * m ^ 4 * σ ^ 2}.Finite

(Lemma 25.5) The set of squarefree integers $r$ admitting a coprime quadruple $(\ell, m, \sigma)$ with $r^2\ell^4 + Ar\ell^2 m^2 + Bm^4 = rm^4\sigma^2$ is finite (it is contained in the divisors of $B$).

structure DescentData : Type 1

Abstract descent data: an abelian group $A$, a subgroup $\mathrm{im}(\varphi) \subseteq A$, a non-zero integer $B$ controlling the descent, and a "descent representative" $A \to \mathbb{Z}$.

• B : ℤ
• hB : self.B ≠ 0
• carrier : Type
• instAddCommGroup : AddCommGroup self.carrier
• imageOfPhi : AddSubgroup self.carrier
• descentRepr : self.carrier → ℤ

theorem lemma_25_5_descent_dvd (d : DescentData) (x : d.carrier) : d.descentRepr x ∣ d.B

Axiom packaging Lemma 25.5: the descent representative of any element divides $B$.

theorem lemma_25_3_compat (d : DescentData) (a b : d.carrier) : -a + b ∈ d.imageOfPhi → d.descentRepr a = d.descentRepr b

Compatibility part of Lemma 25.3: equivalent elements modulo $\mathrm{im}(\varphi)$ have the same descent representative.

theorem lemma_25_3_sep (d : DescentData) (a b : d.carrier) : d.descentRepr a = d.descentRepr b → -a + b ∈ d.imageOfPhi

Separation part of Lemma 25.3: elements with the same descent representative differ by an element of $\mathrm{im}(\varphi)$.

noncomputable def DescentData.quotientMap (d : DescentData) : d.carrier ⧸ d.imageOfPhi → ℤ

The descent representative descends to a function on the quotient $A/\mathrm{im}(\varphi)$.

theorem DescentData.quotientMap_injective (d : DescentData) : Function.Injective d.quotientMap

The descent representative is injective on the quotient $A/\mathrm{im}(\varphi)$ by the separation part of Lemma 25.3.

theorem DescentData.quotient_finite (d : DescentData) : Finite (d.carrier ⧸ d.imageOfPhi)

The quotient $A/\mathrm{im}(\varphi)$ in any descent data is finite.

theorem corollary_25_6 (d₁ d₂ : DescentData) : Finite (d₁.carrier ⧸ d₁.imageOfPhi) ∧ Finite (d₂.carrier ⧸ d₂.imageOfPhi)

(Corollary 25.6) For two descent data, both quotients $A_1/\mathrm{im}(\varphi_1)$ and $A_2/\mathrm{im}(\varphi_2)$ are finite.

theorem lemma_25_5_image_finite (E'Q : Type) [AddCommGroup E'Q] (π : E'Q →+ Additive (ℚˣ ⧸ Subgroup.square ℚˣ)) (B : ℤ) (hB : B ≠ 0) (intRepr : ℚˣ ⧸ Subgroup.square ℚˣ → ℤ) (hRepr_inj : Function.Injective intRepr) (hπ_dvd : ∀ (P : E'Q), intRepr (Additive.toMul (π P)) ∣ B) : (Set.range ⇑π).Finite

Image-finiteness version of Lemma 25.5: if a homomorphism $\pi : E'(\mathbb{Q}) \to \mathbb{Q}^\times/(\mathbb{Q}^\times)^2$ has integer representatives all dividing a fixed nonzero integer $B$, then the image of $\pi$ is finite.