English
Let E/F be a finite Galois extension. Then the size of the Galois group Aut(E/F) equals the degree [E:F].
Русский
Пусть расширение E/F Галуа и конечно. Тогда число элементов группы Галуа Aut(E/F) равно степени расширения [E:F].
LaTeX
$$Nat.card (E ≃ₐ[F] E) = finrank F E$$
Lean4
/-- Let $E / F$ be a finite extension of fields. If $E$ is Galois over $F$, then
$|\text{Aut}(E/F)| = [E : F]$. -/
@[stacks 09I1 "'only if' part"]
theorem card_aut_eq_finrank [FiniteDimensional F E] [IsGalois F E] : Nat.card (E ≃ₐ[F] E) = finrank F E :=
by
obtain ⟨α, hα⟩ := Field.exists_primitive_element F E
let iso : F⟮α⟯ ≃ₐ[F] E :=
{ toFun := fun e => e.val
invFun := fun e => ⟨e, by rw [hα]; exact IntermediateField.mem_top⟩
map_mul' := fun _ _ => rfl
map_add' := fun _ _ => rfl
commutes' := fun _ => rfl }
have H : IsIntegral F α := IsGalois.integral F α
have h_sep : IsSeparable F α := IsGalois.separable F α
have h_splits : (minpoly F α).Splits (algebraMap F E) := IsGalois.splits F α
replace h_splits : Polynomial.Splits (algebraMap F F⟮α⟯) (minpoly F α) := by
simpa using Polynomial.splits_comp_of_splits (algebraMap F E) iso.symm.toAlgHom.toRingHom h_splits
rw [← LinearEquiv.finrank_eq iso.toLinearEquiv]
rw [← IntermediateField.AdjoinSimple.card_aut_eq_finrank F E H h_sep h_splits]
apply Nat.card_congr
exact Equiv.mk (fun ϕ => iso.trans (ϕ.trans iso.symm)) fun ϕ => iso.symm.trans (ϕ.trans iso)
