Finite étale torsors under a finite group

Let a finite group G act on a commutative A-algebra B by A-algebra automorphisms. Then B is a finite étale G-torsor over A (TauCeti.Algebra.IsFiniteEtaleTorsor G A B) if B is a finite étale, faithfully flat A-algebra and the Galois map

B ⊗[A] B → (G → B), b ⊗ b' ↦ (b * g • b')_g

(TauCeti.MulSemiringAction.tensorToPi) is bijective. Geometrically, Spec B → Spec A is a torsor under the constant finite group scheme G: it is finite étale and surjective, and Spec B ×_{Spec A} Spec B is the disjoint union of |G| copies of Spec B. Faithful flatness is part of the definition; it excludes the zero algebra over a nonzero ring, which has a bijective Galois map for every G. Over a field, the torsors are the nonzero finite étale algebras with bijective Galois map, and those that are fields are exactly the finite Galois extensions with Galois group G.

Torsors are stable under base change, so a torsor over A gives a torsor over every A-algebra A', for instance over a localization, a residue field or a completion of A. A torsor B' under G' mapping equivariantly from a torsor B under a quotient G of G' is a torsor over B under the kernel. This splits a torsor along a quotient of its group into two stages, A → B under G and B → B' under the kernel, as for a tower of Galois extensions.

Finite étale torsors are the levels of the towers of finite étale covers used to split every finite étale algebra over a ring and to build its universal cover, as in Scholze's construction of the perfectoid cover of an analytic adic space by a tower of finite étale torsors.

Main definitions

• TauCeti.Algebra.IsFiniteEtaleTorsor G A B: B is a finite étale G-torsor over A.

Main results

• TauCeti.Algebra.isFiniteEtaleTorsor_iff: B is a finite étale G-torsor over A if and only if A → B is injective, A is the ring of invariants, and the action is free, i.e. for each g ≠ 1 the elements g • b - b generate the unit ideal (Chase–Harrison–Rosenberg).
• TauCeti.Algebra.IsFiniteEtaleTorsor.isInvariant: the ring of invariants of a torsor is A.
• TauCeti.Algebra.IsFiniteEtaleTorsor.isGaloisGroup: over a nonzero ring, G is a Galois group of B over A in Mathlib's sense.
• TauCeti.Algebra.IsFiniteEtaleTorsor.rankAtStalk_eq_card: a torsor has constant rank |G|.
• TauCeti.Algebra.IsFiniteEtaleTorsor.of_algEquiv: torsors are invariant under G-equivariant isomorphisms of algebras.
• TauCeti.Algebra.IsFiniteEtaleTorsor.baseChange: for every ring map A → A', A' ⊗[A] B is a G-torsor over A', with G acting on the right factor.
• TauCeti.Algebra.IsFiniteEtaleTorsor.of_isPushout: the same for any base change B' of B along A → A' (Algebra.IsPushout A A' B B') with a compatible action of G.
• TauCeti.Algebra.IsFiniteEtaleTorsor.of_surjective: if B is a G-torsor and B' a G'-torsor over A, an A-algebra map B → B' equivariant along a surjection π : G' → G makes B' a torsor over B under the kernel of π.
• TauCeti.Algebra.IsFiniteEtaleTorsor.iff_field: over a field, a torsor is a nonzero finite étale algebra with bijective Galois map.
• TauCeti.Algebra.IsFiniteEtaleTorsor.iff_isGaloisGroup, TauCeti.Algebra.IsFiniteEtaleTorsor.iff_isGalois: for a field extension L / K, L is a G-torsor over K if and only if G is a Galois group of L / K, if and only if L / K is Galois and G maps isomorphically onto Gal(L / K).

References

• S. U. Chase, D. K. Harrison and A. Rosenberg, Galois theory and Galois cohomology of commutative rings, Mem. Amer. Math. Soc. 52 (1965), 15–33, Theorem 1.3.
• P. Scholze, Étale cohomology of diamonds, Lemma 15.3 and the proof of Proposition 15.4.

class TauCeti.Algebra.IsFiniteEtaleTorsor (G : Type u_1) (A : Type u_2) (B : Type u_3) [Group G] [CommRing A] [CommRing B] [Algebra A B] [MulSemiringAction G B] [SMulCommClass G A B] [Finite G] : Prop

B is a finite étale G-torsor over A: a finite étale, faithfully flat A-algebra whose Galois map B ⊗[A] B → (G → B), b ⊗ b' ↦ (b * g • b')_g, is bijective. Geometrically, Spec B → Spec A is a torsor under the constant finite group scheme G.

• etale : Algebra.Etale A B
• finite : Module.Finite A B
• faithfullyFlat : Module.FaithfullyFlat A B
• bijective_tensorToPi : Function.Bijective ⇑(MulSemiringAction.tensorToPi A B G)

instance TauCeti.Algebra.IsFiniteEtaleTorsor.isInvariant {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [CommRing A] [CommRing B] [Algebra A B] [MulSemiringAction G B] [SMulCommClass G A B] [Finite G] [h : IsFiniteEtaleTorsor G A B] : Algebra.IsInvariant A B G

The ring of invariants of a finite étale torsor is the base ring.

theorem TauCeti.Algebra.isFiniteEtaleTorsor_iff {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [CommRing A] [CommRing B] [Algebra A B] [MulSemiringAction G B] [SMulCommClass G A B] [Finite G] : IsFiniteEtaleTorsor G A B ↔ FaithfulSMul A B ∧ Algebra.IsInvariant A B G ∧ ∀ (g : G), g ≠ 1 → Ideal.span (Set.range fun (b : B) => g • b - b) = ⊤

Chase–Harrison–Rosenberg. B is a finite étale G-torsor over A if and only if A → B is injective, A is the ring of invariants, and the action is free: for each g ≠ 1 the elements g • b - b generate the unit ideal of B.

@[instance 100]

instance TauCeti.Algebra.IsFiniteEtaleTorsor.of_subsingleton {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [CommRing A] [CommRing B] [Algebra A B] [MulSemiringAction G B] [SMulCommClass G A B] [Finite G] [Subsingleton A] : IsFiniteEtaleTorsor G A B

Over the zero ring, the zero algebra is a finite étale torsor under every finite group.

instance TauCeti.Algebra.IsFiniteEtaleTorsor.isGaloisGroup {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [CommRing A] [CommRing B] [Algebra A B] [MulSemiringAction G B] [SMulCommClass G A B] [Finite G] [Nontrivial A] [h : IsFiniteEtaleTorsor G A B] : IsGaloisGroup G A B

Over a nonzero ring, a finite étale torsor under G makes G a Galois group of B over A. Over the zero ring this fails for every nontrivial G, whose action is then not faithful.

theorem TauCeti.Algebra.IsFiniteEtaleTorsor.rankAtStalk_eq_card {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [CommRing A] [CommRing B] [Algebra A B] [MulSemiringAction G B] [SMulCommClass G A B] [Finite G] [h : IsFiniteEtaleTorsor G A B] (p : PrimeSpectrum A) : Module.rankAtStalk B p = Nat.card G

A finite étale G-torsor has rank |G| at every prime of the base: its stalk rank Module.rankAtStalk is constantly Nat.card G.

theorem TauCeti.Algebra.IsFiniteEtaleTorsor.of_algEquiv {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [CommRing A] [CommRing B] [Algebra A B] [MulSemiringAction G B] [SMulCommClass G A B] [Finite G] {C : Type u_4} [CommRing C] [Algebra A C] [MulSemiringAction G C] [SMulCommClass G A C] [h : IsFiniteEtaleTorsor G A B] (e : B ≃ₐ[A] C) (he : ∀ (g : G) (b : B), e (g • b) = g • e b) : IsFiniteEtaleTorsor G A C

A G-equivariant isomorphism of algebras carries finite étale G-torsors to finite étale G-torsors.

theorem TauCeti.Algebra.IsFiniteEtaleTorsor.of_isPushout {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [CommRing A] [CommRing B] [Algebra A B] [MulSemiringAction G B] [SMulCommClass G A B] [Finite G] {A' : Type u_4} {B' : Type u_5} [CommRing A'] [CommRing B'] [Algebra A A'] [Algebra A B'] [Algebra A' B'] [Algebra B B'] [IsScalarTower A A' B'] [IsScalarTower A B B'] [Algebra.IsPushout A A' B B'] [MulSemiringAction G B'] [SMulCommClass G A' B'] [h : IsFiniteEtaleTorsor G A B] (hG : ∀ (g : G) (b : B), g • (algebraMap B B') b = (algebraMap B B') (g • b)) : IsFiniteEtaleTorsor G A' B'

Base change of a finite étale torsor along a pushout. Let B be a finite étale G-torsor over A, and let B' be a base change of B along A → A' (Algebra.IsPushout A A' B B'), on which G acts by A'-algebra automorphisms compatibly with its action on B. Then B' is a finite étale G-torsor over A'.

instance TauCeti.Algebra.IsFiniteEtaleTorsor.baseChange {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [CommRing A] [CommRing B] [Algebra A B] [MulSemiringAction G B] [SMulCommClass G A B] [Finite G] (A' : Type u_4) [CommRing A'] [Algebra A A'] [IsFiniteEtaleTorsor G A B] : IsFiniteEtaleTorsor G A' (TensorProduct A A' B)

Base change of a torsor. For every ring map A → A', the base change A' ⊗[A] B of a finite étale G-torsor is a finite étale G-torsor over A', with G acting on the right factor (Algebra.TensorProduct.rightMulSemiringAction). Geometrically, the pullback of a G-torsor Spec B → Spec A along Spec A' → Spec A is a G-torsor.

theorem TauCeti.Algebra.IsFiniteEtaleTorsor.of_surjective {G : Type u_1} {A : Type u_2} {B : Type u_3} [Group G] [CommRing A] [CommRing B] [Algebra A B] [MulSemiringAction G B] [SMulCommClass G A B] [Finite G] {G' : Type u_4} {B' : Type u_5} [Group G'] [CommRing B'] [Algebra A B'] [Algebra B B'] [IsScalarTower A B B'] [MulSemiringAction G' B'] [SMulCommClass G' A B'] [Finite G'] [hB : IsFiniteEtaleTorsor G A B] [hB' : IsFiniteEtaleTorsor G' A B'] {π : G' →* G} (hπs : Function.Surjective ⇑π) (hπ : ∀ (g : G') (b : B), g • (algebraMap B B') b = (algebraMap B B') (π g • b)) : IsFiniteEtaleTorsor (↥π.ker) B B'

A torsor over a torsor along a surjection of groups. Let B be a finite étale G-torsor and B' a finite étale G'-torsor over A, let π : G' → G be surjective, and let B → B' be an A-algebra map equivariant along π. Then B' is a finite étale torsor over B under the kernel of π. In particular B → B' is injective and faithfully flat.

theorem TauCeti.Algebra.IsFiniteEtaleTorsor.iff_field {G : Type u_1} {B : Type u_3} [Group G] [CommRing B] [MulSemiringAction G B] [Finite G] (K : Type u_4) [Field K] [Algebra K B] [SMulCommClass G K B] : IsFiniteEtaleTorsor G K B ↔ Nontrivial B ∧ Module.Finite K B ∧ Algebra.Etale K B ∧ Function.Bijective ⇑(MulSemiringAction.tensorToPi K B G)

Over a field, a finite étale G-torsor is a nonzero finite étale algebra with bijective Galois map. The algebra may be disconnected, and the characteristic may divide |G|.

theorem TauCeti.Algebra.IsFiniteEtaleTorsor.iff_isGaloisGroup {G : Type u_1} [Group G] [Finite G] {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [SMulCommClass G K L] : IsFiniteEtaleTorsor G K L ↔ IsGaloisGroup G K L

For a field extension L / K, L is a finite étale G-torsor over K exactly when G is a Galois group of L / K.

theorem TauCeti.Algebra.IsFiniteEtaleTorsor.iff_isGalois {G : Type u_1} [Group G] [Finite G] {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K L] [MulSemiringAction G L] [SMulCommClass G K L] : IsFiniteEtaleTorsor G K L ↔ IsGalois K L ∧ Function.Bijective ⇑(MulSemiringAction.toAlgAut G K L)

For a field extension L / K, L is a finite étale G-torsor over K exactly when L / K is Galois and the action identifies G with Gal(L / K).

instance TauCeti.Algebra.IsFiniteEtaleTorsor.of_isGalois (K : Type u_6) (L : Type u_7) [Field K] [Field L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] : IsFiniteEtaleTorsor Gal(L/K) K L

A finite Galois extension L / K is a finite étale torsor under its Galois group.