associated_norm_prod_smith
theorem associated_norm_prod_smith :
∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} [inst : CommRing R] [inst_1 : IsDomain R]
[inst_2 : IsPrincipalIdealRing R] [inst_3 : CommRing S] [inst_4 : IsDomain S] [inst_5 : Algebra R S]
[inst_6 : Fintype ι] (b : Basis ι R S) {f : S} (hf : f ≠ 0),
Associated ((Algebra.norm R) f) (Finset.univ.prod fun i => Ideal.smithCoeffs b (Ideal.span {f}) ⋯ i)
This theorem states that for a non-zero 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` with respect to `R` is associated with the product of the Smith coefficients of the ideal generated by `f`. In other words, for a non-zero element `f` in an algebra `S` over `R` with a finite basis `b`, the determinant of the multiplication by `f` is related to the product of the Smith coefficients of the ideal generated by `{f}` in the structure of a principal ideal ring. The Smith coefficients are calculated using the basis `b`. This association means there exists some unit in the ring, when multiplied with the norm of `f`, gives the product of Smith coefficients.
More concisely: For a non-zero element `f` in a finite, free algebra `S` over a principal ideal domain `R`, the norm of `f` is equal to the product of its Smith coefficients in the ideal generated by `{f}`.
|
finrank_quotient_span_eq_natDegree_norm
theorem finrank_quotient_span_eq_natDegree_norm :
∀ {S : Type u_2} {ι : Type u_3} [inst : CommRing S] [inst_1 : IsDomain S] {F : Type u_4} [inst_2 : Field F]
[inst_3 : Algebra (Polynomial F) S] [inst_4 : Finite ι] [inst_5 : Algebra F S]
[inst_6 : IsScalarTower F (Polynomial F) S],
Basis ι (Polynomial F) S →
∀ {f : S},
f ≠ 0 → FiniteDimensional.finrank F (S ⧸ Ideal.span {f}) = ((Algebra.norm (Polynomial F)) f).natDegree
This theorem states that for a nonzero element `f` in a module `S` over the polynomial ring `F[X]`, the dimension of the quotient space `S/` as a vector space over the field `F` is equal to the degree of the norm of `f` with respect to the polynomial ring `F[X]`. Here, `` denotes the ideal generated by `f` in `S`, and the norm of `f` is computed as the determinant of the map defined by multiplication by `f` in the `R`-algebra. The theorem requires a basis of `S` over `F[X]` for its proof.
More concisely: The dimension of the quotient space of a nonzero module `S` over the polynomial ring `F[X]` by the ideal generated by `f` is equal to the degree of the norm of `f` as a linear map from `S` to itself.
|