English
For a fixed w' and equivalence e, regOfFamily u equals the absolute determinant of the matrix whose (i,w) entry is log of the embedding of u_i, with a factor depending on i = w'.
Русский
Для фиксированного w' и эквивалентности e регулятор равен модулю детерминанта матрицы, у которой элемент (i,w) равен логарифму вложения u_i, с учётом условия i = w'.
LaTeX
$$$regOfFamily u = \\left|\\det\\left( i,w \\mapsto (mult w) \\cdot \\log(w(u_i)) \\right)\\right|$$$
Lean4
/-- The degree of `K` times the regulator of the family `u` is equal to the absolute value of the
determinant of the matrix whose columns are
`(mult w * log w (fundSystem K i))_i, w` and the column `(mult w)_w`.
-/
theorem finrank_mul_regOfFamily_eq_det (u : Fin (rank K) → (𝓞 K)ˣ) (w' : InfinitePlace K)
(e : { w // w ≠ w' } ≃ Fin (rank K)) :
finrank ℚ K * regOfFamily u =
|(of (fun i w : InfinitePlace K ↦ if h : i = w' then (w.mult : ℝ) else w.mult * (w (u (e ⟨i, h⟩))).log)).det| :=
by
let f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv _).trans ((Equiv.optionSubtype _).symm e.symm).val
let g : { w // w ≠ w' } ≃ Fin (rank K) :=
(Equiv.subtypeEquiv f.symm (fun _ ↦ by simp [f])).trans (finSuccAboveEquiv (f.symm w')).symm
rw [← det_reindex_self f.symm, det_eq_sum_row_mul_submatrix_succAbove_succAbove_det _ (f.symm w') (f.symm w'),
abs_mul, abs_mul, abs_neg_one_pow, one_mul]
· simp_rw [reindex_apply, submatrix_submatrix, ← f.symm.sum_comp, f.symm_symm, submatrix_apply, Function.comp_def,
Equiv.apply_symm_apply, of_apply, dif_pos, ← Nat.cast_sum, sum_mult_eq, Nat.abs_cast]
rw [regOfFamily_eq_det u w' e, ← Matrix.det_reindex_self g]
congr with i j
rw [reindex_apply, submatrix_apply, submatrix_apply, of_apply, of_apply, dif_neg]
rfl
· simp_rw [Equiv.forall_congr_left f, ← f.symm.sum_comp, reindex_apply, submatrix_apply, of_apply, f.symm_symm,
f.apply_symm_apply, Finset.sum_dite_irrel, ne_eq, EmbeddingLike.apply_eq_iff_eq]
intro _ h
rw [dif_neg h, sum_mult_mul_log]
