Finite étale algebras over a field as finite continuous Galois sets

Let K be a field and Ω a separable closure of K, with absolute Galois group Gal(Ω/K) carrying the Krull topology. To a finite étale K-algebra A attach the finite set A →ₐ[K] Ω of its Ω-valued points, on which Gal(Ω/K) acts by postcomposition. This file shows that the resulting functor

TauCeti.galoisFiber K Ω : (FiniteEtale K)ᵒᵖ ⥤ ContAction FintypeCat Gal(Ω/K)

to finite sets with a continuous action of Gal(Ω/K) is an equivalence of categories (Grothendieck's Galois theory for a field). It lifts Mathlib's fibre functor CommAlgCat.FiniteEtale.fiber K Ω to the category of Galois sets (TauCeti.galoisFiber_comp_forget₂). Finite étale schemes over K and their morphisms can thus be described by finite sets with a continuous Galois action; this is the dictionary through which a finite étale group scheme over K is attached to a continuous Galois action on a finite group.

Full faithfulness is Galois descent. Over the separably closed field Ω, an étale K-algebra splits: evaluation at the points of A is an isomorphism of Ω-algebras

Ω ⊗[K] A ≃ₐ[Ω] ((A →ₐ[K] Ω) → Ω)

(Algebra.Etale.tensorProductEquivPi), because Ω ⊗[K] A is a finite product of copies of Ω (Mathlib's Algebra.IsFiniteSplit instance) and a totally split algebra is the algebra of functions on its characters. Under this isomorphism the action of Gal(Ω/K) on the scalar factor becomes the conjugation action on functions, whose fixed points are the equivariant functions. The fixed tensors are those of A itself (TauCeti.GaloisDescent), so evaluation identifies A with the Gal(Ω/K)-equivariant functions (A →ₐ[K] Ω) → Ω (Algebra.Etale.pi_id_injective, Algebra.Etale.mem_range_pi_id_iff). An equivariant map of point sets (B →ₐ[K] Ω) → (A →ₐ[K] Ω) therefore pulls functions on A's points back to equivariant functions on B's points, which come from B; this is the algebra map A →ₐ[K] B inducing it.

The action is continuous because the stabilizer of a point φ : A →ₐ[K] Ω contains the subgroup fixing the finite extension of K generated by φ applied to a spanning set of A (AlgHom.stabilizer_isOpen).

Essential surjectivity only needs Ω/K to be Galois. A finite Gal(Ω/K)-set X with open stabilizers is realised by the product, over the orbits of X, of the fields fixed by the stabilizers of orbit representatives: these fields are finite separable over K by infinite Galois theory, the Ω-valued points of a finite product of fields are the points of its factors (AlgHom.exists_eq_comp_piEvalAlgHom), and the embeddings of the field fixed by the stabilizer of x are the translates of the inclusion, by normality of Ω/K, one for each point of the orbit of x.

Main definitions

• Algebra.Etale.tensorProductEquivPi K Ω A: for an étale K-algebra A and a separably closed field Ω, the splitting Ω ⊗[K] A ≃ₐ[Ω] ((A →ₐ[K] Ω) → Ω).
• Algebra.Etale.algHomTensorProductEquivPi K Ω A C: for an A-algebra C, the induced identification of the A-algebra maps C → A ⊗[K] Ω with the families, indexed by the points φ : A →ₐ[K] Ω, of ring maps C → Ω extending φ.
• Algebra.Etale.algHomEquivMulActionHom Ω: for a separable closure Ω of K and an étale K-algebra B, the identification of A →ₐ[K] B with the Gal(Ω/K)-equivariant maps (B →ₐ[K] Ω) → (A →ₐ[K] Ω).
• TauCeti.galoisFiberAction K Ω: the functor sending a finite étale K-algebra to the finite Gal(Ω/K)-set of its Ω-valued points.
• TauCeti.galoisFiber K Ω: the functor sending a finite étale K-algebra to the finite continuous Gal(Ω/K)-set of its Ω-valued points.

Main results

• Algebra.Etale.algHomTensorProductEquivPi_lTensor: the action of Gal(Ω/K) on the scalar factor permutes the components of algHomTensorProductEquivPi.
• Algebra.Etale.pi_id_injective: the Ω-valued points of an étale K-algebra separate its elements.
• Algebra.Etale.mem_range_pi_id_iff: a function on the Ω-valued points of an étale K-algebra is evaluation at an element exactly when it is Gal(Ω/K)-equivariant.
• TauCeti.isContinuous_galoisFiberAction_obj: the Galois action on the points of a finite étale K-algebra is continuous.
• TauCeti.galoisFiber_comp_forget₂: forgetting the action recovers Mathlib's fibre functor.
• TauCeti.faithful_fiber: the fibre functor at a separably closed field is faithful.
• TauCeti.galoisFiberFullyFaithful: for a separable closure Ω of K, galoisFiber K Ω is fully faithful.
• TauCeti.exists_mulActionHom_algHom_bijective: for a Galois extension Ω/K, every finite Gal(Ω/K)-set with open stabilizers is equivariantly the set of Ω-valued points of a finite étale K-algebra.
• TauCeti.essSurj_galoisFiber: for a Galois extension Ω/K, galoisFiber K Ω is essentially surjective.
• TauCeti.isEquivalence_galoisFiber: for a separable closure Ω of K, galoisFiber K Ω is an equivalence of categories.

References

• A. Grothendieck, Revêtements étales et groupe fondamental (SGA 1), Exposé V, §8.
• H. W. Lenstra, Galois theory for schemes, §2.
• The Stacks Project, Tag 03QR.

noncomputable def Algebra.Etale.tensorProductEquivPi (K : Type u_1) (Ω : Type u_2) (A : Type u_3) [Field K] [Field Ω] [Algebra K Ω] [CommRing A] [Algebra K A] [IsSepClosed Ω] [Etale K A] : TensorProduct K Ω A ≃ₐ[Ω] (A →ₐ[K] Ω) → Ω

An étale algebra splits over a separably closed field. For an étale algebra A over a field K and a separably closed field Ω over K, evaluation at the Ω-valued points of A is an isomorphism of Ω-algebras Ω ⊗[K] A ≃ₐ[Ω] ((A →ₐ[K] Ω) → Ω), sending ω ⊗ a to φ ↦ ω * φ a (tensorProductEquivPi_tmul).

@[simp]

theorem Algebra.Etale.tensorProductEquivPi_tmul {K : Type u_1} {Ω : Type u_2} {A : Type u_3} [Field K] [Field Ω] [Algebra K Ω] [CommRing A] [Algebra K A] [IsSepClosed Ω] [Etale K A] (ω : Ω) (a : A) (φ : A →ₐ[K] Ω) : (tensorProductEquivPi K Ω A) (ω ⊗ₜ[K] a) φ = ω * φ a

The splitting sends ω ⊗ a to the function φ ↦ ω * φ a.

theorem Algebra.Etale.pi_id_injective (K : Type u_1) (Ω : Type u_2) (A : Type u_3) [Field K] [Field Ω] [Algebra K Ω] [CommRing A] [Algebra K A] [IsSepClosed Ω] [Etale K A] : Function.Injective ⇑(AlgHom.pi fun (φ : A →ₐ[K] Ω) => φ)

The Ω-valued points of an étale algebra separate its elements, for a separably closed field Ω.

theorem Algebra.Etale.tensorProductEquivPi_map {K : Type u_1} {Ω : Type u_2} {A : Type u_3} [Field K] [Field Ω] [Algebra K Ω] [CommRing A] [Algebra K A] [IsSepClosed Ω] [Etale K A] (σ : Gal(Ω/K)) (t : TensorProduct K Ω A) (φ : A →ₐ[K] Ω) : (tensorProductEquivPi K Ω A) ((_root_.TensorProduct.map σ.toLinearMap LinearMap.id) t) φ = σ ((tensorProductEquivPi K Ω A) t (σ⁻¹ • φ))

Under the splitting tensorProductEquivPi, the action of σ ∈ Gal(Ω/K) on the scalar factor of Ω ⊗[K] A becomes conjugation by σ on functions of the points of A.

theorem Algebra.Etale.mem_range_pi_id_iff {K : Type u_1} {Ω : Type u_2} {A : Type u_3} [Field K] [Field Ω] [Algebra K Ω] [CommRing A] [Algebra K A] [IsSepClosed Ω] [IsGalois K Ω] [Etale K A] (h : (A →ₐ[K] Ω) → Ω) : h ∈ (AlgHom.pi fun (φ : A →ₐ[K] Ω) => φ).range ↔ ∀ (σ : Gal(Ω/K)) (φ : A →ₐ[K] Ω), h (σ • φ) = σ (h φ)

Galois descent for an étale algebra. For an étale algebra A over a field K and a separable closure Ω of K, a function h on the Ω-valued points of A is evaluation at an element of A if and only if it is Gal(Ω/K)-equivariant: h (σ • φ) = σ (h φ).

theorem Algebra.Etale.tensorProductEquivPi_comm {K : Type u_1} {Ω : Type u_2} {A : Type u_3} [Field K] [Field Ω] [Algebra K Ω] [CommRing A] [Algebra K A] [IsSepClosed Ω] [Etale K A] (t : TensorProduct K A Ω) (φ : A →ₐ[K] Ω) : (tensorProductEquivPi K Ω A) ((TensorProduct.comm K A Ω) t) φ = (TensorProduct.productMap φ (AlgHom.id K Ω)) t

With the tensor factors in the order A ⊗[K] Ω, the splitting tensorProductEquivPi sends t to the function whose value at φ is the image of t under a ⊗ ω ↦ φ a * ω.

noncomputable def Algebra.Etale.algHomTensorProductEquivPi (K : Type u_1) (Ω : Type u_2) (A : Type u_3) [Field K] [Field Ω] [Algebra K Ω] [CommRing A] [Algebra K A] (C : Type u_4) [CommRing C] [Algebra A C] [IsSepClosed Ω] [Etale K A] : (C →ₐ[A] TensorProduct K A Ω) ≃ ((φ : A →ₐ[K] Ω) → { f : C →+* Ω // f.comp (algebraMap A C) = ↑φ })

A-algebra maps into A ⊗[K] Ω split over the points of A. For an étale algebra A over a field K, a separably closed field Ω over K and an A-algebra C, an A-algebra map g : C → A ⊗[K] Ω amounts to a family, indexed by the K-algebra maps φ : A → Ω, of ring maps f_φ : C → Ω extending φ, that is, of Ω-valued points of C for the A-algebra structure of Ω given by φ. The φ-component of g is g followed by a ⊗ ω ↦ φ a * ω (algHomTensorProductEquivPi_apply); the inverse is characterized by productMap_algHomTensorProductEquivPi_symm_apply.

@[simp]

theorem Algebra.Etale.algHomTensorProductEquivPi_apply {K : Type u_1} {Ω : Type u_2} {A : Type u_3} [Field K] [Field Ω] [Algebra K Ω] [CommRing A] [Algebra K A] {C : Type u_4} [CommRing C] [Algebra A C] [IsSepClosed Ω] [Etale K A] (g : C →ₐ[A] TensorProduct K A Ω) (φ : A →ₐ[K] Ω) (c : C) : ↑((algHomTensorProductEquivPi K Ω A C) g φ) c = (TensorProduct.productMap φ (AlgHom.id K Ω)) (g c)

The φ-component of algHomTensorProductEquivPi K Ω A C g sends c to the image of g c under a ⊗ ω ↦ φ a * ω.

@[simp]

theorem Algebra.Etale.productMap_algHomTensorProductEquivPi_symm_apply {K : Type u_1} {Ω : Type u_2} {A : Type u_3} [Field K] [Field Ω] [Algebra K Ω] [CommRing A] [Algebra K A] {C : Type u_4} [CommRing C] [Algebra A C] [IsSepClosed Ω] [Etale K A] (f : (φ : A →ₐ[K] Ω) → { f : C →+* Ω // f.comp (algebraMap A C) = ↑φ }) (φ : A →ₐ[K] Ω) (c : C) : (TensorProduct.productMap φ (AlgHom.id K Ω)) (((algHomTensorProductEquivPi K Ω A C).symm f) c) = ↑(f φ) c

The A-algebra map attached to a family f of points has φ-component f φ: following it by a ⊗ ω ↦ φ a * ω gives f φ.

theorem Algebra.Etale.algHomTensorProductEquivPi_lTensor {K : Type u_1} {Ω : Type u_2} {A : Type u_3} [Field K] [Field Ω] [Algebra K Ω] [CommRing A] [Algebra K A] {C : Type u_4} [CommRing C] [Algebra A C] [IsSepClosed Ω] [Etale K A] (σ : Gal(Ω/K)) (g : C →ₐ[A] TensorProduct K A Ω) (φ : A →ₐ[K] Ω) : ↑((algHomTensorProductEquivPi K Ω A C) ((TensorProduct.lTensor A ↑σ).comp g) φ) = (↑σ).comp ↑((algHomTensorProductEquivPi K Ω A C) g (σ⁻¹ • φ))

Galois equivariance of the splitting. Apply σ ∈ Aut(Ω/K) to the scalar factor of A ⊗[K] Ω. The φ-component of the image of an A-algebra map g : C → A ⊗[K] Ω is σ composed with the σ⁻¹ • φ-component of g.

noncomputable def Algebra.Etale.algHomEquivMulActionHom {K : Type u_1} (Ω : Type u_2) {A : Type u_3} [Field K] [Field Ω] [Algebra K Ω] [Semiring A] [Algebra K A] [IsSepClosed Ω] [IsGalois K Ω] {B : Type u_4} [CommRing B] [Algebra K B] [Etale K B] : (A →ₐ[K] B) ≃ ((B →ₐ[K] Ω) →ₑ[_root_.id] A →ₐ[K] Ω)

Algebra maps into an étale algebra are equivariant maps of points. For a separable closure Ω of K and an étale K-algebra B, precomposition identifies the K-algebra maps A →ₐ[K] B with the Gal(Ω/K)-equivariant maps (B →ₐ[K] Ω) → (A →ₐ[K] Ω) of Ω-valued points (algHomEquivMulActionHom_apply_apply, apply_algHomEquivMulActionHom_symm_apply).

@[simp]

theorem Algebra.Etale.algHomEquivMulActionHom_apply_apply {K : Type u_1} {Ω : Type u_2} {A : Type u_3} [Field K] [Field Ω] [Algebra K Ω] [Semiring A] [Algebra K A] [IsSepClosed Ω] [IsGalois K Ω] {B : Type u_4} [CommRing B] [Algebra K B] [Etale K B] (f : A →ₐ[K] B) (ψ : B →ₐ[K] Ω) : ((algHomEquivMulActionHom Ω) f) ψ = ψ.comp f

The equivariant map of points induced by f : A →ₐ[K] B is precomposition with f.

@[simp]

theorem Algebra.Etale.apply_algHomEquivMulActionHom_symm_apply {K : Type u_1} {Ω : Type u_2} {A : Type u_3} [Field K] [Field Ω] [Algebra K Ω] [Semiring A] [Algebra K A] [IsSepClosed Ω] [IsGalois K Ω] {B : Type u_4} [CommRing B] [Algebra K B] [Etale K B] (u : (B →ₐ[K] Ω) →ₑ[_root_.id] A →ₐ[K] Ω) (ψ : B →ₐ[K] Ω) (a : A) : ψ (((algHomEquivMulActionHom Ω).symm u) a) = (u ψ) a

The algebra map inducing an equivariant map u of points sends a to the element of B at which evaluation is ψ ↦ u ψ a.

noncomputable def TauCeti.galoisFiberAction (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] : CategoryTheory.Functor (CommAlgCat.FiniteEtale K)ᵒᵖ (Action FintypeCat Gal(Ω/K))

The functor sending a finite étale K-algebra A to the finite Gal(Ω/K)-set A →ₐ[K] Ω of its Ω-valued points, with Gal(Ω/K) acting by postcomposition. It lands in the continuous actions (isContinuous_galoisFiberAction_obj), which is recorded by galoisFiber.

@[simp]

theorem TauCeti.galoisFiberAction_obj_ρ_apply (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] (A : (CommAlgCat.FiniteEtale K)ᵒᵖ) (σ : Gal(Ω/K)) (φ : ↑(Opposite.unop A).obj →ₐ[K] Ω) : (CategoryTheory.ConcreteCategory.hom (((galoisFiberAction K Ω).obj A).ρ σ).asHom) φ = σ • φ

Gal(Ω/K) acts on the points of a finite étale K-algebra by postcomposition.

@[simp]

theorem TauCeti.galoisFiberAction_map_hom_apply (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] {A B : (CommAlgCat.FiniteEtale K)ᵒᵖ} (f : A ⟶ B) (φ : ↑(Opposite.unop A).obj →ₐ[K] Ω) : (CategoryTheory.ConcreteCategory.hom ((galoisFiberAction K Ω).map f).hom) φ = φ.comp (CommAlgCat.Hom.hom f.unop.hom)

The map of points induced by a morphism of finite étale K-algebras is precomposition.

theorem TauCeti.isContinuous_galoisFiberAction_obj (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] (A : (CommAlgCat.FiniteEtale K)ᵒᵖ) : Action.isContinuous FintypeCat Gal(Ω/K) ((galoisFiberAction K Ω).obj A)

The Galois action on the points of a finite étale algebra is continuous: it is trivial on the intersection of the finitely many point stabilizers, which is an open subgroup (AlgHom.stabilizer_isOpen).

noncomputable def TauCeti.galoisFiber (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] : CategoryTheory.Functor (CommAlgCat.FiniteEtale K)ᵒᵖ (ContAction FintypeCat Gal(Ω/K))

Finite étale algebras as finite continuous Galois sets. For a field K and a field Ω over K, the functor sending a finite étale K-algebra A to the finite set A →ₐ[K] Ω of its Ω-valued points, with the continuous action of Gal(Ω/K) by postcomposition. When Ω is a separable closure of K it is fully faithful (galoisFiberFullyFaithful).

theorem TauCeti.galoisFiber_comp_forget₂ (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] : (galoisFiber K Ω).comp (CategoryTheory.forget₂ (ContAction FintypeCat Gal(Ω/K)) FintypeCat) = CommAlgCat.FiniteEtale.fiber K Ω

Forgetting the Galois action, galoisFiber K Ω is Mathlib's fibre functor at Ω.

@[simp]

theorem TauCeti.galoisFiber_obj_ρ_apply (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] (A : (CommAlgCat.FiniteEtale K)ᵒᵖ) (σ : Gal(Ω/K)) (φ : ↑(Opposite.unop A).obj →ₐ[K] Ω) : (CategoryTheory.ConcreteCategory.hom (((galoisFiber K Ω).obj A).obj.ρ σ).asHom) φ = σ • φ

Gal(Ω/K) acts on the points of a finite étale K-algebra by postcomposition.

@[simp]

theorem TauCeti.galoisFiber_map_hom_apply (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] {A B : (CommAlgCat.FiniteEtale K)ᵒᵖ} (f : A ⟶ B) (φ : ↑(Opposite.unop A).obj →ₐ[K] Ω) : (CategoryTheory.ConcreteCategory.hom ((galoisFiber K Ω).map f).hom.hom) φ = φ.comp (CommAlgCat.Hom.hom f.unop.hom)

The map of points induced by a morphism of finite étale K-algebras is precomposition.

instance TauCeti.faithful_fiber (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] : (CommAlgCat.FiniteEtale.fiber K Ω).Faithful

The fibre functor at a separably closed field is faithful: the Ω-valued points of a finite étale K-algebra separate its elements (Algebra.Etale.pi_id_injective).

instance TauCeti.instFaithfulOppositeFiniteEtaleContActionFintypeCatFunObjFiniteAlgEquivGaloisFiberOfIsSepClosed (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] : (galoisFiber K Ω).Faithful

instance TauCeti.instFullOppositeFiniteEtaleContActionFintypeCatFunObjFiniteAlgEquivGaloisFiberOfIsSepClosedOfIsGalois (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] : (galoisFiber K Ω).Full

noncomputable def TauCeti.galoisFiberFullyFaithful (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] : (galoisFiber K Ω).FullyFaithful

Finite étale algebras over a field embed into finite continuous Galois sets. For a separable closure Ω of K, sending a finite étale K-algebra to the finite continuous Gal(Ω/K)-set of its Ω-valued points is fully faithful: algebra maps A →ₐ[K] B are the same as Gal(Ω/K)-equivariant maps (B →ₐ[K] Ω) → (A →ₐ[K] Ω).

Every finite continuous Galois set comes from a finite étale algebra

Let X be a finite set with an action of Gal(Ω/K) whose stabilizers are open. The finite étale algebra realising X is the product, over the orbits of X, of the fields Ω ^ stabilizer x fixed by the stabilizer of a chosen point x of the orbit. The point σ • x of X is the embedding σ ∘ (projection to the factor of x); it does not depend on the choice of σ because the stabilizer of x fixes its factor.

theorem TauCeti.exists_mulActionHom_algHom_bijective {K : Type u_1} {Ω : Type v} {X : Type w} [Field K] [Field Ω] [Algebra K Ω] [MulAction Gal(Ω/K) X] [IsGalois K Ω] [Finite X] (hX : ∀ (x : X), IsOpen ↑(MulAction.stabilizer Gal(Ω/K) x)) : ∃ (A : Type (max v w)) (x : CommRing A) (x_1 : Algebra K A) (_ : Algebra.Etale K A) (_ : Module.Finite K A) (f : X →ₑ[id] A →ₐ[K] Ω), Function.Bijective ⇑f

Every finite Galois set with open stabilizers is the set of points of a finite étale algebra. For a Galois extension Ω/K and a finite set X on which Gal(Ω/K) acts with open stabilizers, there are a finite étale K-algebra A and a Gal(Ω/K)-equivariant bijection from X to the Ω-valued points A →ₐ[K] Ω. The algebra A is the product, over the orbits of X, of the fields fixed by the stabilizers of orbit representatives.

instance TauCeti.essSurj_galoisFiber (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsGalois K Ω] : (galoisFiber K Ω).EssSurj

Every finite continuous Galois set is the set of points of a finite étale algebra: for a Galois extension Ω/K, the functor galoisFiber K Ω is essentially surjective.

instance TauCeti.isEquivalence_galoisFiber (K Ω : Type u) [Field K] [Field Ω] [Algebra K Ω] [IsSepClosed Ω] [IsGalois K Ω] : (galoisFiber K Ω).IsEquivalence

Finite étale algebras over a field are finite continuous Galois sets. For a separable closure Ω of K, the functor sending a finite étale K-algebra to the finite continuous Gal(Ω/K)-set of its Ω-valued points is an equivalence of categories (FiniteEtale K)ᵒᵖ ≌ ContAction FintypeCat Gal(Ω/K).