Double and simple roots of quadratics modulo the maximal ideal

Let R be a local ring with perfect residue field. If the discriminant a² + 4 b of the monic quadratic T² + a T − b lies in the maximal ideal, then the reduction of the quadratic has a double root in the residue field (Polynomial.exists_quadratic_eq_zero_and_two_mul_add_eq_zero_of_discrim_eq_zero), and any lift s ∈ R of it is a root of the quadratic and of its derivative modulo the maximal ideal. In characteristic two the double root is a square root, which is where perfectness is needed.

This is the completing-the-square step of Tate's algorithm (Step 6), where it is applied twice to the coefficients of a Weierstrass equation over a discrete valuation ring.

Conversely, over any local ring, if the discriminant a² + 4 b is a unit then every root t of T² + a T − b modulo the maximal ideal is simple: the derivative 2 t + a is a unit, since (2 t + a)² = 4 (t² + a t − b) + (a² + 4 b).

Main results

• TauCeti.IsLocalRing.exists_add_two_mul_mem_maximalIdeal_and_sub_mul_sub_sq_mem_maximalIdeal: if a² + 4 b ∈ 𝔪, some s has a + 2 s ∈ 𝔪 and b − s a − s² ∈ 𝔪.
• TauCeti.IsLocalRing.isUnit_two_mul_add_of_isUnit_sq_add_four_mul: if a² + 4 b is a unit and t² + a t − b ∈ 𝔪, then 2 t + a is a unit.
• TauCeti.HenselianLocalRing.exists_quadratic_root_of_isUnit_discriminant: in a Henselian local ring, a root modulo the maximal ideal of a monic quadratic with unit discriminant lifts to a root with unit derivative.

theorem TauCeti.IsLocalRing.isUnit_two_mul_add_of_isUnit_sq_add_four_mul {R : Type u_1} [CommRing R] [IsLocalRing R] {a b t : R} (hd : IsUnit (a ^ 2 + 4 * b)) (ht : t ^ 2 + a * t - b ∈ IsLocalRing.maximalIdeal R) : IsUnit (2 * t + a)

A root of T² + a T − b modulo the maximal ideal is simple when the discriminant a² + 4 b is a unit: if t² + a t − b ∈ 𝔪, then 2 t + a is a unit, since (2 t + a)² = 4 (t² + a t − b) + (a² + 4 b).

theorem TauCeti.IsLocalRing.exists_add_two_mul_mem_maximalIdeal_and_sub_mul_sub_sq_mem_maximalIdeal {R : Type u_1} [CommRing R] [IsLocalRing R] [PerfectField (IsLocalRing.ResidueField R)] {a b : R} (h : a ^ 2 + 4 * b ∈ IsLocalRing.maximalIdeal R) : ∃ (s : R), a + 2 * s ∈ IsLocalRing.maximalIdeal R ∧ b - s * a - s ^ 2 ∈ IsLocalRing.maximalIdeal R

A double root of T² + a T − b modulo the maximal ideal, lifted from the perfect residue field: if the discriminant a² + 4 b lies in the maximal ideal, some s ∈ R has a + 2 s ∈ 𝔪 and b − s a − s² ∈ 𝔪.

theorem TauCeti.HenselianLocalRing.exists_quadratic_root_of_isUnit_discriminant {R : Type u_1} [CommRing R] [HenselianLocalRing R] {a b t : R} (hd : IsUnit (a ^ 2 + 4 * b)) (ht : t ^ 2 + a * t - b ∈ IsLocalRing.maximalIdeal R) : ∃ (s : R), s ^ 2 + a * s - b = 0 ∧ s - t ∈ IsLocalRing.maximalIdeal R ∧ IsUnit (2 * s + a)

A root of T² + a T − b modulo the maximal ideal of a Henselian local ring lifts to a root in the same residue class with unit derivative when a² + 4 b is a unit.