English
If μ is a primitive n-th root of unity in CyclotomicField n K, then the cyclotomic ring is generated by μ together with the base A; i.e. CyclotomicRing n A K = adjoin A {μ}.
Русский
Пусть μ — примитивный корень век n-й степени в CyclotomicField n K; тогда циклотомическое кольцо порождается μ вместе с A: CyclotomicRing n A K = adjoin A {μ}.
LaTeX
$$$\\operatorname{CyclotomicRing}(n,A,K) = \\operatorname{adjoin}_A\\{\\mu\\}$$$
Lean4
instance [IsFractionRing A K] [IsDomain A] [NeZero (n : A)] :
IsFractionRing (CyclotomicRing n A K) (CyclotomicField n K)
where
map_units := fun ⟨x, hx⟩ => by
rw [isUnit_iff_ne_zero]
apply map_ne_zero_of_mem_nonZeroDivisors
· apply adjoin_algebra_injective
· exact hx
surj
x := by
have : NeZero (n : K) := NeZero.nat_of_injective (IsFractionRing.injective A K)
refine
Algebra.adjoin_induction (hx :=
((IsCyclotomicExtension.iff_singleton n K (CyclotomicField n K)).1
(CyclotomicField.isCyclotomicExtension n K)).2
x)
(fun y hy => ?_) (fun k => ?_) ?_ ?_
· exact ⟨⟨⟨y, subset_adjoin hy⟩, 1⟩, by simp; rfl⟩
· have : IsLocalization (nonZeroDivisors A) K := inferInstance
replace := this.surj
obtain ⟨⟨z, w⟩, hw⟩ := this k
refine
⟨⟨algebraMap A (CyclotomicRing n A K) z, algebraMap A (CyclotomicRing n A K) w,
map_mem_nonZeroDivisors _ (algebraBase_injective n A K) w.2⟩,
?_⟩
letI : IsScalarTower A K (CyclotomicField n K) := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
@IsScalarTower.algebraMap_apply A K _ _ _ _ _ (_root_.CyclotomicField.algebra n K) _ _ w, ← RingHom.map_mul, hw,
← IsScalarTower.algebraMap_apply]
· rintro y z - - ⟨a, ha⟩ ⟨b, hb⟩
refine ⟨⟨a.1 * b.2 + b.1 * a.2, a.2 * b.2, mul_mem_nonZeroDivisors.2 ⟨a.2.2, b.2.2⟩⟩, ?_⟩
rw [RingHom.map_mul, add_mul, ← mul_assoc, ha, mul_comm ((algebraMap (CyclotomicRing n A K) _) ↑a.2), ← mul_assoc,
hb]
simp only [map_add, map_mul]
· rintro y z - - ⟨a, ha⟩ ⟨b, hb⟩
refine ⟨⟨a.1 * b.1, a.2 * b.2, mul_mem_nonZeroDivisors.2 ⟨a.2.2, b.2.2⟩⟩, ?_⟩
rw [RingHom.map_mul, mul_comm ((algebraMap (CyclotomicRing n A K) _) ↑a.2), mul_assoc, ← mul_assoc z, hb, ←
mul_comm ((algebraMap (CyclotomicRing n A K) _) ↑a.2), ← mul_assoc, ha]
simp only [map_mul]
exists_of_eq {x y} h := ⟨1, by rw [adjoin_algebra_injective n A K h]⟩
