unit_smul_mem_iff_mem_torsion — Mathlib

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

Похожие утверждения