The torsor square of a free finite-group quotient

For a finite group G acting on a commutative ring A, the action graphs give a canonical map from the disjoint union of copies of Spec A to Spec A ×_{Spec Aᴳ} Spec A. This map is an isomorphism exactly when the action is free scheme-theoretically: for each g ≠ 1, the differences g • a - a generate the unit ideal.

Together with the finite étale surjectivity of the invariant-spectrum projection, this identifies the quotient as a torsor under the constant group scheme. The pullback square isPullback_of_free records both maps of its action relation, so it can be used for descent without replacing scheme morphisms by geometric points. In particular, over a disconnected test scheme the group element relating two lifts can vary between components. The same square, with the components reindexed by g ↦ g⁻¹, is isPullback_specAction_of_free, stated with the covariant action specAction A G g; this is the form that matches an action of G on a scheme by automorphisms.

The proof uses the existing Chase–Harrison–Rosenberg isomorphism TauCeti.MulSemiringAction.tensorToPi_bijective, Mathlib's sigmaSpec, and pullbackSpecIso. No reducedness, finite-type or invertible-order hypothesis is required.

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.
• M. Demazure and A. Grothendieck, Schémas en groupes (SGA 3), Exposé V, §4.

theorem TauCeti.AffineInvariantQuotient.isIso_actionMap_iff (A : Type u) (G : Type v) [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] : CategoryTheory.IsIso (actionMap A G) ↔ ∀ (g : G), g ≠ 1 → Ideal.span (Set.range fun (a : A) => g • a - a) = ⊤

The torsor criterion for an affine finite-group quotient. The action relation is the kernel pair of the quotient projection exactly when every nonidentity element has empty scheme-theoretic fixed locus.

theorem TauCeti.AffineInvariantQuotient.isPullback_of_free (A : Type u) (G : Type v) [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] (hG : ∀ (g : G), g ≠ 1 → Ideal.span (Set.range fun (a : A) => g • a - a) = ⊤) : CategoryTheory.IsPullback (CategoryTheory.Limits.Sigma.desc fun (x : G) => CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧A)) (CategoryTheory.Limits.Sigma.desc fun (g : G) => specComap A G g) (projection A G) (projection A G)

The torsor square. For a free finite-group action, the two maps from the disjoint union of copies of Spec A exhibit the kernel pair of the finite étale quotient projection.

theorem TauCeti.AffineInvariantQuotient.isPullback_specAction_of_free (A : Type u) (G : Type v) [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] (hG : ∀ (g : G), g ≠ 1 → Ideal.span (Set.range fun (a : A) => g • a - a) = ⊤) : CategoryTheory.IsPullback (CategoryTheory.Limits.Sigma.desc fun (x : G) => CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧A)) (CategoryTheory.Limits.Sigma.desc fun (g : G) => ((specAction A G) g).asIso.hom) (projection A G) (projection A G)

The torsor square, in terms of the covariant action. For a free finite-group action, the identity and the automorphism specAction A G g on the component of g exhibit the disjoint union of copies of Spec A as the kernel pair of the quotient projection.