Splitting finite étale schemes over a field

Every finite étale scheme over a field becomes the spectrum of a finite product of n copies of the base field after a finite Galois extension whose degree divides n!. The isomorphism is over the extended base, so it labels all points as rational points, including their scheme structures. The empty scheme corresponds to the product indexed by Fin 0.

This is the scheme form of TauCeti.Algebra.Etale.exists_isFiniteSplit_tensorProduct, transported through TauCeti.FiniteEtaleScheme.spec and Mathlib's affine pullback comparison. Two finite étale schemes split over a common finite Galois extension, one splitting their disjoint union.

Once a finite étale scheme S and an S-scheme E of constant rank d are both split over the base field, E is d copies of S (AlgebraicGeometry.Scheme.Hom.exists_split_of_finrank_eq): the rational points of E above each rational point of S are counted by the rank (Algebra.IsFiniteSplit.nonempty_algEquiv_fun_of_rankAtStalk_eq).

Counted in the functor-of-points sense, there is a finite Galois extension L / K of degree dividing n! over which a finite étale scheme X of rank n over K has exactly n points with values in L, that is n morphisms Spec L ⟶ X over Spec K. The rank is Mathlib's AlgebraicGeometry.Scheme.Hom.finrank, so this applies to any finite étale scheme over a field whose rank is known.

References

• The Stacks Project, Tag 03QR (schemes étale over a point).

theorem AlgebraicGeometry.Scheme.Hom.exists_split_of_isFinite_of_etale {K : Type u} [Field K] {X : Scheme} (f : X ⟶ Spec ↧K) [IsFinite f] [Etale f] : ∃ (L : Type u) (x : Field L) (x_1 : Algebra K L) (_ : Module.Finite K L) (_ : IsGalois K L) (n : ℕ), Module.finrank K L ∣ n.factorial ∧ Nonempty (CategoryTheory.Over.mk (CategoryTheory.Limits.pullback.snd f (Spec.algebraMap K L)) ≅ CategoryTheory.Over.mk (Spec.algebraMap L (Fin n → L)))

A finite étale scheme becomes a disjoint union of n rational points after a finite Galois field extension of degree dividing n!. The splitting is an isomorphism over the extended base.

theorem AlgebraicGeometry.Scheme.Hom.exists_split_of_isFinite_of_etale₂ {K : Type u} [Field K] {X Y : Scheme} (f : X ⟶ Spec ↧K) (g : Y ⟶ Spec ↧K) [IsFinite f] [Etale f] [IsFinite g] [Etale g] : ∃ (L : Type u) (x : Field L) (x_1 : Algebra K L) (_ : Module.Finite K L) (_ : IsGalois K L) (n : ℕ) (m : ℕ), Nonempty (CategoryTheory.Over.mk (CategoryTheory.Limits.pullback.snd f (Spec.algebraMap K L)) ≅ CategoryTheory.Over.mk (Spec.algebraMap L (Fin n → L))) ∧ Nonempty (CategoryTheory.Over.mk (CategoryTheory.Limits.pullback.snd g (Spec.algebraMap K L)) ≅ CategoryTheory.Over.mk (Spec.algebraMap L (Fin m → L)))

Two finite étale schemes over a field become disjoint unions of n and m rational points after one common finite Galois field extension. The splittings are isomorphisms over the extended base.

theorem AlgebraicGeometry.Scheme.Hom.exists_split_of_finrank_eq {L : Type u} [Field L] {S E : Scheme} {n m d : ℕ} (p : E ⟶ S) (hp : ∀ (s : ↥S), finrank p s = d) (e : S ≅ Spec ↧(Fin n → L)) (eE : E ≅ Spec ↧(Fin m → L)) (h : CategoryTheory.CategoryStruct.comp eE.hom (Spec.algebraMap L (Fin m → L)) = CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp e.hom (Spec.algebraMap L (Fin n → L)))) : ∃ (e' : E ≅ Spec ↧(Fin d → Fin n → L)), CategoryTheory.CategoryStruct.comp e'.hom (Spec.algebraMap (Fin n → L) (Fin d → Fin n → L)) = CategoryTheory.CategoryStruct.comp p e.hom

A morphism of constant rank between split schemes over a field is a trivial cover. Let p : E ⟶ S have rank d at every point, where S and E are identified with Spec (Fin n → L) and Spec (Fin m → L) compatibly with their morphisms to Spec L; such a p is automatically finite and flat. Then E is Spec (Fin d → Fin n → L) over S, that is, d copies of S.

theorem AlgebraicGeometry.Scheme.Hom.exists_natCard_hom_eq_finrank_of_isFinite_of_etale {K : Type u} [Field K] {X : Scheme} (f : X ⟶ Spec ↧K) [IsFinite f] [Etale f] (s : ↥(Spec ↧K)) : ∃ (L : Type u) (x : Field L) (x_1 : Algebra K L) (_ : Module.Finite K L) (_ : IsGalois K L), Module.finrank K L ∣ (finrank f s).factorial ∧ Nat.card (CategoryTheory.Over.mk (Spec.algebraMap K L) ⟶ CategoryTheory.Over.mk f) = finrank f s

A finite étale scheme of rank n has n points over a Galois extension of degree dividing n!. For a finite étale morphism f : X ⟶ Spec K of rank n there is a finite Galois extension L / K of degree dividing n! such that exactly n morphisms Spec L ⟶ X lie over Spec K.