Integral Hilbert 90 for quadratic conjugation

This file proves Hilbert's Theorem 90 for quadratic conjugation in the integral form needed for ideal-class descent. Mathlib provides groupCohomology.exists_div_of_norm_eq_one; for a quadratic extension the elementary construction here gives an element of 𝓞 K rather than merely of K.

Main result

• NumberField.exists_ne_zero_mul_eq_mul_ringOfIntegersQuadraticConj: if nonzero x : 𝓞 K and y : 𝓞 K have equal products with their conjugates, there is nonzero ε : 𝓞 K satisfying x ε = y σε.

theorem NumberField.exists_ne_zero_mul_eq_mul_ringOfIntegersQuadraticConj {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) {x y : RingOfIntegers K} (hx : x ≠ 0) (hnorm : x * (ringOfIntegersQuadraticConj hmin hgen) x = y * (ringOfIntegersQuadraticConj hmin hgen) y) : ∃ (ε : RingOfIntegers K), ε ≠ 0 ∧ x * ε = y * (ringOfIntegersQuadraticConj hmin hgen) ε

Hilbert's Theorem 90 for quadratic conjugation. Let σ be the quadratic conjugation of a quadratic number field and let x y : 𝓞 K with x ≠ 0 have equal norms, x σx = y σy. Then there is a nonzero ε : 𝓞 K with x ε = y σε; equivalently y / x = ε / σε is a "coboundary". The construction is explicit: ε = σx (x + y) works unless x + y = 0, and then ε = σx θ x does.