English
For primitive root ζ of order n, the adjunction of the cyclotomic rootSet equals the adjunction of {ζ}.
Русский
Пусть ζ — примитивный корень порядка n; адъюнкция множества корней Φ_n равна адъюнкции {ζ}.
LaTeX
$$$IsPrimitiveRoot(\\ζ,n) \\Rightarrow Algebra.adjoin A ((Φ_n(A)).rootSet B) = Algebra.adjoin A\\{\\zeta\\}$$$
Lean4
theorem adjoin_roots_cyclotomic_eq_adjoin_nth_roots [IsDomain B] {ζ : B} {n : ℕ} [NeZero n] (hζ : IsPrimitiveRoot ζ n) :
adjoin A ((cyclotomic n A).rootSet B) = adjoin A {b : B | ∃ a : ℕ, a ∈ ({ n } : Set ℕ) ∧ a ≠ 0 ∧ b ^ a = 1} :=
by
simp only [mem_singleton_iff, exists_eq_left]
refine le_antisymm (adjoin_mono fun x hx => ?_) (adjoin_le fun x hx => ?_)
· rw [mem_rootSet'] at hx
simp only [mem_setOf_eq]
rw [isRoot_of_unity_iff (NeZero.pos n)]
refine ⟨NeZero.ne n, n, Nat.mem_divisors_self n (NeZero.ne n), ?_⟩
rw [IsRoot.def, ← map_cyclotomic n (algebraMap A B), eval_map, ← aeval_def]
exact hx.2
· simp only [mem_setOf_eq] at hx
obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx.2
refine SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin ?_) _)
rw [mem_rootSet', map_cyclotomic, aeval_def, ← eval_map, map_cyclotomic, ← IsRoot]
exact ⟨cyclotomic_ne_zero n B, hζ.isRoot_cyclotomic (NeZero.pos n)⟩
