English
If L/K is S-cyclotomic, then L/K is a Galois extension.
Русский
Если L/K циклотомическое по S, то L/K — галуа-расширение.
LaTeX
$$$IsCyclotomicExtension(S,K,L) \\Rightarrow IsGalois(K,L)$$$
Lean4
theorem isGalois [IsCyclotomicExtension S K L] : IsGalois K L :=
by
rw [isGalois_iff]
use isSeparable S K L
obtain ⟨i⟩ := nonempty_algEquiv_adjoin_of_isSepClosed S K L (AlgebraicClosure K)
rw [i.transfer_normal, IntermediateField.normal_iff_forall_map_le]
intro f x hx
rw [← IntermediateField.mem_toSubalgebra, IntermediateField.toSubalgebra_map, Subalgebra.mem_map] at hx
obtain ⟨y, hy, rfl⟩ := hx
rw [IntermediateField.mem_toSubalgebra] at hy
induction hy using IntermediateField.adjoin_induction with
| mem x hx =>
obtain ⟨n, hn, h1, h2⟩ := hx
apply IntermediateField.subset_adjoin
use n, hn, h1
rw [← map_pow, ← map_one f, h2]
| algebraMap x =>
convert IntermediateField.algebraMap_mem _ x
exact AlgHom.commutes _ x
| add x y hx hy ihx ihy =>
rw [map_add]
exact add_mem ihx ihy
| mul x y hx hy ihx ihy =>
rw [map_mul]
exact mul_mem ihx ihy
| inv x hx ihx =>
rw [map_inv₀]
exact inv_mem ihx
