Norms on free modules over principal ideal domains #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
associated_norm_prod_smith
{R : Type u_1}
{S : Type u_2}
{ι : Type u_3}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[comm_ring S]
[is_domain S]
[algebra R S]
[fintype ι]
(b : basis ι R S)
{f : S}
(hf : f ≠ 0) :
associated (⇑(algebra.norm R) f) (finset.univ.prod (λ (i : ι), ideal.smith_coeffs 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.
@[protected, instance]
def
has_quotient.quotient.finite_dimensional
{S : Type u_2}
{ι : Type u_3}
[comm_ring S]
[is_domain S]
{F : Type u_4}
[field F]
[algebra (polynomial F) S]
[finite ι]
(b : basis ι (polynomial F) S)
{I : ideal S}
(hI : I ≠ ⊥)
(i : ι) :
finite_dimensional F (polynomial F ⧸ ideal.span {ideal.smith_coeffs b I hI i})
theorem
finrank_quotient_span_eq_nat_degree_norm
{S : Type u_2}
{ι : Type u_3}
[comm_ring S]
[is_domain S]
{F : Type u_4}
[field F]
[algebra (polynomial F) S]
[finite ι]
[algebra F S]
[is_scalar_tower F (polynomial F) S]
(b : basis ι (polynomial F) S)
{f : S}
(hf : f ≠ 0) :
finite_dimensional.finrank F (S ⧸ ideal.span {f}) = (⇑(algebra.norm (polynomial F)) f).nat_degree
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].