Integrality from a monic quadratic relation

Mathlib's IsIntegral.of_aeval_monic_of_isIntegral_coeff takes a monic polynomial and asks for each coefficient to be integral. Applying it to a quadratic means writing the polynomial out, discharging the degree computation, and answering the coefficient obligation index by index — the same half-dozen lines every time.

Main results

• IsIntegral.of_sq_add_mul_add_eq_zero: if y ^ 2 + b * y + c = 0 with b and c integral over R, then y is integral over R.

The relation is stated as an equation rather than through Polynomial.aeval, which is the form a caller actually holds: a change-of-variables identity or a curve equation, rearranged by linear_combination.

Provenance

Extracted from TauCeti/AlgebraicGeometry/EllipticCurve/Integrality.lean, where it was a private helper for WeierstrassCurve.isIntegral_y_of_equation_of_isIntegral_x with a note that it was "kept here rather than exported, since isIntegral_y_of_equation_of_isIntegral_x is its only consumer". A second consumer now exists — the coordinates of a change of variables between integral Weierstrass models — so the note no longer holds and the statement moves to where both can reach it. The proof is unchanged; only the name is now IsIntegral-prefixed, since nothing about it is about elliptic curves.

theorem IsIntegral.of_sq_add_mul_add_eq_zero {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {b c y : A} (hb : IsIntegral R b) (hc : IsIntegral R c) (h : y ^ 2 + b * y + c = 0) : IsIntegral R y

An element satisfying a monic quadratic relation with integral coefficients is integral. y, b and c live in an arbitrary commutative R-algebra A, and the relation is an equation in A rather than a statement about Polynomial.aeval, so a caller supplies whatever identity it already holds.