English
For a nonzero f in an S-module over a PID, the norm of f factors as a product of Smith coefficients.
Русский
Норма f в модуле S над PID распадается на произведение smithCoeffs.
LaTeX
$$Associated (Algebra.norm R f) (∏ i, smithCoeffs b _ (span {f}) i)$$
Lean4
/-- 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`. -/
theorem associated_norm_prod_smith [Fintype ι] (b : Basis ι R S) {f : S} (hf : f ≠ 0) :
Associated (Algebra.norm R f) (∏ i, smithCoeffs b _ (span_singleton_eq_bot.not.2 hf) i) :=
by
have hI := span_singleton_eq_bot.not.2 hf
let b' := ringBasis b (span { f }) hI
classical
rw [← Matrix.det_diagonal, ← LinearMap.det_toLin b']
let e :=
(b'.equiv ((span { f }).selfBasis b hI) <| Equiv.refl _).trans ((LinearEquiv.coord S S f hf).restrictScalars R)
refine (LinearMap.associated_det_of_eq_comp e _ _ ?_).symm
dsimp only [e, LinearEquiv.trans_apply]
simp_rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.comp_apply, ← LinearMap.ext_iff]
refine b'.ext fun i => ?_
simp_rw [LinearMap.comp_apply, LinearEquiv.coe_toLinearMap, Matrix.toLin_apply, Basis.repr_self,
Finsupp.single_eq_pi_single, Matrix.diagonal_mulVec_single, Pi.single_apply, ite_smul, zero_smul,
Finset.sum_ite_eq', mul_one, if_pos (Finset.mem_univ _), b'.equiv_apply]
change _ = f * _
rw [mul_comm, ← smul_eq_mul, LinearEquiv.restrictScalars_apply]
-- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
erw [LinearEquiv.coord_apply_smul]
rw [Ideal.selfBasis_def]
rfl
