English
In a cyclic Galois finite extension L/K with a primitive nth root of unity in K, there exists α ∈ L with α^finrank(K,L) ∈ range(algebraMap(K,L)) and K⟮α⟯ = L.
Русский
В циклическом Галуа конечном расширении L/K существует α ∈ L с α^{finrank(K,L)} ∈ диапазон алгебраического отображения и K⟮α⟯ = L.
LaTeX
$$$\exists α\in L:\ α^{\mathrm{finrank}(K,L)} \in \mathrm{range}(\mathrm{algebraMap}_{K,L}) \wedge K⟮α⟯ = ⊤.$$$
Lean4
/-- If `L/K` is a cyclic extension of degree `n`, and `K` contains all `n`-th roots of unity,
then `L = K[α]` for some `α ^ n ∈ K`. -/
theorem exists_root_adjoin_eq_top_of_isCyclic [IsGalois K L] [IsCyclic (L ≃ₐ[K] L)] :
∃ (α : L), α ^ (finrank K L) ∈ Set.range (algebraMap K L) ∧ K⟮α⟯ = ⊤ := by
-- Let `ζ` be an `n`-th root of unity, and `σ` be a generator of `L ≃ₐ[K] L`.
have ⟨ζ, hζ⟩ := hK
rw [mem_primitiveRoots finrank_pos] at hζ
obtain ⟨σ, hσ⟩ := ‹IsCyclic (L ≃ₐ[K] L)›
have hσ' := orderOf_eq_card_of_forall_mem_zpowers hσ
have : IsRoot (minpoly K σ.toLinearMap) ζ :=
by
rw [IsGalois.card_aut_eq_finrank] at hσ'
simpa [minpoly_algEquiv_toLinearMap σ (isOfFinOrder_of_finite σ), hσ', sub_eq_zero] using hζ.pow_eq_one
obtain ⟨v, hv⟩ := (Module.End.hasEigenvalue_of_isRoot this).exists_hasEigenvector
have hv' := hv.pow_apply
simp_rw [← AlgEquiv.pow_toLinearMap, AlgEquiv.toLinearMap_apply] at hv'
refine ⟨v, ?_, ?_⟩
· -- Since `v ^ n` is fixed by `σ` (`σ (v ^ n) = ζ ^ n • v ^ n = v ^ n`), it is in `K`.
rw [← IntermediateField.mem_bot, ← OrderIso.map_bot IsGalois.intermediateFieldEquivSubgroup.symm]
intro ⟨σ', hσ'⟩
obtain ⟨n, rfl : σ ^ n = σ'⟩ := mem_powers_iff_mem_zpowers.mpr (hσ σ')
rw [smul_pow', Submonoid.smul_def, AlgEquiv.smul_def, hv', smul_pow, ← pow_mul, mul_comm, pow_mul, hζ.pow_eq_one,
one_pow, one_smul]
· -- Since `σ` does not fix `K⟮α⟯`, `K⟮α⟯` is `L`.
apply IsGalois.intermediateFieldEquivSubgroup.injective
rw [map_top, eq_top_iff]
intro σ' hσ'
obtain ⟨n, rfl : σ ^ n = σ'⟩ := mem_powers_iff_mem_zpowers.mpr (hσ σ')
have := hσ' ⟨v, IntermediateField.mem_adjoin_simple_self K v⟩
simp only [AlgEquiv.smul_def, hv'] at this
conv_rhs at this => rw [← one_smul K v]
obtain ⟨k, rfl⟩ := hζ.dvd_of_pow_eq_one n (smul_left_injective K hv.2 this)
rw [pow_mul, ← IsGalois.card_aut_eq_finrank, pow_card_eq_one', one_pow]
exact one_mem _
