English
Let u be a unit in the ring of integers of a cubic cyclotomic extension. Then u lies among the six roots of unity: 1, -1, η, -η, η^2, -η^2.
Русский
Пусть u — единица в кольце целых в кубической циклотомической расширении. Тогда u принадлежит шести корням единицы: 1, -1, η, -η, η^2, -η^2.
LaTeX
$$$u \in \{1, -1, \eta, -\eta, \eta^{2}, -\eta^{2}\}$$$
Lean4
/-- Let `u` be a unit in `(𝓞 K)ˣ`, then `u ∈ [1, -1, η, -η, η^2, -η^2]`. -/
-- Here `List` is more convenient than `Finset`, even if further from the informal statement.
-- For example, `fin_cases` below does not work with a `Finset`.
theorem mem [NumberField K] [IsCyclotomicExtension { 3 } ℚ K] : u ∈ [1, -1, η, -η, η ^ 2, -η ^ 2] :=
by
have hrank : rank K = 0 := by
dsimp only [rank]
rw [card_eq_nrRealPlaces_add_nrComplexPlaces, nrRealPlaces_eq_zero (n := 3) K (by decide), zero_add,
nrComplexPlaces_eq_totient_div_two (n := 3)]
rfl
obtain ⟨⟨x, e⟩, hxu, -⟩ := exist_unique_eq_mul_prod _ u
replace hxu : u = x := by
rw [← mul_one x.1, hxu]
apply congr_arg
rw [← Finset.prod_empty]
congr
rw [Finset.univ_eq_empty_iff, hrank]
infer_instance
obtain ⟨n, hnpos, hn⟩ := isOfFinOrder_iff_pow_eq_one.1 <| (CommGroup.mem_torsion _ _).1 x.2
replace hn : (↑u : K) ^ ((⟨n, hnpos⟩ : ℕ+) : ℕ) = 1 :=
by
rw [← map_pow]
convert map_one (algebraMap (𝓞 K) K)
rw_mod_cast [hxu, hn]
simp
obtain ⟨r, hr3, hru⟩ :=
hζ.exists_pow_or_neg_mul_pow_of_isOfFinOrder (by decide) (isOfFinOrder_iff_pow_eq_one.2 ⟨n, hnpos, hn⟩)
replace hr : r ∈ Finset.Ico 0 3 := Finset.mem_Ico.2 ⟨by simp, hr3⟩
replace hru : ↑u = η ^ r ∨ ↑u = -η ^ r := by
rcases hru with h | h
· left; ext; exact h
· right; ext; exact h
fin_cases hr <;> rcases hru with h | h <;> simp [h]
