Minimal polynomials of quadratic elements

This file collects reusable facts about minimal polynomials of quadratic elements.

Main results

• TauCeti.Algebra.minpoly_eq_X_sq_sub_C_of_sq_eq_of_natDegree_eq_two: the minimal polynomial of a quadratic element of an F-algebra whose square is in the base field F.
• IsIntegral.exists_quadratic_relation: a degree-two integral element of a ring algebra satisfies a monic quadratic relation over its commutative base ring.

theorem TauCeti.Algebra.minpoly_eq_X_sq_sub_C_of_sq_eq_of_natDegree_eq_two {F : Type u_1} {L : Type u_2} [Field F] [Ring L] [Algebra F L] {x : L} {r : F} (hx2 : x ^ 2 = (algebraMap F L) r) (hdegree : (minpoly F x).natDegree = 2) : minpoly F x = Polynomial.X ^ 2 - Polynomial.C r

The minimal polynomial of a quadratic element whose square is r is X² - r.

Only the base F need be a field; L is an arbitrary F-algebra ring, so this also covers quadratic elements of noncommutative algebras, such as i in a quaternion algebra.

theorem IsIntegral.exists_quadratic_relation {K : Type u_1} {L : Type u_2} [CommRing K] [Ring L] [Algebra K L] {y : L} (hyint : IsIntegral K y) (hdeg : (minpoly K y).natDegree = 2) : ∃ (b : K) (c : K), y ^ 2 + (algebraMap K L) b * y + (algebraMap K L) c = 0

An integral element of degree two satisfies a monic quadratic relation over the base ring.