English
There exists a fundamental system of units of K, a coherent family of units corresponding to each rank position, lifting a basis modulo torsion.
Русский
Существует фундаментальная система единиц поля K, соответствующая каждому порядку и являющаяся подъемом базиса модуляtorsion.
LaTeX
$$$\text{basisModTorsion} : \text{Basis}_{\mathbb{Z}}(\text{Fin}(\mathrm{rank}\,K))\; (\text{Additive}((\mathcal{O}_K)^×/\mathrm{torsion}))$$$
Lean4
theorem unitLattice_span_eq_top : Submodule.span ℝ (unitLattice K : Set (logSpace K)) = ⊤ := by
classical
refine
le_antisymm le_top
?_
-- The standard basis
let B :=
Pi.basisFun ℝ
{ w : InfinitePlace K // w ≠ w₀ }
-- The image by log_embedding of the family of units constructed above
let v := fun w : { w : InfinitePlace K // w ≠ w₀ } ↦
logEmbedding K
(Additive.ofMul (exists_unit K w).choose)
-- To prove the result, it is enough to prove that the family `v` is linearly independent
suffices B.det v ≠ 0 by
rw [← isUnit_iff_ne_zero, ← Basis.is_basis_iff_det] at this
rw [← this.2]
refine Submodule.span_monotone fun _ ⟨w, hw⟩ ↦ ⟨(exists_unit K w).choose, trivial, hw⟩
rw [Basis.det_apply]
-- We use a specific lemma to prove that this determinant is nonzero
refine det_ne_zero_of_sum_col_lt_diag (fun w ↦ ?_)
simp_rw [Real.norm_eq_abs, B, Basis.coePiBasisFun.toMatrix_eq_transpose, Matrix.transpose_apply]
rw [← sub_pos, sum_congr rfl (fun x hx ↦ abs_of_neg ?_), sum_neg_distrib, sub_neg_eq_add,
sum_erase_eq_sub (mem_univ _), ← add_comm_sub]
· refine add_pos_of_nonneg_of_pos ?_ ?_
· rw [sub_nonneg]
exact le_abs_self _
· rw [sum_logEmbedding_component (exists_unit K w).choose]
refine mul_pos_of_neg_of_neg ?_ ((exists_unit K w).choose_spec _ w.prop.symm)
rw [mult]; split_ifs <;> norm_num
· refine mul_neg_of_pos_of_neg ?_ ((exists_unit K w).choose_spec x ?_)
· rw [mult]; split_ifs <;> norm_num
· exact Subtype.ext_iff.not.mp (ne_of_mem_erase hx)
