The norm on AdjoinRoot g is a resultant

For a monic g : R[X] and any p : R[X], the norm of AdjoinRoot.mk g p over R is the resultant of g and p:

Algebra.norm R (AdjoinRoot.mk g p) = g.resultant p g.natDegree p.natDegree.

Write m = g.natDegree and k = p.natDegree. Mathlib's Sylvester map S : R[X]_m × R[X]_k →ₗ R[X]_(m + k), (u, v) ↦ g * v + p * u, has the Sylvester matrix as its matrix, so det S is the resultant (Polynomial.toMatrix_sylvesterMap'). Taking p = 1 gives Ψ : (u, v) ↦ g * v + u, which for monic g is a linear equivalence — its inverse is division with remainder, q ↦ (q %ₘ g, q /ₘ g) — and det Ψ = resultant g 1 m k = 1.

Then S = Ψ ∘ₗ B for the endomorphism B = Ψ⁻¹ ∘ₗ S of R[X]_m × R[X]_k, which is (u, v) ↦ ((p * u) %ₘ g, v + (p * u) /ₘ g). In the block decomposition B is lower triangular with diagonal blocks mulModByMonic hg p and 1, so det B = det (mulModByMonic hg p). Finally AdjoinRoot.degreeLTEquiv hg : R[X]_m ≃ₗ AdjoinRoot g conjugates mulModByMonic hg p into multiplication by mk g p, whose determinant is the norm by definition.

No signs appear anywhere: B is an endomorphism, so the two blocks are never reordered.

Main results

• Polynomial.mulModByMonic — multiplication by p on R[X]_(g.natDegree), the map that AdjoinRoot.degreeLTEquiv turns into multiplication by mk g p.
• Polynomial.sylvesterEquivOne — the Sylvester map of g and 1 is a linear equivalence, inverted by division with remainder.
• Polynomial.det_sylvesterBlock — the block-triangular B has the determinant of its upper-left block.
• AdjoinRoot.degreeLTEquiv — mk g restricted to R[X]_(g.natDegree) is a linear equivalence onto AdjoinRoot g, with coe_degreeLTEquiv_symm_apply/_mk characterising its inverse.
• AdjoinRoot.norm_mk_eq_det_mulModByMonic, AdjoinRoot.norm_mk_eq_resultant — the norm as a determinant, and then as a resultant.
• AdjoinRoot.norm_algebraMap_sub_root, AdjoinRoot.norm_mk_C_sub_X_add — the two values that resultant algebra reads off it: the norm of x - θ, and, when g has x as a root, the norm of the corrected representative x - θ + q θ that replaces it. The first is stated in simp-normal form and is @[simp]; the second carries side conditions simp cannot discharge and is used by explicit rw.

Provenance

Adapted from Michael Stoll's EllipticCurves (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0) at commit 66889eada51a74c2f5dfb7fb5909b0b5a0a2d96e, file EllipticCurves/Mathlib/Basic.lean lines 694-919, where the result is a Mathlib-bound prerequisite of the explicit 2-descent. The source targets Lean v4.32.0 and predates parts of Mathlib's current API, so this is a forward port rather than a copy: degreeLTEquiv is built from Mathlib's AdjoinRoot.modByMonicHom instead of from a bijectivity argument, and the source's Monic.resultant_one_right is replaced by Mathlib's Polynomial.resultant_one_right.

norm_algebraMap_sub_root and norm_mk_C_sub_X_add come from the same repository at the same commit, EllipticCurves/WeakMordellWeil.lean lines 277-313, where they are stated for the polynomial of an elliptic curve. Their proofs use no curve input beyond monicity and the factorization, so they are stated here at that level instead.

noncomputable def Polynomial.mulModByMonic {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (p : Polynomial R) : ↥(degreeLT R g.natDegree) →ₗ[R] ↥(degreeLT R g.natDegree)

Multiplication by p on R[X]_(g.natDegree), that is, q ↦ (p * q) %ₘ g. This is the map that AdjoinRoot.degreeLTEquiv hg turns into multiplication by AdjoinRoot.mk g p.

Equations

• Polynomial.mulModByMonic hg p = { toFun := fun (q : ↥(Polynomial.degreeLT R g.natDegree)) => ⟨p * ↑q %ₘ g, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Polynomial.mulModByMonic_apply_coe {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (p : Polynomial R) (q : ↥(degreeLT R g.natDegree)) : ↑((mulModByMonic hg p) q) = p * ↑q %ₘ g

noncomputable def Polynomial.sylvesterEquivOne {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (n : ℕ) : (↥(degreeLT R g.natDegree) × ↥(degreeLT R n)) ≃ₗ[R] ↥(degreeLT R (g.natDegree + n))

For monic g, the Sylvester map of g and 1, namely (u, v) ↦ g * v + u, is a linear equivalence R[X]_(g.natDegree) × R[X]_n ≃ₗ R[X]_(g.natDegree + n). Its inverse is division with remainder, q ↦ (q %ₘ g, q /ₘ g). This is the general-monic analogue of Mathlib's Polynomial.degreeLT.addLinearEquiv, which is the case g = X ^ m.

Equations

• Polynomial.sylvesterEquivOne hg n = LinearEquiv.ofBijective (g.sylvesterMap 1 ⋯ ⋯) ⋯

@[simp]

theorem Polynomial.coe_sylvesterEquivOne {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (n : ℕ) : ↑(sylvesterEquivOne hg n) = g.sylvesterMap 1 ⋯ ⋯

theorem Polynomial.coe_sylvesterEquivOne_apply {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (n : ℕ) (w : ↥(degreeLT R g.natDegree) × ↥(degreeLT R n)) : ↑((sylvesterEquivOne hg n) w) = g * ↑w.2 + ↑w.1

@[simp]

theorem Polynomial.coe_sylvesterEquivOne_symm_fst {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (n : ℕ) (q : ↥(degreeLT R (g.natDegree + n))) : ↑((sylvesterEquivOne hg n).symm q).1 = ↑q %ₘ g

The first coordinate of the inverse of sylvesterEquivOne is · %ₘ g.

@[simp]

theorem Polynomial.coe_sylvesterEquivOne_symm_snd {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (n : ℕ) (q : ↥(degreeLT R (g.natDegree + n))) : ↑((sylvesterEquivOne hg n).symm q).2 = ↑q /ₘ g

The second coordinate of the inverse of sylvesterEquivOne is · /ₘ g.

noncomputable def Polynomial.sylvesterBlock {R : Type u_1} [CommRing R] {g : Polynomial R} {n : ℕ} (hg : g.Monic) (p : Polynomial R) (hp : p.natDegree ≤ n) : ↥(degreeLT R g.natDegree) × ↥(degreeLT R n) →ₗ[R] ↥(degreeLT R g.natDegree) × ↥(degreeLT R n)

The block-triangular endomorphism B = Ψ⁻¹ ∘ₗ S of R[X]_(g.natDegree) × R[X]_n.

Equations

• Polynomial.sylvesterBlock hg p hp = ↑(Polynomial.sylvesterEquivOne hg n).symm ∘ₗ g.sylvesterMap p ⋯ hp

theorem Polynomial.sylvesterBlock_eq {R : Type u_1} [CommRing R] {g : Polynomial R} {n : ℕ} (hg : g.Monic) (p : Polynomial R) (hp : p.natDegree ≤ n) : sylvesterBlock hg p hp = ↑(sylvesterEquivOne hg n).symm ∘ₗ g.sylvesterMap p ⋯ hp

@[simp]

theorem Polynomial.coe_sylvesterBlock_apply_fst {R : Type u_1} [CommRing R] {g : Polynomial R} {n : ℕ} (hg : g.Monic) (p : Polynomial R) (hp : p.natDegree ≤ n) (u : ↥(degreeLT R g.natDegree)) (v : ↥(degreeLT R n)) : ↑((sylvesterBlock hg p hp) (u, v)).1 = p * ↑u %ₘ g

The first coordinate of B (u, v) is (p * u) %ₘ g.

@[simp]

theorem Polynomial.coe_sylvesterBlock_apply_snd {R : Type u_1} [CommRing R] {g : Polynomial R} {n : ℕ} (hg : g.Monic) (p : Polynomial R) (hp : p.natDegree ≤ n) (u : ↥(degreeLT R g.natDegree)) (v : ↥(degreeLT R n)) : ↑((sylvesterBlock hg p hp) (u, v)).2 = ↑v + p * ↑u /ₘ g

The second coordinate of B (u, v) is v + (p * u) /ₘ g.

theorem Polynomial.det_sylvesterBlock {R : Type u_1} [CommRing R] {g : Polynomial R} {n : ℕ} (hg : g.Monic) (p : Polynomial R) (hp : p.natDegree ≤ n) : LinearMap.det (sylvesterBlock hg p hp) = LinearMap.det (mulModByMonic hg p)

The determinant of the block-triangular map B is the determinant of its upper-left block.

noncomputable def AdjoinRoot.degreeLTEquiv {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) : ↥(Polynomial.degreeLT R g.natDegree) ≃ₗ[R] AdjoinRoot g

For monic g, AdjoinRoot.mk g restricted to the polynomials of degree < g.natDegree is a linear equivalence onto AdjoinRoot g. Its inverse is Mathlib's AdjoinRoot.modByMonicHom, corestricted to R[X]_(g.natDegree).

Not to be confused with Polynomial.degreeLTEquiv, which reads the same submodule off as its coefficient vector Fin n → R; the namespace says which target is meant.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AdjoinRoot.degreeLTEquiv_apply {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (q : ↥(Polynomial.degreeLT R g.natDegree)) : (degreeLTEquiv hg) q = (mk g) ↑q

@[simp]

theorem AdjoinRoot.coe_degreeLTEquiv_symm_apply {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (a : AdjoinRoot g) : ↑((degreeLTEquiv hg).symm a) = (modByMonicHom hg) a

The inverse of degreeLTEquiv is Mathlib's AdjoinRoot.modByMonicHom: it picks the representative of degree < g.natDegree.

theorem AdjoinRoot.coe_degreeLTEquiv_symm_mk {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (q : Polynomial R) : ↑((degreeLTEquiv hg).symm ((mk g) q)) = q %ₘ g

The inverse of degreeLTEquiv sends the class of q to q %ₘ g. Deliberately not @[simp]: coe_degreeLTEquiv_symm_apply and Mathlib's AdjoinRoot.modByMonicHom_mk are both simp lemmas, so the simp set already normalises this left-hand side and tagging it too would put it out of simp-normal form.

theorem AdjoinRoot.norm_mk_eq_det_mulModByMonic {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (p : Polynomial R) : (Algebra.norm R) ((mk g) p) = LinearMap.det (Polynomial.mulModByMonic hg p)

The norm of mk g p is the determinant of multiplication by p on R[X]_(g.natDegree), because degreeLTEquiv hg conjugates the latter into multiplication by mk g p.

theorem AdjoinRoot.norm_mk_eq_resultant {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (p : Polynomial R) : (Algebra.norm R) ((mk g) p) = g.resultant p

The norm on AdjoinRoot g is a resultant. For monic g, the norm of AdjoinRoot.mk g p over the base ring is the resultant of g and p. Equivalently, it is the product of the values of p at the roots of g.

@[simp]

theorem AdjoinRoot.norm_algebraMap_sub_root {R : Type u_1} [CommRing R] {g : Polynomial R} (hg : g.Monic) (x : R) : (Algebra.norm R) ((of g) x - root g) = Polynomial.eval x g

The norm of x - θ is g x. Here θ is root g, the image of X in AdjoinRoot g, and of g x is the image of x, so the left-hand side is the norm of x - θ.

Stated in this form rather than as Algebra.norm R (mk g (C x - X)) because that is what simp normalises to: mk is a ring hom and mk_C, mk_X are rfl, so the mk spelling rewrites away before any lemma stated in it can match.

theorem AdjoinRoot.norm_mk_C_sub_X_add {R : Type u_1} [CommRing R] {g q : Polynomial R} {x : R} (hq : q.Monic) (hgq : g = q * (Polynomial.X - Polynomial.C x)) : (Algebra.norm R) ((mk g) (Polynomial.C x - Polynomial.X + q)) = Polynomial.eval x q ^ 2

At a root the corrected representative has square norm. If g = q * (X - C x) with q monic, then x - θ is a zero divisor in AdjoinRoot g, and the corrected representative x - θ + q θ that replaces it has norm (q.eval x) ^ 2.

Deliberately not @[simp], unlike norm_algebraMap_sub_root: g, q and x are all fixed by the left-hand side, so hgq : g = q * (X - C x) and hq : q.Monic become rigid side goals that the default discharger would have to prove. At the shape this targets they are f_eq_mul_of_eval_eq_zero hx — which needs a hypothesis not visible to simp — and the untagged monic_fCofactor. Use it by explicit rw.

For 2 ≤ q.natDegree the factorization splits the resultant into two factors, each equal to q.eval x: against X - C x the corrected representative is evaluated at x, and against q the added multiple of q drops out, leaving a resultant with C x - X. Below that degree the resultant bookkeeping does not apply and the representative is a scalar instead: at q.natDegree = 1 the X terms cancel and it is C (q.eval x) in an algebra of rank 2, and at q.natDegree = 0 it is 1, as is q.eval x.