English
A refined determinant formula expresses finrank(K) times regOfFamily u as the determinant of a matrix whose entries depend on whether i equals w' and involve logs of embeddings.
Русский
Уточнённая формула детерминанта выражает произведение ранг K на regOfFamily(u) как детерминант матрицы со степенными зависимостями от i относительно w' и логарифмов вложений.
LaTeX
$$$\\mathrm{finrank}\\;K \\cdot regOfFamily u = \\left|\\det( f(i,w) )\\right|, \\text{ где } f(i,w) = \\begin{cases} w.mult^{\\,cast} & \\text{если } i = w' \\\\ w.mult^{\\,cast} \\cdot \\log w(u_i) & \\text{иначе} \\end{cases}$$$
Lean4
/-- Let `u : Fin (rank K) → (𝓞 K)ˣ` be a family of units and let `w₁` and `w₂` be two infinite
places. Then, the two square matrices with entries `(mult w * log w (u i))_i` where `w ≠ w_j` for
`j = 1, 2` have the same determinant in absolute value.
-/
theorem abs_det_eq_abs_det (u : Fin (rank K) → (𝓞 K)ˣ) {w₁ w₂ : InfinitePlace K} (e₁ : { w // w ≠ w₁ } ≃ Fin (rank K))
(e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)) :
|(of fun i w : { w // w ≠ w₁ } ↦ (mult w.val : ℝ) * (w.val (u (e₁ i) : K)).log).det| =
|(of fun i w : { w // w ≠ w₂ } ↦ (mult w.val : ℝ) * (w.val (u (e₂ i) : K)).log).det| :=
by
-- We construct an equiv `Fin (rank K + 1) ≃ InfinitePlace K` from `e₂.symm`
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
have h_col :=
congr_arg abs <|
det_permute (g.trans e₂.symm) (of fun i w : { w // w ≠ w₂ } ↦ (mult w.val : ℝ) * (w.val (u (e₂ i) : K)).log)
rw [abs_mul, ← Int.cast_abs, Equiv.Perm.sign_abs, Int.cast_one, one_mul] at h_col
rw [← h_col]
have h :=
congr_arg abs <|
submatrix_succAbove_det_eq_negOnePow_submatrix_succAbove_det' (of fun i w ↦ (mult (f w) : ℝ) * ((f w) (u i)).log)
?_ 0 (f.symm w₂)
· rw [← det_reindex_self e₁, ← det_reindex_self g]
· rw [Units.smul_def, abs_zsmul, Int.abs_negOnePow, one_smul] at h
convert h
· ext;
simp only [ne_eq, reindex_apply, submatrix_apply, of_apply, Equiv.apply_symm_apply, Equiv.trans_apply,
Fin.succAbove_zero, id_eq, finSuccEquiv_succ, Equiv.optionSubtype_symm_apply_apply_coe, f]
· ext;
simp only [ne_eq, Equiv.coe_trans, reindex_apply, submatrix_apply, Function.comp_apply, Equiv.apply_symm_apply,
id_eq, of_apply];
rfl
· intro _
simp_rw [of_apply, ← Real.log_pow]
rw [← Real.log_prod, Equiv.prod_comp f (fun w ↦ (w (u _) ^ (mult w))), prod_eq_abs_norm, Units.norm, Rat.cast_one,
Real.log_one]
exact fun _ _ ↦ pow_ne_zero _ <| (map_ne_zero _).mpr (coe_ne_zero _)
