English
For a fractional ideal I in 𝓞K, and any reindexing of the basis linking the standard integral basis to a basis of I, the absolute value of the determinant of this basis change equals the absolute norm of I.
Русский
Для дробного идеала I над 𝓞K и произвольного отображения базиса от обычного интегрального базиса к базису I, модульDet имеет абсолютное значение, равное AbsNorm(I).
LaTeX
$$$\\Big| \\det\\big( (\\text{integralBasis } K) \\big) \\big( (\\text{basisOfFractionalIdeal } K I) \\!\\text{.reindex } e^{-1} \\big) \\Big| \;=\; \\operatorname{absNorm}(I).$$$
Lean4
/-- The absolute value of the determinant of the base change from `integralBasis` to
`basisOfFractionalIdeal I` is equal to the norm of `I`. -/
theorem det_basisOfFractionalIdeal_eq_absNorm (I : (FractionalIdeal (𝓞 K)⁰ K)ˣ)
(e : (Free.ChooseBasisIndex ℤ (𝓞 K)) ≃ (Free.ChooseBasisIndex ℤ I)) :
|(integralBasis K).det ((basisOfFractionalIdeal K I).reindex e.symm)| = FractionalIdeal.absNorm I.1 :=
by
rw [← FractionalIdeal.abs_det_basis_change (RingOfIntegers.basis K) I.1 ((fractionalIdealBasis K I.1).reindex e.symm)]
congr
ext
simpa using basisOfFractionalIdeal_apply K I _
