English
The extension IsCyclotomicExtension {n} A (CyclotomicRing n A K) holds, i.e. adding nth roots of unity yields a cyclotomic extension of A by the singleton {n}.
Русский
Расширение IsCyclotomicExtension {n} A (CyclotomicRing n A K) означает, что добавление корней n-й степени образует циклотомическое расширение относительно единственного множества {n}.
LaTeX
$$$\\mathrm{IsCyclotomicExtension}\\left(\\{n\\}\\right)\\;A\\;\\operatorname{CyclotomicRing}(n,A,K)$$$
Lean4
instance isCyclotomicExtension [IsFractionRing A K] [NeZero ((n : ℕ) : A)] :
IsCyclotomicExtension { n } A (CyclotomicRing n A K)
where
exists_isPrimitiveRoot {a} han
_ := by
rw [mem_singleton_iff] at han
subst a
have := NeZero.of_faithfulSMul A K n
have := NeZero.of_faithfulSMul A (CyclotomicField n K) n
obtain ⟨μ, hμ⟩ := (CyclotomicField.isCyclotomicExtension n K).exists_isPrimitiveRoot (mem_singleton n) (NeZero.ne n)
refine ⟨⟨μ, subset_adjoin ?_⟩, ?_⟩
· apply (isRoot_of_unity_iff (NeZero.pos n) (CyclotomicField n K)).mpr
refine ⟨n, Nat.mem_divisors_self _ (NeZero.ne n), ?_⟩
rwa [← isRoot_cyclotomic_iff] at hμ
· rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk]
adjoin_roots
x := by
obtain ⟨x, hx⟩ := x
refine adjoin_induction (fun y hy => ?_) (fun a => ?_) (fun y z _ _ hy hz => ?_) (fun y z _ _ hy hz => ?_) hx
· refine subset_adjoin ?_
simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq]
exact ⟨NeZero.ne n, by rwa [← Subalgebra.coe_eq_one, Subalgebra.coe_pow, Subtype.coe_mk]⟩
· exact Subalgebra.algebraMap_mem _ a
· exact Subalgebra.add_mem _ hy hz
· exact Subalgebra.mul_mem _ hy hz
