English
The determinant of the lattice basis equals the norm of the fractional ideal.
Русский
Определитель базиса решётки равен норме дробного идеала.
LaTeX
$$$ |\text{Basis.det} (latticeBasis K) ((mixedEmbedding K) \circ (basisOfFractionalIdeal K I) \circ e)| = \ FractionalIdeal.absNorm I.1 $$$
Lean4
/-- The generalized index of the lattice generated by `I` in the lattice generated by
`𝓞 K` is equal to the norm of the ideal `I`. The result is stated in terms of base change
determinant and is the translation of `NumberField.det_basisOfFractionalIdeal_eq_absNorm` in
the mixed space. This is useful, in particular, to prove that the family obtained from
the `ℤ`-basis of `I` is actually an `ℝ`-basis of the mixed space, see
`fractionalIdealLatticeBasis`. -/
theorem det_basisOfFractionalIdeal_eq_norm (e : (ChooseBasisIndex ℤ (𝓞 K)) ≃ (ChooseBasisIndex ℤ I)) :
|Basis.det (latticeBasis K) ((mixedEmbedding K ∘ (basisOfFractionalIdeal K I) ∘ e))| =
FractionalIdeal.absNorm I.1 :=
by
suffices
Basis.det (latticeBasis K) ((mixedEmbedding K ∘ (basisOfFractionalIdeal K I) ∘ e)) =
(algebraMap ℚ ℝ) ((Basis.det (integralBasis K)) ((basisOfFractionalIdeal K I) ∘ e))
by
rw [this, eq_ratCast, ← Rat.cast_abs, ← Equiv.symm_symm e, ← Basis.coe_reindex,
det_basisOfFractionalIdeal_eq_absNorm K I e]
rw [Basis.det_apply, Basis.det_apply, RingHom.map_det]
congr
ext i j
simp_rw [RingHom.mapMatrix_apply, Matrix.map_apply, Basis.toMatrix_apply, Function.comp_apply]
exact latticeBasis_repr_apply K _ i
