English
For a CM-field K, the regulator of the real fundamental system equals 2^rank(K) times the regulator of the maximal real subfield K^+; i.e., regOfFamily(realFundSystem(K)) = 2^{rank K} · regulator(K^+).
Русский
Для поля CM K регулятор реальной фундаментальной системы равен 2^{rank K} умножить на регулятор максимального действительного подполя K^+; то есть regOfFamily(realFundSystem(K)) = 2^{rank K} · regulator(K^+).
LaTeX
$$$\\mathrm{regOfFamily}(\\mathrm{realFundSystem}(K)) = 2^{\\mathrm{rank}}(K) \\cdot \\mathrm{regulator}(K^+)$$$
Lean4
theorem regOfFamily_realFunSystem : regOfFamily (realFundSystem K) = 2 ^ rank K * regulator K⁺ := by
classical
let W₀ := (equivInfinitePlace K).symm w₀
let f : { w : InfinitePlace K // w ≠ W₀ } ≃ { w : InfinitePlace K⁺ // w ≠ w₀ } :=
(equivInfinitePlace K).subtypeEquiv fun w ↦ by rw [not_iff_not, Equiv.eq_symm_apply]
let g := ((finCongr (units_rank_eq_units_rank K).symm).trans (equivFinRank K⁺)).trans f.symm
rw [show (2 : ℝ) ^ rank K = |∏ w : { w : InfinitePlace K⁺ // w ≠ w₀ }, 2|
by
rw [Finset.prod_const, abs_pow, abs_of_pos zero_lt_two, ← units_rank_eq_units_rank K, rank]
simp]
rw [regulator_eq_regOfFamily_fundSystem, regOfFamily_eq_det _ W₀ g.symm, regOfFamily_eq_det', ← abs_mul, ←
Matrix.det_mul_column, ← Matrix.det_reindex_self f, Matrix.reindex_apply]
congr; ext i w
rw [Matrix.submatrix_apply, Matrix.of_apply, Matrix.of_apply, show f.symm w = (equivInfinitePlace K).symm w.1 by rfl,
show algebraMap (𝓞 K) K _ = algebraMap K⁺ K _ by rfl, equivInfinitePlace_symm_apply]
simp [f, g]
