English
Let x be a unit in the ring of integers of K, written uniquely as a root of unity ζ times a product of powers of the fundamental units: x = ζ · ∏i (fundSystem K i)^{fi}, with ζ torsion. Then the vector f = (fi) is precisely the coordinate representation of the additive image of x with respect to the torsion-free basis basisModTorsion.
Русский
Пусть x — единица в кольце целых чисел K, представимая единственным образом как ζ · ∏i (fundSystem K i)^{fi}, где ζ — корень единства (torsion). Тогда вектор f = (fi) есть координатное представление изображения x по отношению к базису без torsion, basisModTorsion.
LaTeX
$$$\\forall K [Field K] [NumberField K], \\forall x \\in (\\mathcal{O}_K)^{\\times}, \\forall \\zeta \\in \\mathrm{torsion}(K), \\forall f : \\mathrm{Fin}(\\mathrm{rank}\\,K) \\to \\mathbb{Z},\\; (\\zeta \\in \\mathrm{torsion}(K) \\land x = \\zeta \\cdot \\prod_i (\\mathrm{fundSystem}~K~i)^{f(i)}) \\Rightarrow f = (\\mathrm{basisModTorsion}~K).repr(\\mathrm{Additive.ofMul}(x)).$$$
Lean4
/-- The exponents that appear in the unique decomposition of a unit as the product of
a root of unity and powers of the units of the fundamental system `fundSystem` (see
`exist_unique_eq_mul_prod`) are given by the representation of the unit on `basisModTorsion`. -/
theorem fun_eq_repr {x ζ : (𝓞 K)ˣ} {f : Fin (rank K) → ℤ} (hζ : ζ ∈ torsion K)
(h : x = ζ * ∏ i, (fundSystem K i) ^ (f i)) : f = (basisModTorsion K).repr (Additive.ofMul ↑x) :=
by
suffices Additive.ofMul ↑x = ∑ i, (f i) • (basisModTorsion K i) by rw [← (basisModTorsion K).repr_sum_self f, ← this]
calc
Additive.ofMul ↑x
_ = ∑ i, (f i) • Additive.ofMul ↑(fundSystem K i) := by
rw [h, QuotientGroup.mk_mul, (QuotientGroup.eq_one_iff _).mpr hζ, one_mul, QuotientGroup.mk_prod, ofMul_prod]; rfl
_ = ∑ i, (f i) • (basisModTorsion K i) := by simp_rw [fundSystem, QuotientGroup.out_eq', ofMul_toMul]
