Binary diagonal quadratic forms in normal form

A binary form here is a diagonal form in two variables, that is QuadraticMap.weightedSumSquares R ![a, b] : QuadraticForm R (Fin 2 → R), classically written ⟨a, b⟩. This file proves the two normal-form theorems that pin such a form down.

The first is the representation normal form: a unit c is represented by ⟨a, b⟩ exactly when c may be taken as the first coefficient, the second being forced to a * b * c. Its content is a single explicit change of variables. If a x² + b y² = c with c invertible, then the vector (x, y) and its orthogonal companion (-b y, a x) form a basis, because the determinant of the pair is exactly c, and reading ⟨a, b⟩ in that basis gives ⟨c, a b c⟩. Since a * b * c and a * b * c⁻¹ differ by the square c², the two spellings of the second coefficient found in the sources present the same form. Only the represented value has to be a unit here, so this half of the theory is developed over a commutative ring.

The second is the binary equivalence criterion: two binary forms with unit coefficients are isometric exactly when they have the same discriminant modulo squares and represent a common unit. One direction follows from the discriminant change-of-variables formula; the other applies the representation normal form to both sides and compares the forced second coefficients.

Both statements are about the unit value set QuadraticMap.unitValueSet. Invertibility of the represented value carries the whole content of the first theorem: every quadratic form represents 0 through the zero vector, so a reading at c = 0 says nothing.

Main definitions

• TauCeti.isometryEquivBinaryNormalForm: the change of variables carrying ⟨c, a b c⟩ to ⟨a, b⟩, built from a solution of a x² + b y² = c.

Main results

• TauCeti.mem_unitValueSet_binary_iff_equivalent: the representation normal form, Lam I.2.3 (2).
• TauCeti.equivalent_binaryNormalForm_inv: the two spellings a b c and a b c⁻¹ of the forced second coefficient present the same form.
• TauCeti.isSquare_mul_mul_of_equivalent_binary: isometric binary forms have equal discriminants modulo squares.
• TauCeti.apply_mul_eq_of_equivalent_binary: a multiplicative pairing constant on isometric binary forms agrees on their discriminants.
• TauCeti.equivalent_binary_iff: the binary equivalence criterion, Lam I.5.1.

References

• T. Y. Lam, Introduction to Quadratic Forms over Fields, Graduate Studies in Mathematics 67, American Mathematical Society (2005), Chapter I, Proposition 2.3 and Proposition 5.1.

theorem TauCeti.represents_binary_left {R : Type u} [CommSemiring R] (a b : R) : (QuadraticMap.weightedSumSquares R ![a, b]).Represents a

A binary diagonal form represents its first coefficient.

theorem TauCeti.mem_unitValueSet_binary_left {R : Type u} [CommSemiring R] (a : Rˣ) (b : R) : a ∈ (QuadraticMap.weightedSumSquares R ![↑a, b]).unitValueSet

The first coefficient of a binary diagonal form lies in its unit value set.

def TauCeti.isometryEquivBinaryNormalForm {R : Type u} [CommRing R] (a b x y : R) (c : Rˣ) (h : a * x ^ 2 + b * y ^ 2 = ↑c) : (QuadraticMap.weightedSumSquares R ![↑c, a * b * ↑c]).IsometryEquiv (QuadraticMap.weightedSumSquares R ![a, b])

The binary representation normal form as an explicit change of variables: a solution of a x² + b y² = c with c invertible carries ⟨c, a * b * c⟩ to ⟨a, b⟩.

The map sends the first standard basis vector to (x, y), on which ⟨a, b⟩ takes the value c, and the second to the orthogonal companion (-b y, a x), on which ⟨a, b⟩ takes the value a * b * c. Its determinant is a x² + b y² = c, which is why the hypothesis asks for a unit.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.isometryEquivBinaryNormalForm_apply {R : Type u} [CommRing R] (a b x y : R) (c : Rˣ) (h : a * x ^ 2 + b * y ^ 2 = ↑c) (v : Fin 2 → R) : (isometryEquivBinaryNormalForm a b x y c h) v = ![x * v 0 - b * y * v 1, y * v 0 + a * x * v 1]

The explicit coordinates of the isometry on a vector.

@[simp]

theorem TauCeti.isometryEquivBinaryNormalForm_symm_apply {R : Type u} [CommRing R] (a b x y : R) (c : Rˣ) (h : a * x ^ 2 + b * y ^ 2 = ↑c) (v : Fin 2 → R) : (isometryEquivBinaryNormalForm a b x y c h).symm v = ![↑c⁻¹ * (a * x * v 0 + b * y * v 1), ↑c⁻¹ * (x * v 1 - y * v 0)]

The explicit coordinates of the inverse isometry on a vector.

theorem TauCeti.equivalent_binaryNormalForm_of_mem_unitValueSet {R : Type u} [CommRing R] {a b : R} {c : Rˣ} (h : c ∈ (QuadraticMap.weightedSumSquares R ![a, b]).unitValueSet) : (QuadraticMap.weightedSumSquares R ![a, b]).Equivalent (QuadraticMap.weightedSumSquares R ![↑c, a * b * ↑c])

The binary representation normal form, Lam I.2.3 (2): a unit represented by a binary diagonal form may be taken as its first coefficient.

theorem TauCeti.mem_unitValueSet_binary_iff_equivalent {R : Type u} [CommRing R] (a b : R) (c : Rˣ) : c ∈ (QuadraticMap.weightedSumSquares R ![a, b]).unitValueSet ↔ (QuadraticMap.weightedSumSquares R ![a, b]).Equivalent (QuadraticMap.weightedSumSquares R ![↑c, a * b * ↑c])

The binary representation normal form, Lam I.2.3 (2). A binary diagonal form represents a unit c exactly when it is isometric to ⟨c, a * b * c⟩.

⚠ That c is a unit is essential: every quadratic form represents the scalar 0 through the zero vector, and ⟨a, b⟩ is in general not isometric to ⟨0, 0⟩.

theorem TauCeti.equivalent_binaryNormalForm_inv {R : Type u} [CommRing R] (a b : R) (c : Rˣ) : (QuadraticMap.weightedSumSquares R ![↑c, a * b * ↑c]).Equivalent (QuadraticMap.weightedSumSquares R ![↑c, a * b * ↑c⁻¹])

The two spellings of the second coefficient of the binary normal form present the same form: a * b * c and a * b * c⁻¹ differ by the square c², so ⟨c, a b c⟩ and ⟨c, a b c⁻¹⟩ are isometric.

Sources state the normal form both ways, the second because the square class of the second coefficient is forced to be that of the discriminant a * b divided by c.

theorem TauCeti.equivalent_binary_of_isSquare_of_mem_unitValueSet {R : Type u} [CommRing R] {a b c d e : Rˣ} (hdisc : IsSquare (a * b * (c * d))) (hab : e ∈ (QuadraticMap.weightedSumSquares R ![↑a, ↑b]).unitValueSet) (hcd : e ∈ (QuadraticMap.weightedSumSquares R ![↑c, ↑d]).unitValueSet) : (QuadraticMap.weightedSumSquares R ![↑a, ↑b]).Equivalent (QuadraticMap.weightedSumSquares R ![↑c, ↑d])

Two binary diagonal forms with unit coefficients that have the same discriminant modulo squares and represent a common unit are isometric. This is the substantial direction of Lam I.5.1, and it needs no assumption on the characteristic.

theorem TauCeti.isSquare_mul_mul_of_equivalent_binary {R : Type u} [CommRing R] [Invertible 2] {a b c d : Rˣ} (h : (QuadraticMap.weightedSumSquares R ![↑a, ↑b]).Equivalent (QuadraticMap.weightedSumSquares R ![↑c, ↑d])) : IsSquare (a * b * (c * d))

Isometric binary diagonal forms with unit coefficients have the same discriminant modulo squares: the discriminant of ⟨a, b⟩ is a * b and that of ⟨c, d⟩ is c * d, and the two agree modulo squares exactly when their product a * b * (c * d) is a square.

theorem TauCeti.apply_mul_eq_of_equivalent_binary {R : Type u} [CommRing R] [Invertible 2] {M : Type u_1} [CommMonoid M] {F : Rˣ → Rˣ → M} (hmul : ∀ (a b c : Rˣ), F (a * b) c = F a c * F b c) (hF : ∀ (a b c d : Rˣ), (QuadraticMap.weightedSumSquares R ![↑a, ↑b]).Equivalent (QuadraticMap.weightedSumSquares R ![↑c, ↑d]) → F a b = F c d) {a b c d : Rˣ} (h : (QuadraticMap.weightedSumSquares R ![↑a, ↑b]).Equivalent (QuadraticMap.weightedSumSquares R ![↑c, ↑d])) (x : Rˣ) : F (a * b) x = F (c * d) x

A pairing that is multiplicative in its first argument and constant on the coefficients of isometric binary forms takes the same values at the two discriminants of isometric binary forms.

theorem TauCeti.equivalent_binary_iff {R : Type u} [CommRing R] [Invertible 2] (a b c d : Rˣ) : (QuadraticMap.weightedSumSquares R ![↑a, ↑b]).Equivalent (QuadraticMap.weightedSumSquares R ![↑c, ↑d]) ↔ IsSquare (a * b * (c * d)) ∧ ∃ e ∈ (QuadraticMap.weightedSumSquares R ![↑a, ↑b]).unitValueSet, e ∈ (QuadraticMap.weightedSumSquares R ![↑c, ↑d]).unitValueSet

The binary equivalence criterion, Lam I.5.1. Two binary diagonal forms with unit coefficients are isometric exactly when their discriminants agree modulo squares and they represent a common unit.

The quotient-free spelling IsSquare (a * b * (c * d)) of "equal discriminants" is the one that TauCeti.squareClass_eq_zero_iff translates into the square-class group.

theorem TauCeti.anisotropic_binary_one_one_iff {F : Type u_1} [Field F] : (QuadraticMap.weightedSumSquares F ![1, 1]).Anisotropic ↔ ¬IsSquare (-1)

The binary form ⟨1, 1⟩ is anisotropic exactly when -1 is not a square.