Quadratic algebras and quadratic extensions

This file relates the concrete construction QuadraticAlgebra R a b to the predicate Algebra.IsQuadraticExtension: a QuadraticAlgebra is a quadratic extension of R, and conversely every commutative quadratic extension is isomorphic to a QuadraticAlgebra.

Main results

• a QuadraticAlgebra is a quadratic extension, as an instance;
• Algebra.IsQuadraticExtension.exists_algEquiv_quadraticAlgebra: every commutative quadratic extension is isomorphic to some QuadraticAlgebra R a b.

instance QuadraticAlgebra.instIsQuadraticExtension {R : Type u_1} [CommSemiring R] {a b : R} [StrongRankCondition R] : Algebra.IsQuadraticExtension R (QuadraticAlgebra R a b)

A quadratic algebra is a quadratic extension.

theorem Algebra.IsQuadraticExtension.exists_algEquiv_quadraticAlgebra {R : Type u_1} {A : Type u_2} [CommRing R] [StrongRankCondition R] [CommRing A] [Algebra R A] [IsQuadraticExtension R A] : ∃ (a : R) (b : R), Nonempty (A ≃ₐ[R] QuadraticAlgebra R a b)

Every quadratic extension A / R is isomorphic to QuadraticAlgebra R a b for some a, b.