Discriminant of a quadratic algebra

This file introduces the discriminant of a quadratic algebra QuadraticAlgebra R a b (with the convention ω² = a + b·ω), describes how it transforms under a change of generator, and derives the classification of quadratic algebras up to isomorphism together with a criterion, over a field, for QuadraticAlgebra K a b to be a field.

Main definitions

• QuadraticAlgebra.discr: the discriminant discr a b = b ^ 2 + 4 * a.

Main results

• QuadraticAlgebra.discr_changeGenerator: the discriminant scales by u ^ 2 under the change of generator ω ↦ u • ω + k.
• QuadraticAlgebra.exists_sq_eq_iff_isSquare_discr: over a ring with 2 invertible, X ^ 2 - b * X - a has a root iff discr a b is a square.
• QuadraticAlgebra.nonempty_algEquiv_iff_of_invertible_two and QuadraticAlgebra.nonempty_algEquiv_int_iff: the discriminant classifies quadratic algebras up to isomorphism, modulo squares of units when 2 is invertible and exactly over ℤ.
• QuadraticAlgebra.algEquivEdivEmod: over ℤ, a quadratic algebra of discriminant D is isomorphic to QuadraticAlgebra ℤ (D / 4) (D % 4).
• QuadraticAlgebra.nonempty_algEquiv_int_iff_discr_eq: for D ≡ 0, 1 mod 4, a quadratic algebra over ℤ is isomorphic to QuadraticAlgebra ℤ (D / 4) (D % 4) iff its discriminant is D, so these algebras are canonical representatives.
• QuadraticAlgebra.isField_iff_not_isSquare_discr: over a field with 2 ≠ 0, QuadraticAlgebra K a b is a field iff discr a b is not a square.

def QuadraticAlgebra.discr {R : Type u_1} [CommSemiring R] (a b : R) : R

The discriminant of the quadratic algebra QuadraticAlgebra R a b, that is, the discriminant b ^ 2 + 4 * a of the polynomial X ^ 2 - b * X - a.

Equations

• QuadraticAlgebra.discr a b = b ^ 2 + 4 * a

theorem QuadraticAlgebra.discr_def {R : Type u_1} [CommSemiring R] (a b : R) : discr a b = b ^ 2 + 4 * a

theorem QuadraticAlgebra.im_sq_mul_discr {R : Type u_1} [CommRing R] {a b : R} (z : QuadraticAlgebra R a b) : z.im ^ 2 * discr a b = trace z ^ 2 - 4 * norm z

z.im ^ 2 times the discriminant of the algebra equals trace z ^ 2 - 4 * norm z.

@[simp]

theorem QuadraticAlgebra.discr_algebraMap {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (a b : R) : discr ((algebraMap R S) a) ((algebraMap R S) b) = (algebraMap R S) (discr a b)

The discriminant commutes with a base change R → S.

theorem QuadraticAlgebra.discr_changeGenerator {R : Type u_1} [CommRing R] (a b u k : R) : discr (u ^ 2 * a - u * b * k - k ^ 2) (u * b + 2 * k) = u ^ 2 * discr a b

Under the change of generator ω ↦ u • ω + k (see QuadraticAlgebra.changeGenerator), the discriminant is multiplied by u ^ 2.

@[deprecated QuadraticAlgebra.discr_changeGenerator (since := "2026-08-14")]

theorem QuadraticAlgebra.discr_map {R : Type u_1} [CommRing R] (a b u k : R) : discr (u ^ 2 * a - u * b * k - k ^ 2) (u * b + 2 * k) = u ^ 2 * discr a b

Alias of QuadraticAlgebra.discr_changeGenerator.

---

Under the change of generator ω ↦ u • ω + k (see QuadraticAlgebra.changeGenerator), the discriminant is multiplied by u ^ 2.

theorem QuadraticAlgebra.algebraMap_discr {R : Type u_1} [CommRing R] (a b : R) : (algebraMap R (QuadraticAlgebra R a b)) (discr a b) = (omega - star omega) ^ 2

The discriminant is the square of the different ω - star ω.

theorem QuadraticAlgebra.exists_sq_eq_iff_isSquare_discr {R : Type u_1} [CommRing R] [Invertible 2] {a b : R} : (∃ (r : R), r ^ 2 = a + b * r) ↔ IsSquare (discr a b)

If 2 is invertible, the polynomial X ^ 2 - b * X - a has a root if and only if the discriminant is a square.

theorem QuadraticAlgebra.discr_eq_im_sq_mul_discr {R : Type u_1} [CommRing R] {a b a' b' : R} (f : QuadraticAlgebra R a b →ₐ[R] QuadraticAlgebra R a' b') (hf : Function.Injective ⇑f) : discr a b = (f omega).im ^ 2 * discr a' b'

The transformation law for an injective algebra map.

def QuadraticAlgebra.algEquivDiscrZero {R : Type u_1} [CommRing R] [Invertible 2] (a b : R) : QuadraticAlgebra R a b ≃ₐ[R] QuadraticAlgebra R (discr a b) 0

If 2 is a unit, QuadraticAlgebra R a b is isomorphic to the standard form QuadraticAlgebra R (discr a b) 0.

Equations

• QuadraticAlgebra.algEquivDiscrZero a b = (QuadraticAlgebra.changeGeneratorEquiv a b (unitOfInvertible 2) (-b) ⋯ ⋯).symm

@[simp]

theorem QuadraticAlgebra.algEquivDiscrZero_re {R : Type u_1} [CommRing R] {a b : R} [Invertible 2] (z : QuadraticAlgebra R a b) : ((algEquivDiscrZero a b) z).re = z.re + ⅟2 * b * z.im

@[simp]

theorem QuadraticAlgebra.algEquivDiscrZero_im {R : Type u_1} [CommRing R] {a b : R} [Invertible 2] (z : QuadraticAlgebra R a b) : ((algEquivDiscrZero a b) z).im = ⅟2 * z.im

@[simp]

theorem QuadraticAlgebra.algEquivDiscrZero_symm_re {R : Type u_1} [CommRing R] {a b : R} [Invertible 2] (z : QuadraticAlgebra R (discr a b) 0) : ((algEquivDiscrZero a b).symm z).re = z.re - b * z.im

@[simp]

theorem QuadraticAlgebra.algEquivDiscrZero_symm_im {R : Type u_1} [CommRing R] {a b : R} [Invertible 2] (z : QuadraticAlgebra R (discr a b) 0) : ((algEquivDiscrZero a b).symm z).im = 2 * z.im

@[simp]

theorem QuadraticAlgebra.algEquivDiscrZero_add_smul {R : Type u_1} [CommRing R] {a b : R} [Invertible 2] (x y : R) : (algEquivDiscrZero a b) (x • 1 + y • omega) = (x + ⅟2 * b * y) • 1 + (⅟2 * y) • omega

@[simp]

theorem QuadraticAlgebra.algEquivDiscrZero_symm_add_smul {R : Type u_1} [CommRing R] {a b : R} [Invertible 2] (x y : R) : (algEquivDiscrZero a b).symm (x • 1 + y • omega) = (x - b * y) • 1 + (2 * y) • omega

theorem QuadraticAlgebra.nonempty_algEquiv_iff {R : Type u_1} [CommRing R] {a b a' b' : R} (h : IsRegular 2) : Nonempty (QuadraticAlgebra R a b ≃ₐ[R] QuadraticAlgebra R a' b') ↔ ∃ (u : Rˣ), discr a b = ↑u ^ 2 * discr a' b' ∧ 2 ∣ b - ↑u * b'

If 2 is regular, QuadraticAlgebra R a b and QuadraticAlgebra R a' b' are isomorphic iff discr a b = u ^ 2 * discr a' b' for some unit u with 2 ∣ b - u * b'.

theorem QuadraticAlgebra.nonempty_algEquiv_iff_of_invertible_two {R : Type u_1} [CommRing R] {a b a' b' : R} [Invertible 2] : Nonempty (QuadraticAlgebra R a b ≃ₐ[R] QuadraticAlgebra R a' b') ↔ ∃ (u : Rˣ), discr a b = ↑u ^ 2 * discr a' b'

If 2 is invertible, the discriminant classifies quadratic algebras up to isomorphism, modulo squares of units.

theorem QuadraticAlgebra.nonempty_algEquiv_int_iff {a b a' b' : ℤ} : Nonempty (QuadraticAlgebra ℤ a b ≃ₐ[ℤ] QuadraticAlgebra ℤ a' b') ↔ discr a b = discr a' b'

Over ℤ the discriminant is a complete invariant of quadratic algebras up to isomorphism.

theorem QuadraticAlgebra.discr_ediv_emod {D : ℤ} (hD : D % 4 = 0 ∨ D % 4 = 1) : discr (D / 4) (D % 4) = D

For D ≡ 0, 1 mod 4, the canonical representative QuadraticAlgebra ℤ (D / 4) (D % 4) has discriminant D.

def QuadraticAlgebra.algEquivEdivEmod (a b : ℤ) : QuadraticAlgebra ℤ a b ≃ₐ[ℤ] QuadraticAlgebra ℤ (discr a b / 4) (discr a b % 4)

Every quadratic algebra over ℤ is isomorphic to the canonical representative of its discriminant, obtained by translating ω by the integer ⌊b / 2⌋.

Equations

• QuadraticAlgebra.algEquivEdivEmod a b = QuadraticAlgebra.changeGeneratorEquiv (QuadraticAlgebra.discr a b / 4) (QuadraticAlgebra.discr a b % 4) 1 (b / 2) ⋯ ⋯

@[simp]

theorem QuadraticAlgebra.re_algEquivEdivEmod_symm_apply (a b : ℤ) (a✝ : QuadraticAlgebra ℤ (discr a b / 4) (discr a b % 4)) : ((algEquivEdivEmod a b).symm a✝).re = a✝.re + -(a✝.im * (b / 2))

@[simp]

theorem QuadraticAlgebra.im_algEquivEdivEmod_symm_apply (a b : ℤ) (a✝ : QuadraticAlgebra ℤ (discr a b / 4) (discr a b % 4)) : ((algEquivEdivEmod a b).symm a✝).im = a✝.im

@[simp]

theorem QuadraticAlgebra.re_algEquivEdivEmod_apply (a b : ℤ) (a✝ : QuadraticAlgebra ℤ a b) : ((algEquivEdivEmod a b) a✝).re = a✝.re + a✝.im * (b / 2)

@[simp]

theorem QuadraticAlgebra.im_algEquivEdivEmod_apply (a b : ℤ) (a✝ : QuadraticAlgebra ℤ a b) : ((algEquivEdivEmod a b) a✝).im = a✝.im

@[simp]

theorem QuadraticAlgebra.algEquivEdivEmod_omega (a b : ℤ) : (algEquivEdivEmod a b) omega = (b / 2) • 1 + omega

theorem QuadraticAlgebra.nonempty_algEquiv_int_iff_discr_eq {a b D : ℤ} (hD : D % 4 = 0 ∨ D % 4 = 1) : Nonempty (QuadraticAlgebra ℤ a b ≃ₐ[ℤ] QuadraticAlgebra ℤ (D / 4) (D % 4)) ↔ discr a b = D

For D ≡ 0, 1 mod 4, a quadratic algebra over ℤ is isomorphic to the canonical representative QuadraticAlgebra ℤ (D / 4) (D % 4) iff its discriminant is D.

instance QuadraticAlgebra.instFactForallNeHPowOfNatHAddHMul_1 {K : Type u_2} [Field K] {a b : K} [NeZero 2] [Fact ¬IsSquare (discr a b)] : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)

theorem QuadraticAlgebra.not_isField_of_isSquare_discr {K : Type u_2} [Field K] [NeZero 2] {a b : K} (h : IsSquare (discr a b)) : ¬IsField (QuadraticAlgebra K a b)

If discr a b is a square, QuadraticAlgebra K a b is not a field.

theorem QuadraticAlgebra.isField_iff_not_isSquare_discr {K : Type u_2} [Field K] [NeZero 2] {a b : K} : IsField (QuadraticAlgebra K a b) ↔ ¬IsSquare (discr a b)

If 2 ≠ 0 in the field K, QuadraticAlgebra K a b is a field iff discr a b is not a square.