English
Equivalence of adjoin roots of cyclotomic vs. all roots with nth exponent.
Русский
Эквивалентность адъюнкции корней Φ_n и подмножества корней b с b^n = 1.
LaTeX
$$$adjoin A ((cyclotomic n A).rootSet B) = adjoin A \\{ b : B \\mid ∃ a = n, a \\neq 0 ∧ b^a = 1 \\}$$$
Lean4
theorem adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic {n : ℕ} [NeZero n] [IsDomain B] {ζ : B}
(hζ : IsPrimitiveRoot ζ n) : adjoin A ((cyclotomic n A).rootSet B) = adjoin A { ζ } :=
by
refine le_antisymm (adjoin_le fun x hx => ?_) (adjoin_mono fun x hx => ?_)
· suffices hx : x ^ n = 1 by
obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx
exact SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin <| mem_singleton ζ) _)
refine (isRoot_of_unity_iff (NeZero.pos n) B).2 ?_
refine ⟨n, Nat.mem_divisors_self n (NeZero.ne n), ?_⟩
rw [mem_rootSet', aeval_def, ← eval_map, map_cyclotomic, ← IsRoot] at hx
exact hx.2
· simp only [mem_singleton_iff] at hx
simpa only [hx, mem_rootSet', map_cyclotomic, aeval_def, ← eval_map, IsRoot] using
And.intro (cyclotomic_ne_zero n B) (hζ.isRoot_cyclotomic (NeZero.pos n))
