English
Given a family of units and two different infinite places w1, w2, the determinants of two matrices with entries (mult w · log w (u_i)) are equal in absolute value.
Русский
Для пары единиц и двух бесконечных мест w1, w2 детерминанты двух матриц, заполненных (mult w · log w (u_i)), равны по модулю.
LaTeX
$$$|\\det\\big(\\text{Matrix from }(\\mathrm{mult}\\,w \\cdot \\log w(u_i))\\big)| = |\\det\\big(\\text{Matrix from }(\\mathrm{mult}\\,w \\cdot \\log w(u_i))\\big)|$$$
Lean4
/-- A family of units is of maximal rank iff the index of the subgroup it generates has finite index.
-/
theorem isMaxRank_iff_closure_finiteIndex {u : Fin (rank K) → (𝓞 K)ˣ} :
IsMaxRank u ↔ (closure (Set.range u)).FiniteIndex := by
classical
have h₁ :
(closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
Finite
(unitLattice K ⧸ span ℤ (Set.range ((logEmbeddingEquiv K) ∘ Additive.toMul.symm ∘ QuotientGroup.mk ∘ u))) :=
by
change _ ↔ Finite ((unitLattice K).toAddSubgroup ⧸ (span ℤ (Set.range _)).toAddSubgroup)
rw [← AddSubgroup.index_ne_zero_iff_finite]
have := index_map (closure (Set.range u)) (QuotientGroup.mk' (torsion K))
rw [QuotientGroup.ker_mk', QuotientGroup.range_mk', index_top, mul_one] at this
rw [← this, ← index_toAddSubgroup, ← AddSubgroup.index_map_equiv _ (logEmbeddingEquiv K).toAddEquiv, Set.range_comp,
← map_span (logEmbeddingEquiv K), ← map_coe_toLinearMap, map_toAddSubgroup, span_int_eq_addSubgroupClosure,
MonoidHom.map_closure, toAddSubgroup_closure, Set.range_comp, Set.range_comp, QuotientGroup.coe_mk',
Set.preimage_equiv_eq_image_symm]
exact Iff.rfl
have h₂ : DiscreteTopology (span ℤ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i)))) :=
by
refine DiscreteTopology.of_subset (inferInstance : DiscreteTopology (unitLattice K)) ?_
rw [SetLike.coe_subset_coe, Submodule.span_le]
rintro _ ⟨i, rfl⟩
exact ⟨Additive.ofMul (u i), mem_top, rfl⟩
rw [finiteIndex_iff_sup_torsion_finiteIndex, finiteIndex_iff, h₁, finiteQuotient_iff, unitLattice_rank, ← Set.finrank,
IsMaxRank, linearIndependent_iff_card_eq_finrank_span, Real.finrank_eq_int_finrank_of_discrete h₂, Set.finrank,
Set.finrank, ← finrank_map_subtype_eq, map_span, ← Set.range_comp', eq_comm]
simp
