Quadratic algebras over ℚ

Every quadratic algebra over ℚ with nonzero discriminant is isomorphic to a standard form QuadraticAlgebra ℚ d 0 for a unique squarefree integer d. This classifies quadratic algebras over ℚ by squarefree integers.

Main results

• QuadraticAlgebra.Rat.exists_squarefree_algEquiv: every QuadraticAlgebra ℚ a b with nonzero discriminant is isomorphic to QuadraticAlgebra ℚ d 0 for a squarefree integer d.
• QuadraticAlgebra.Rat.nonempty_algEquiv_iff: over ℚ, the squarefree integer d is a complete invariant of the standard form QuadraticAlgebra ℚ d 0.

theorem QuadraticAlgebra.Rat.exists_squarefree_algEquiv {a b : ℚ} (hd : discr a b ≠ 0) : ∃ (d : ℤ), Squarefree d ∧ Nonempty (QuadraticAlgebra ℚ a b ≃ₐ[ℚ] QuadraticAlgebra ℚ (↑d) 0)

Every QuadraticAlgebra ℚ a b with nonzero discriminant is isomorphic to QuadraticAlgebra ℚ d 0 for a squarefree integer d.

theorem QuadraticAlgebra.Rat.nonempty_algEquiv_iff {d₁ d₂ : ℤ} (h₁ : Squarefree d₁) (h₂ : Squarefree d₂) : Nonempty (QuadraticAlgebra ℚ (↑d₁) 0 ≃ₐ[ℚ] QuadraticAlgebra ℚ (↑d₂) 0) ↔ d₁ = d₂

For squarefree integers d₁, d₂, the standard forms QuadraticAlgebra ℚ d₁ 0 and QuadraticAlgebra ℚ d₂ 0 are isomorphic if and only if d₁ = d₂.