Ring-theoretic properties of quadratic algebras

This file collects ring-theoretic properties of QuadraticAlgebra R a b as an R-algebra.

Main results

• QuadraticAlgebra.polynomial_discr_eq_discr: the discriminant of the polynomial X ^ 2 - C b * X - C a equals discr a b.
• Algebra.trace_quadraticAlgebra_apply and Algebra.norm_quadraticAlgebra_apply: Algebra.trace and Algebra.norm on QuadraticAlgebra R a b agree with QuadraticAlgebra.trace and QuadraticAlgebra.norm.
• Algebra.discr_quadraticAlgebra: Algebra.discr R (basis a b) equals discr a b.

theorem QuadraticAlgebra.polynomial_discr_eq_discr {R : Type u_1} [CommRing R] (a b : R) : (Polynomial.X ^ 2 - Polynomial.C b * Polynomial.X - Polynomial.C a).discr = discr a b

The discriminant of the polynomial X ^ 2 - C b * X - C a is the discriminant discr a b of the quadratic algebra QuadraticAlgebra R a b.

theorem Algebra.leftMulMatrix_quadraticAlgebra {R : Type u_1} [CommRing R] {a b : R} (z : QuadraticAlgebra R a b) : (leftMulMatrix (QuadraticAlgebra.basis a b)) z = !![z.re, a * z.im; z.im, z.re + b * z.im]

The matrix of left multiplication by z in the basis {1, ω}.

@[simp]

theorem Algebra.trace_quadraticAlgebra_apply {R : Type u_1} [CommRing R] {a b : R} (z : QuadraticAlgebra R a b) : (trace R (QuadraticAlgebra R a b)) z = QuadraticAlgebra.trace z

The algebra trace of QuadraticAlgebra R a b is the elementary trace.

@[simp]

theorem Algebra.norm_quadraticAlgebra_apply {R : Type u_1} [CommRing R] {a b : R} (z : QuadraticAlgebra R a b) : (norm R) z = QuadraticAlgebra.norm z

The algebra norm of QuadraticAlgebra R a b is the elementary norm.

@[simp]

theorem Algebra.discr_quadraticAlgebra {R : Type u_1} [CommRing R] {a b : R} : discr R ⇑(QuadraticAlgebra.basis a b) = QuadraticAlgebra.discr a b

The Algebra.discr of the standard basis {1, ω} is the elementary discriminant.