English
The cyclotomic extension is equivalent to the subalgebra generated by all nth roots of unity of orders in S: IsCyclotomicExtension S A C iff C equals adjoin A { x : B | ∃ n ∈ S, x^n = 1 }.
Русский
Циклотомическое расширение эквивалентно подалгебре, порождаемой всеми n-й степенью единиц из S: IsCyclotomicExtension S A C эквивалентно C = adjoin A { x | ∃ n ∈ S, x^n = 1 }.
LaTeX
$$$\\text{IsCyclotomicExtension}(S,A,C) \\iff C = \\operatorname{adjoin}_A\\{\,x:\\; \\exists n\\in S, n\\neq 0 \\land x^n = 1\,\\}$$$
Lean4
theorem isCyclotomicExtension_iff_eq_adjoin (C : Subalgebra A B) (hS : ∀ n ∈ S, n ≠ 0 → ∃ r : B, IsPrimitiveRoot r n) :
IsCyclotomicExtension S A C ↔ C = Algebra.adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} :=
by
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot S A B hS⟩
have := congr_arg (Subalgebra.map C.val) ((IsCyclotomicExtension.iff_adjoin_eq_top _ _ _).mp h).2
rw [← Subalgebra.range_val C, ← Algebra.map_top, ← this, AlgHom.map_adjoin]
congr; ext
simp only [Subalgebra.coe_val, ne_eq, ← Subalgebra.coe_eq_one, SubmonoidClass.coe_pow, Set.mem_image,
Set.mem_setOf_eq, Subtype.exists, exists_and_left, exists_prop, exists_eq_right_right, and_iff_left_iff_imp,
forall_exists_index, and_imp]
exact fun n hn₁ hn₂ hx ↦ h.mem_of_pow_eq_one S C hn₁ hn₂ hx
