English
Let K be a p^k-th cyclotomic extension of Q and ζ a primitive p^k-th root of unity in K. Then the integral closure of Z in K is the Z-algebra generated by ζ; i.e., 𝒪_K = Z[ζ].
Русский
Пусть K — p^k-ое циклотомическое расширение Q и ζ — примитивный корень ζ^{p^k} в K. Тогда целочисленное замыкание Z в K равно Z[ζ].
LaTeX
$$$\operatorname{IsIntegralClosure}(\operatorname{adjoin}_{\mathbb{Z}} (\{\zeta\}\,), \mathbb{Z}, K)$$$
Lean4
/-- If `K` is a `p ^ k`-th cyclotomic extension of `ℚ`, then `(adjoin ℤ {ζ})` is the
integral closure of `ℤ` in `K`. -/
theorem isIntegralClosure_adjoin_singleton_of_prime_pow [hcycl : IsCyclotomicExtension {p ^ k} ℚ K]
(hζ : IsPrimitiveRoot ζ (p ^ k)) : IsIntegralClosure (adjoin ℤ ({ ζ } : Set K)) ℤ K :=
by
refine ⟨Subtype.val_injective, @fun x => ⟨fun h => ⟨⟨x, ?_⟩, rfl⟩, ?_⟩⟩
swap
· rintro ⟨y, rfl⟩
exact
IsIntegral.algebraMap
((le_integralClosure_iff_isIntegral.1 (adjoin_le_integralClosure (hζ.isIntegral (NeZero.pos _)))).isIntegral _)
let B := hζ.subOnePowerBasis ℚ
have hint : IsIntegral ℤ B.gen := (hζ.isIntegral (NeZero.pos _)).sub isIntegral_one
letI := IsCyclotomicExtension.finiteDimensional {p ^ k} ℚ K
have H := discr_mul_isIntegral_mem_adjoin ℚ hint h
obtain ⟨u, n, hun⟩ := discr_prime_pow_eq_unit_mul_pow' hζ
rw [hun] at H
replace H := Subalgebra.smul_mem _ H u.inv
rw [← smul_assoc, ← smul_mul_assoc, Units.inv_eq_val_inv, zsmul_eq_mul, ← Int.cast_mul, Units.inv_mul, Int.cast_one,
one_mul, smul_def, map_pow] at H
cases k
· haveI : IsCyclotomicExtension { 1 } ℚ K := by simpa using hcycl
have : x ∈ (⊥ : Subalgebra ℚ K) := by
rw [singleton_one ℚ K]
exact mem_top
obtain ⟨y, rfl⟩ := mem_bot.1 this
replace h := (isIntegral_algebraMap_iff (algebraMap ℚ K).injective).1 h
obtain ⟨z, hz⟩ := IsIntegrallyClosed.isIntegral_iff.1 h
rw [← hz, ← IsScalarTower.algebraMap_apply]
exact Subalgebra.algebraMap_mem _ _
· have hmin : (minpoly ℤ B.gen).IsEisensteinAt (Submodule.span ℤ {(p : ℤ)}) :=
by
have h₁ := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hint
have h₂ := hζ.minpoly_sub_one_eq_cyclotomic_comp (cyclotomic.irreducible_rat (NeZero.pos _))
rw [IsPrimitiveRoot.subOnePowerBasis_gen] at h₁
rw [h₁, ← map_cyclotomic_int, show Int.castRingHom ℚ = algebraMap ℤ ℚ by rfl,
show X + 1 = map (algebraMap ℤ ℚ) (X + 1) by simp, ← map_comp] at h₂
rw [IsPrimitiveRoot.subOnePowerBasis_gen, map_injective (algebraMap ℤ ℚ) (algebraMap ℤ ℚ).injective_int h₂]
exact cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt p _
refine
adjoin_le ?_
(mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt (n := n) (Nat.prime_iff_prime_int.1 hp.out) hint h
(by simpa using H) hmin)
simp only [Set.singleton_subset_iff, SetLike.mem_coe]
exact Subalgebra.sub_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _)
