English
If L1 ≤ L2 are sublattices, then the ratio of covolumes equals the sublattice index: covolume(L1)/covolume(L2) = relIndex(L1,L2).
Русский
Пусть L1 ≤ L2 — подрешетки; тогда отношение коволюмов равно относительному индексу: covolume(L1)/covolume(L2) = relIndex(L1,L2).
LaTeX
$$$\\dfrac{\\operatorname{covolume}(L_1,\\mu)}{\\operatorname{covolume}(L_2,\\mu)} = \\operatorname{relIndex}\\big(L_1^{\\,+}, L_2^{\\,+}\\big)$$$
Lean4
/-- Let `L₁` be a sub-`ℤ`-lattice of `L₂`. Then the index of `L₁` inside `L₂` is equal to
`covolume L₁ / covolume L₂`.
-/
theorem covolume_div_covolume_eq_relIndex {ι : Type*} [Fintype ι] (L₁ L₂ : Submodule ℤ (ι → ℝ)) [DiscreteTopology L₁]
[IsZLattice ℝ L₁] [DiscreteTopology L₂] [IsZLattice ℝ L₂] (h : L₁ ≤ L₂) :
covolume L₁ / covolume L₂ = L₁.toAddSubgroup.relIndex L₂.toAddSubgroup := by
classical
let b₁ := IsZLattice.basis L₁
let b₂ := IsZLattice.basis L₂
rw [AddSubgroup.relIndex_eq_natAbs_det L₁.toAddSubgroup L₂.toAddSubgroup h b₁ b₂, Nat.cast_natAbs, Int.cast_abs]
trans |(b₂.ofZLatticeBasis ℝ).det (b₁.ofZLatticeBasis ℝ)|
· rw [← Basis.det_mul_det _ (Pi.basisFun ℝ ι) _, abs_mul, Pi.basisFun_det_apply, ← Basis.det_inv,
Units.val_inv_eq_inv_val, IsUnit.unit_spec, Pi.basisFun_det_apply, covolume_eq_det _ b₁, covolume_eq_det _ b₂,
mul_comm, abs_inv]
congr 3 <;> ext <;> simp
· rw [Basis.det_apply, Basis.det_apply, Int.cast_det]
congr; ext i j
rw [Matrix.map_apply, Basis.toMatrix_apply, Basis.toMatrix_apply, Basis.ofZLatticeBasis_apply]
exact (b₂.ofZLatticeBasis_repr_apply ℝ L₂ ⟨b₁ j, h (coe_mem _)⟩ i)
