Splitting finite étale algebras over a field

A finite étale algebra A over a field K becomes a product of copies of the ground field after a finite Galois extension L / K whose degree divides (finrank K A)!. Thus all the points of a finite étale scheme can be labelled over one finite separable extension, even when the ground field is imperfect, and the degree of that extension is bounded in terms of the number of geometric points alone.

Over a separably closed field Ω, the algebra A has exactly finrank K A points (TauCeti.Algebra.Etale.card_algHom_eq_finrank). For Ω a separable closure, the splitting field is the subfield generated by the values of all these points. It is stable under Gal(Ω / K), hence Galois over K, and its Galois group acts faithfully on the finrank K A points of A with values in it, so its degree divides (finrank K A)!.

References

• The Stacks Project, Tag 03QR (finite étale schemes over a field).
• H. W. Lenstra, Galois theory for schemes, Section 5.

theorem TauCeti.Algebra.Etale.card_algHom_eq_finrank (K : Type u) (A : Type v) [Field K] [CommRing A] [Algebra K A] [Algebra.Etale K A] (Ω : Type u_1) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] : Nat.card (A →ₐ[K] Ω) = Module.finrank K A

An étale algebra has as many separably closed points as its dimension. A finite étale algebra A over a field K has exactly finrank K A points with values in any separably closed extension of K.

theorem TauCeti.Algebra.Etale.exists_isFiniteSplit_tensorProduct (K : Type u) (A : Type v) [Field K] [CommRing A] [Algebra K A] [Algebra.Etale K A] : ∃ (L : Type u) (x : Field L) (x_1 : Algebra K L) (_ : Module.Finite K L) (_ : IsGalois K L), Module.finrank K L ∣ (Module.finrank K A).factorial ∧ Algebra.IsFiniteSplit L (TensorProduct K L A)

A finite étale algebra over a field splits after a Galois extension of degree dividing (finrank K A)!. The extension is finite and Galois over K, and it lives in the universe of K.