Norms on free modules over principal ideal domains #
theorem
associated_norm_prod_smith
{R : Type u_1}
{S : Type u_2}
{ι : Type u_3}
[CommRing R]
[IsDomain R]
[IsPrincipalIdealRing R]
[CommRing S]
[IsDomain S]
[Algebra R S]
[Fintype ι]
(b : Basis ι R S)
{f : S}
(hf : f ≠ 0)
:
Associated ((Algebra.norm R) f) (∏ i : ι, Ideal.smithCoeffs b (Ideal.span {f}) ⋯ i)
For a nonzero element f in an algebra S over a principal ideal domain R that is finite and
free as an R-module, the norm of f relative to R is associated to the product of the Smith
coefficients of the ideal generated by f.
instance
instFiniteDimensionalQuotientPolynomialIdealSpanSingletonSetSmithCoeffs
{S : Type u_2}
{ι : Type u_3}
[CommRing S]
[IsDomain S]
{F : Type u_4}
[Field F]
[Algebra (Polynomial F) S]
[Finite ι]
(b : Basis ι (Polynomial F) S)
{I : Ideal S}
(hI : I ≠ ⊥)
(i : ι)
:
FiniteDimensional F (Polynomial F ⧸ Ideal.span {Ideal.smithCoeffs b I hI i})
theorem
finrank_quotient_span_eq_natDegree_norm
{S : Type u_2}
{ι : Type u_3}
[CommRing S]
[IsDomain S]
{F : Type u_4}
[Field F]
[Algebra (Polynomial F) S]
[Finite ι]
[Algebra F S]
[IsScalarTower F (Polynomial F) S]
(b : Basis ι (Polynomial F) S)
{f : S}
(hf : f ≠ 0)
:
For a nonzero element f in a F[X]-module S, the dimension of $S/\langle f \rangle$ as an
F-vector space is the degree of the norm of f relative to F[X].