English
There exists a canonical algebra isomorphism between the ℤ-adjoin of {ζ} and the ring of integers 𝓞_K in a cyclotomic extension, respecting the primitive root structure.
Русский
Существует каноническое алгебраическое изоморфизм между ℤ-объединением {ζ} и кольцом целых 𝓞_K в циклотомическом расширении, сохраняющий структуру примитивного корня.
LaTeX
$$$$ \text{IsPrimitiveRoot}.adjoinEquivRingOfIntegers' (\text{…}) : \text{adjoin } \mathbb{Z}({\zeta}) \cong \mathcal{O}_K $$$$
Lean4
@[simp]
theorem integralPowerBasis_gen [hcycl : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) :
hζ.integralPowerBasis.gen = hζ.toInteger :=
Subtype.ext <|
show algebraMap _ K hζ.integralPowerBasis.gen = _
by
rw [integralPowerBasis, PowerBasis.map_gen, adjoin.powerBasis'_gen]
simp only [adjoinEquivRingOfIntegers_apply, IsIntegralClosure.algebraMap_lift]
rfl
/- We name `hcycl` so it can be used as a named argument, but this is unused in the declaration
otherwise, so we need to disable the linter. -/
