English
The determinant of the fractional ideal basis equals the absolute norm of I.
Русский
Определитель базы дробного идеала равен абсолютной норме I.
LaTeX
$$$ |Basis.det (latticeBasis K) ((mixedEmbedding K) (basisOfFractionalIdeal K I) \circ e)| = FractionalIdeal.absNorm I.1 $$$
Lean4
/-- A `ℝ`-basis of the mixed space of `K` that is also a `ℤ`-basis of the image of the fractional
ideal `I`. -/
def fractionalIdealLatticeBasis : Basis (ChooseBasisIndex ℤ I) ℝ (mixedSpace K) :=
by
let e : (ChooseBasisIndex ℤ (𝓞 K)) ≃ (ChooseBasisIndex ℤ I) :=
by
refine Fintype.equivOfCardEq ?_
rw [← finrank_eq_card_chooseBasisIndex, ← finrank_eq_card_chooseBasisIndex, fractionalIdeal_rank]
refine Basis.reindex ?_ e
suffices IsUnit ((latticeBasis K).det ((mixedEmbedding K) ∘ (basisOfFractionalIdeal K I) ∘ e))
by
rw [← Basis.is_basis_iff_det] at this
exact Basis.mk this.1 (by rw [this.2])
rw [isUnit_iff_ne_zero, ne_eq, ← abs_eq_zero.not, det_basisOfFractionalIdeal_eq_norm, Rat.cast_eq_zero,
FractionalIdeal.absNorm_eq_zero_iff]
exact Units.ne_zero I
