English
The volume of the fundamental domain associated to a fractional ideal lattice equals a scaled volume of the lattice domain.
Русский
Объем фундаментального домена, связанного с фракционным идеалом-решеткой, равен масштабированному объему решетки.
LaTeX
$$$\operatorname{volume}(\text{fundamentalDomain}(\text{fractionalIdealLatticeBasis } K I)) = .\!\text{ofReal}(\text{absNorm}(I)) \cdot \operatorname{volume}(\text{fundamentalDomain}(\text{latticeBasis } K)).$$$
Lean4
theorem volume_fundamentalDomain_fractionalIdealLatticeBasis :
volume (fundamentalDomain (fractionalIdealLatticeBasis K I)) =
.ofReal (FractionalIdeal.absNorm I.1) * volume (fundamentalDomain (latticeBasis K)) :=
by
let e : (Module.Free.ChooseBasisIndex ℤ I) ≃ (Module.Free.ChooseBasisIndex ℤ (𝓞 K)) :=
by
refine Fintype.equivOfCardEq ?_
rw [← finrank_eq_card_chooseBasisIndex, ← finrank_eq_card_chooseBasisIndex, fractionalIdeal_rank]
rw [← fundamentalDomain_reindex (fractionalIdealLatticeBasis K I) e,
measure_fundamentalDomain ((fractionalIdealLatticeBasis K I).reindex e)]
· rw [show (fractionalIdealLatticeBasis K I).reindex e = (mixedEmbedding K) ∘ (basisOfFractionalIdeal K I) ∘ e.symm by
ext1; simp only [Basis.coe_reindex, Function.comp_apply, fractionalIdealLatticeBasis_apply]]
rw [mixedEmbedding.det_basisOfFractionalIdeal_eq_norm]
