English
The integral closure of the cyclotomic ring inside the cyclotomic field is the cyclotomic field’s ring of integers, i.e., 𝒪_{K} is generated by the standard cyclotomic ring over Z.
Русский
Целочисленное замыкание кольца циклотомии внутри циклотомического поля равно кольцу целых числа поля, т.е. 𝒪_K порождается кольцом циклотомии над Z.
LaTeX
$$$\operatorname{IsIntegralClosure}(\operatorname{CyclotomicRing}(p^k)\, \mathbb{Z}, \mathbb{Q}, \mathit{CyclotomicField}(p^k))$$$
Lean4
/-- The integral closure of `ℤ` inside `CyclotomicField (p ^ k) ℚ` is
`CyclotomicRing (p ^ k) ℤ ℚ`. -/
theorem cyclotomicRing_isIntegralClosure_of_prime_pow :
IsIntegralClosure (CyclotomicRing (p ^ k) ℤ ℚ) ℤ (CyclotomicField (p ^ k) ℚ) :=
by
have hζ := zeta_spec (p ^ k) ℚ (CyclotomicField (p ^ k) ℚ)
refine ⟨IsFractionRing.injective _ _, @fun x => ⟨fun h => ⟨⟨x, ?_⟩, rfl⟩, ?_⟩⟩
· obtain ⟨y, rfl⟩ := (isIntegralClosure_adjoin_singleton_of_prime_pow hζ).isIntegral_iff.1 h
refine adjoin_mono ?_ y.2
simp only [Set.singleton_subset_iff, Set.mem_setOf_eq]
exact hζ.pow_eq_one
· rintro ⟨y, rfl⟩
exact IsIntegral.algebraMap ((IsCyclotomicExtension.integral {p ^ k} ℤ _).isIntegral _)
