English
In a finite dimensional setting with all nth roots in K, being Galois and cyclic, existence of a specific irreducible polynomial and a root adjoin property are all equivalent (TFAE).
Русский
В конечном размерном случае, если в K содержатся все корни n-й степени, то being Galois и цикличность автоматически равнозначны через существование нужного irreducible полинома и соответствующего α.
LaTeX
$$List.TFAE[ IsGalois(K,L) ∧ IsCyclic(L ≃_K L), ∃ a, Irreducible(X^n − C a) ∧ IsSplittingField(K,L,X^n − C a), ∃ α∈L, α^{finrank(K,L)} ∈ range(algebraMap K L) ∧ K⟮α⟯ = ⊤ ]$$
Lean4
/-- Suppose `L/K` is a finite extension of dimension `n`, and `K` contains all `n`-th roots of unity.
Then `L/K` is cyclic iff
`L` is a splitting field of some irreducible polynomial of the form `Xⁿ - a : K[X]` iff
`L = K[α]` for some `αⁿ ∈ K`.
-/
theorem isCyclic_tfae (K L) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
(hK : (primitiveRoots (Module.finrank K L) K).Nonempty) :
List.TFAE
[IsGalois K L ∧ IsCyclic (L ≃ₐ[K] L),
∃ a : K, Irreducible (X ^ (finrank K L) - C a) ∧ IsSplittingField K L (X ^ (finrank K L) - C a),
∃ (α : L), α ^ (finrank K L) ∈ Set.range (algebraMap K L) ∧ K⟮α⟯ = ⊤] :=
by
have : NeZero (Module.finrank K L) := NeZero.of_pos finrank_pos
tfae_have 1 → 3
| ⟨inst₁, inst₂⟩ => exists_root_adjoin_eq_top_of_isCyclic K L hK
tfae_have 3 → 2
| ⟨α, ⟨a, ha⟩, hα⟩ =>
⟨a, irreducible_X_pow_sub_C_of_root_adjoin_eq_top ha.symm hα,
isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top hK ha.symm hα⟩
tfae_have 2 → 1
| ⟨a, H, inst⟩ => ⟨isGalois_of_isSplittingField_X_pow_sub_C hK H L, isCyclic_of_isSplittingField_X_pow_sub_C hK H L⟩
tfae_finish
