English
For a number field K, the absolute determinant of the linear map given by the inverse of the FunL-equivalence associated to the complete basis equals finrank_Q(K) times the regulator of K.
Русский
Для числового поля K модулярная прямая линейного отображения, заданная обратной связью equivFunL к полному базису, имеет абсолютное значение детерминанта, равное finrank_Q(K) умножить на регулятор K.
LaTeX
$$$\left|\det\left( (\text{completeBasis}(K).\text{equivFunL}).\text{symm} : \mathbb{R}^{r} \to \mathbb{R}^{r} \right)\right| = \operatorname{finrank}_{\mathbb{Q}} K \cdot \operatorname{regulator}(K)$$$
Lean4
theorem abs_det_completeBasis_equivFunL_symm :
|((completeBasis K).equivFunL.symm : realSpace K →L[ℝ] realSpace K).det| = Module.finrank ℚ K * regulator K := by
classical
rw [ContinuousLinearMap.det, ← LinearMap.det_toMatrix (completeBasis K), ← Matrix.det_transpose,
regulator_eq_regOfFamily_fundSystem, finrank_mul_regOfFamily_eq_det _ w₀ equivFinRank.symm]
congr 2 with w i
rw [Matrix.transpose_apply, LinearMap.toMatrix_apply, Matrix.of_apply, ← Basis.equivFunL_apply,
ContinuousLinearMap.coe_coe, ContinuousLinearEquiv.coe_apply, (completeBasis K).equivFunL.apply_symm_apply]
split_ifs with hw
· rw [hw, completeBasis_apply_of_eq]
· simp_rw [completeBasis_apply_of_ne K ⟨w, hw⟩, expMap_symm_apply, normAtAllPlaces_mixedEmbedding]
