The algebra norm and trace of a quadratic algebra #
QuadraticAlgebra R a b is free of rank two over R, on the basis 1, ω with ω² = a + bω.
Its explicit norm QuadraticAlgebra.norm and trace QuadraticAlgebra.trace are the determinant
and the trace of multiplication on that basis, so they agree with the general Algebra.norm and
Algebra.trace of a finite free algebra.
These comparisons let the general theory of Algebra.norm (for instance surjectivity of the norm
of an extension of finite fields, or Hensel's lemma for the norm) be applied to the explicit norm
form x² + bxy - ay².
Main results #
QuadraticAlgebra.algebraNorm_eq_norm:Algebra.norm R z = z.norm.QuadraticAlgebra.algebraTrace_eq_trace:Algebra.trace R _ z = trace z.
@[simp]
theorem
QuadraticAlgebra.algebraNorm_eq_norm
{R : Type u_1}
[CommRing R]
{a b : R}
(z : QuadraticAlgebra R a b)
:
The algebra norm of QuadraticAlgebra R a b over R is its explicit norm
z.re² + b z.re z.im - a z.im².
@[simp]
theorem
QuadraticAlgebra.algebraTrace_eq_trace
{R : Type u_1}
[CommRing R]
{a b : R}
(z : QuadraticAlgebra R a b)
:
The algebra trace of QuadraticAlgebra R a b over R is its explicit trace
2 z.re + b z.im.