The determinant of the actual multiplication matrix gives a homogeneous polynomial of degree equal to the extension dimension. Its evaluation is the actual algebra norm. This construction is shared input for norm equations and the cohomology of function fields.
The actual norm as a polynomial in the coordinates of a basis.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped BigOperators
namespace Module.Basis
variable {F E ι : Type*} [Field F] [Field E] [Algebra F E]
[Fintype ι] [DecidableEq ι]def normPolynomial (b : Basis ι F E) : MvPolynomial ι FSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped BigOperators
namespace Module.Basis
variable {F E ι : Type*} [Field F] [Field E] [Algebra F E]
[Fintype ι] [DecidableEq ι]theorem eval_normPolynomial (b : Basis ι F E) (x : ι → F) :
MvPolynomial.eval x b.normPolynomial = Algebra.norm F (∑ i, x i • b i)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open scoped BigOperators
namespace Module.Basis
variable {F E ι : Type*} [Field F] [Field E] [Algebra F E]
[Fintype ι] [DecidableEq ι]theorem normPolynomial_isHomogeneous (b : Basis ι F E) :
b.normPolynomial.IsHomogeneous (Fintype.card ι)