English
For hx and a unit u, u·x ∈ fundamentalCone(K) iff u is torsion in the unit group.
Русский
Для hx и единицы u условие u·x ∈ fundamentalCone(K) эквивалентно тому, что u имеет тривиальную торию в группе единиц.
LaTeX
$$(hx : x ∈ fundamentalCone(K)) (u : Units(RingOfIntegers K)) : (u·x ∈ fundamentalCone(K) \iff u ∈ torsion K).$$
Lean4
theorem unit_smul_mem_iff_mem_torsion (hx : x ∈ fundamentalCone K) (u : (𝓞 K)ˣ) :
u • x ∈ fundamentalCone K ↔ u ∈ torsion K := by
classical
refine ⟨fun h ↦ ?_, fun h ↦ torsion_smul_mem_of_mem hx h⟩
rw [← logEmbedding_eq_zero_iff]
let B := (basisUnitLattice K).ofZLatticeBasis ℝ
refine
(Subtype.mk_eq_mk (h := ?_) (h' := Submodule.zero_mem _)).mp <|
(ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)).unique ?_ ?_
· rw [Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]
exact ⟨u, trivial, rfl⟩
· rw [AddSubmonoid.mk_vadd, vadd_eq_add, ← logMap_unit_smul _ hx.2]
exact h.1
· rw [AddSubmonoid.mk_vadd, vadd_eq_add, zero_add]
exact hx.1