Finite étale group schemes over a field and Galois groups

Let K be a field and Ω a separable closure of K. Grothendieck's Galois theory for K (TauCeti.galoisFiber, TauCeti.isEquivalence_galoisFiber) identifies finite étale K-algebras with finite sets carrying a continuous action of Gal(Ω/K). Composed with the anti-equivalence between finite étale algebras and finite étale schemes, it gives the scheme form of the correspondence (TauCeti.FiniteEtaleScheme.galoisEquivalence):

FiniteEtaleScheme (Spec K) ≌ ContAction FintypeCat Gal(Ω/K),

sending a finite étale K-scheme Spec A to the finite Gal(Ω/K)-set of Ω-valued points of A (TauCeti.FiniteEtaleScheme.specCompGaloisEquivalenceFunctorIso).

Both categories are cartesian monoidal: finite étale schemes over K are closed under fibre products over K, and continuous actions on finite sets are closed under products with the diagonal action. Like every equivalence of categories, galoisEquivalence K Ω preserves finite products, so it is a monoidal functor for these structures, braided as well, and it carries group objects to group objects. The correspondence therefore restricts to an equivalence between group objects in finite étale K-schemes and group objects in finite continuous Gal(Ω/K)-sets, that is, finite groups on which Gal(Ω/K) acts continuously by group automorphisms (TauCeti.FiniteEtaleScheme.galoisEquivalenceGrp), and between their commutative versions (TauCeti.FiniteEtaleScheme.galoisEquivalenceCommGrp). Being equivalences of categories, these also identify the homomorphisms of group objects on the two sides.

A bilinear alternating pairing G ⊗ G ⟶ M of commutative group objects, in the sense of TauCeti.CategoryTheory.IsBilinear and TauCeti.CategoryTheory.IsAlternating (conditions on points with values in every object), corresponds under the equivalence to a bilinear alternating pairing of the associated Galois sets, and conversely (TauCeti.FiniteEtaleScheme.galoisEquivalenceAlternatingPairingEquiv). For instance, a Galois-equivariant alternating pairing of a finite Galois module with values in the roots of unity gives a finite étale group scheme with an alternating pairing.

Group objects in FiniteEtaleScheme S are the finite étale group schemes over S (TauCeti.FiniteEtaleScheme.essImage_mapGrp_ι_iff, in TauCeti.AlgebraicGeometry.FiniteEtale.GroupScheme).

Main definitions

• TauCeti.FiniteEtaleScheme.galoisEquivalence K Ω: finite étale K-schemes are equivalent to finite continuous Gal(Ω/K)-sets.
• TauCeti.FiniteEtaleScheme.galoisEquivalenceGrp K Ω: group objects in finite étale K-schemes are equivalent to group objects in finite continuous Gal(Ω/K)-sets.
• TauCeti.FiniteEtaleScheme.galoisEquivalenceCommGrp K Ω: the same for commutative group objects.
• TauCeti.FiniteEtaleScheme.galoisEquivalenceAlternatingPairingEquiv K Ω: bilinear alternating pairings of finite étale K-group schemes correspond to bilinear alternating pairings of the associated finite Galois sets.

Main results

• TauCeti.FiniteEtaleScheme.specCompGaloisEquivalenceFunctorIso: on spectra, the equivalence is the functor of Ω-valued points with its Galois action.
• TauCeti.FiniteEtaleScheme.galoisEquivalenceGrp_functor_comp_forget and TauCeti.FiniteEtaleScheme.galoisEquivalenceCommGrp_functor_comp_forget: on underlying objects, the equivalences of group objects are galoisEquivalence K Ω.

References

• A. Grothendieck, Revêtements étales et groupe fondamental (SGA 1), Exposé V, §8.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Graduate Texts in Mathematics 66, Springer, 1979, §6.4.

noncomputable def TauCeti.FiniteEtaleScheme.galoisEquivalence (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] : FiniteEtaleScheme (AlgebraicGeometry.Spec ↧K) ≌ ContAction FintypeCat Gal(Ω/K)

Galois theory for finite étale schemes over a field. For a separable closure Ω of K, finite étale K-schemes are equivalent to finite sets with a continuous action of Gal(Ω/K). A finite étale scheme Spec A goes to the set of Ω-valued points of A (specCompGaloisEquivalenceFunctorIso).

@[simp]

theorem TauCeti.FiniteEtaleScheme.galoisEquivalence_functor (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] : (galoisEquivalence K Ω).functor = (finiteEtaleCommAlgCatOpEquivFiniteEtaleScheme ↧K).inverse.comp (galoisFiber K Ω)

The functor of galoisEquivalence K Ω takes coordinate algebras and then Ω-valued points.

@[simp]

theorem TauCeti.FiniteEtaleScheme.galoisEquivalence_inverse (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] : (galoisEquivalence K Ω).inverse = (galoisFiber K Ω).asEquivalence.inverse.comp (spec ↧K)

The inverse of galoisEquivalence K Ω inverts the Galois fibre functor and then takes the spectrum.

noncomputable def TauCeti.FiniteEtaleScheme.specCompGaloisEquivalenceFunctorIso (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] : (spec ↧K).comp (galoisEquivalence K Ω).functor ≅ galoisFiber K Ω

The Galois set of a spectrum. For a finite étale K-algebra A, galoisEquivalence K Ω sends Spec A to the finite set A →ₐ[K] Ω of Ω-valued points of A, with Gal(Ω/K) acting by postcomposition.

@[simp]

theorem TauCeti.FiniteEtaleScheme.specCompGaloisEquivalenceFunctorIso_hom_app (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] (A : (CommAlgCat.FiniteEtale K)ᵒᵖ) : (specCompGaloisEquivalenceFunctorIso K Ω).hom.app A = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((galoisFiber K Ω).map ((finiteEtaleCommAlgCatOpEquivFiniteEtaleScheme ↧K).unitIso.inv.app A))

The component of specCompGaloisEquivalenceFunctorIso at A is the Galois fibre functor applied to the inverse unit of the finite étale anti-equivalence at A, after identifying spec with the forward functor of that anti-equivalence.

@[simp]

theorem TauCeti.FiniteEtaleScheme.specCompGaloisEquivalenceFunctorIso_inv_app (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] (A : (CommAlgCat.FiniteEtale K)ᵒᵖ) : (specCompGaloisEquivalenceFunctorIso K Ω).inv.app A = CategoryTheory.CategoryStruct.comp ((galoisFiber K Ω).map ((finiteEtaleCommAlgCatOpEquivFiniteEtaleScheme ↧K).unitIso.hom.app A)) (CategoryTheory.eqToHom ⋯)

The inverse component of specCompGaloisEquivalenceFunctorIso at A is the Galois fibre functor applied to the unit of the finite étale anti-equivalence at A, after identifying the forward functor of that anti-equivalence with spec.

@[instance_reducible]

noncomputable instance TauCeti.FiniteEtaleScheme.instMonoidalSpecOfContActionFintypeCatFunObjFiniteAlgEquivFunctorGaloisEquivalence (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] : (galoisEquivalence K Ω).functor.Monoidal

The functor of galoisEquivalence K Ω is monoidal for the cartesian monoidal structures, as it preserves finite products.

@[instance_reducible]

noncomputable instance TauCeti.FiniteEtaleScheme.instMonoidalContActionFintypeCatFunObjFiniteAlgEquivSpecOfInverseGaloisEquivalence (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] : (galoisEquivalence K Ω).inverse.Monoidal

The inverse of galoisEquivalence K Ω is monoidal for the cartesian monoidal structures, as it preserves finite products.

@[instance_reducible]

noncomputable instance TauCeti.FiniteEtaleScheme.instBraidedSpecOfContActionFintypeCatFunObjFiniteAlgEquivFunctorGaloisEquivalence (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] : (galoisEquivalence K Ω).functor.Braided

The functor of galoisEquivalence K Ω is braided.

@[instance_reducible]

noncomputable instance TauCeti.FiniteEtaleScheme.instBraidedContActionFintypeCatFunObjFiniteAlgEquivSpecOfInverseGaloisEquivalence (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] : (galoisEquivalence K Ω).inverse.Braided

The inverse of galoisEquivalence K Ω is braided.

noncomputable def TauCeti.FiniteEtaleScheme.galoisEquivalenceGrp (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] : CategoryTheory.Grp (FiniteEtaleScheme (AlgebraicGeometry.Spec ↧K)) ≌ CategoryTheory.Grp (ContAction FintypeCat Gal(Ω/K))

Finite étale group schemes over a field are finite Galois groups. Group objects in finite étale K-schemes are equivalent to group objects in finite continuous Gal(Ω/K)-sets, that is, to finite groups on which Gal(Ω/K) acts continuously by group automorphisms. Morphisms on both sides are homomorphisms of group objects.

theorem TauCeti.FiniteEtaleScheme.galoisEquivalenceGrp_functor_comp_forget (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] : (galoisEquivalenceGrp K Ω).functor.comp (CategoryTheory.Grp.forget (ContAction FintypeCat Gal(Ω/K))) = (CategoryTheory.Grp.forget (FiniteEtaleScheme (AlgebraicGeometry.Spec ↧K))).comp (galoisEquivalence K Ω).functor

On underlying objects, galoisEquivalenceGrp K Ω is galoisEquivalence K Ω.

theorem TauCeti.FiniteEtaleScheme.galoisEquivalenceGrp_inverse_comp_forget (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] : (galoisEquivalenceGrp K Ω).inverse.comp (CategoryTheory.Grp.forget (FiniteEtaleScheme (AlgebraicGeometry.Spec ↧K))) = (CategoryTheory.Grp.forget (ContAction FintypeCat Gal(Ω/K))).comp (galoisEquivalence K Ω).inverse

On underlying objects, the inverse of galoisEquivalenceGrp K Ω is the inverse of galoisEquivalence K Ω.

noncomputable def TauCeti.FiniteEtaleScheme.galoisEquivalenceCommGrp (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] : CategoryTheory.CommGrp (FiniteEtaleScheme (AlgebraicGeometry.Spec ↧K)) ≌ CategoryTheory.CommGrp (ContAction FintypeCat Gal(Ω/K))

Finite étale commutative group schemes over a field are finite Galois modules. Commutative group objects in finite étale K-schemes are equivalent to commutative group objects in finite continuous Gal(Ω/K)-sets, that is, to finite abelian groups with a continuous action of Gal(Ω/K) by group automorphisms.

theorem TauCeti.FiniteEtaleScheme.galoisEquivalenceCommGrp_functor_comp_forget (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] : (galoisEquivalenceCommGrp K Ω).functor.comp (CategoryTheory.CommGrp.forget (ContAction FintypeCat Gal(Ω/K))) = (CategoryTheory.CommGrp.forget (FiniteEtaleScheme (AlgebraicGeometry.Spec ↧K))).comp (galoisEquivalence K Ω).functor

On underlying objects, galoisEquivalenceCommGrp K Ω is galoisEquivalence K Ω.

theorem TauCeti.FiniteEtaleScheme.galoisEquivalenceCommGrp_inverse_comp_forget (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] : (galoisEquivalenceCommGrp K Ω).inverse.comp (CategoryTheory.CommGrp.forget (FiniteEtaleScheme (AlgebraicGeometry.Spec ↧K))) = (CategoryTheory.CommGrp.forget (ContAction FintypeCat Gal(Ω/K))).comp (galoisEquivalence K Ω).inverse

On underlying objects, the inverse of galoisEquivalenceCommGrp K Ω is the inverse of galoisEquivalence K Ω.

noncomputable def TauCeti.FiniteEtaleScheme.galoisEquivalenceAlternatingPairingEquiv (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] (G M : CategoryTheory.CommGrp (FiniteEtaleScheme (AlgebraicGeometry.Spec ↧K))) : { e : CategoryTheory.MonoidalCategoryStruct.tensorObj G.X G.X ⟶ M.X // CategoryTheory.IsBilinear e ∧ CategoryTheory.IsAlternating e } ≃ { e : CategoryTheory.MonoidalCategoryStruct.tensorObj ((galoisEquivalence K Ω).functor.obj G.X) ((galoisEquivalence K Ω).functor.obj G.X) ⟶ (galoisEquivalence K Ω).functor.obj M.X // CategoryTheory.IsBilinear e ∧ CategoryTheory.IsAlternating e }

The Galois correspondence transports alternating pairings. For commutative group objects G and M of finite étale K-schemes, bilinear alternating pairings G ⊗ G ⟶ M correspond to bilinear alternating pairings F G ⊗ F G ⟶ F M of the associated finite continuous Gal(Ω/K)-sets, where F = (galoisEquivalence K Ω).functor and F G, with its group structure, is the underlying object of (galoisEquivalenceCommGrp K Ω).functor.obj G. A pairing e goes to μ F G G ≫ F.map e.

@[simp]

theorem TauCeti.FiniteEtaleScheme.galoisEquivalenceAlternatingPairingEquiv_apply_coe (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] (G M : CategoryTheory.CommGrp (FiniteEtaleScheme (AlgebraicGeometry.Spec ↧K))) (e : { e : CategoryTheory.MonoidalCategoryStruct.tensorObj G.X G.X ⟶ M.X // CategoryTheory.IsBilinear e ∧ CategoryTheory.IsAlternating e }) : ↑((galoisEquivalenceAlternatingPairingEquiv K Ω G M) e) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (galoisEquivalence K Ω).functor G.X G.X) ((galoisEquivalence K Ω).functor.map ↑e)

galoisEquivalenceAlternatingPairingEquiv K Ω sends a pairing e to μ F G G ≫ F.map e, for F = (galoisEquivalence K Ω).functor.

@[simp]

theorem TauCeti.FiniteEtaleScheme.galoisEquivalenceAlternatingPairingEquiv_symm_apply_coe (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] (G M : CategoryTheory.CommGrp (FiniteEtaleScheme (AlgebraicGeometry.Spec ↧K))) (e : { e : CategoryTheory.MonoidalCategoryStruct.tensorObj ((galoisEquivalence K Ω).functor.obj G.X) ((galoisEquivalence K Ω).functor.obj G.X) ⟶ (galoisEquivalence K Ω).functor.obj M.X // CategoryTheory.IsBilinear e ∧ CategoryTheory.IsAlternating e }) : ↑((galoisEquivalenceAlternatingPairingEquiv K Ω G M).symm e) = (galoisEquivalence K Ω).fullyFaithfulFunctor.preimage (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ (galoisEquivalence K Ω).functor G.X G.X) ↑e)

The inverse of galoisEquivalenceAlternatingPairingEquiv K Ω sends a pairing e of Galois sets to the unique morphism G ⊗ G ⟶ M whose image under F = (galoisEquivalence K Ω).functor is δ F G G ≫ e.