Free relative invariant quotients by finite groups are fppf quotients

Let A be a quasi-coherent commutative 𝒪ₓ-algebra on a scheme X and let a finite group G act on Spec_X(A) by automorphisms over X, through ρ : G →* Aut A. Write Spec_X(A) ⟶ Spec_X(A)/G for the relative invariant quotient projection of TauCeti.AlgebraicGeometry.Quotient.FiniteGroup.Relative.Basic.

When the action is free, in the sense that over every affine open U of X and for every g ≠ 1 the sections g • a - a with a in Γ(A.X, U) generate the unit ideal, the projection is a finite étale G-torsor and Spec_X(A)/G is the fppf quotient. Over each affine open U this is the affine statement (TauCeti.AffineInvariantQuotient.etale_projection, TauCeti.AffineInvariantQuotient.isPullback_of_free). Étaleness is local on the target. The torsor square, which identifies ∐_g Spec_X(A) with Spec_X(A) ×_{Spec_X(A)/G} Spec_X(A), is local on the source of the projection (AlgebraicGeometry.Scheme.isPullback_of_openCover): over the chart Spec Γ(A.X, U), finite coproducts are stable under base change (CategoryTheory.FinitaryPreExtensive.isPullback_sigmaMap_sigmaDesc_id) and the chart of Spec_X(A)/G over U has preimage the chart of Spec_X(A) (CategoryTheory.CommMon.isPullback_projection_relativeSpecπ), so the square restricts to the affine torsor square. The étale surjective projection generates an fppf covering sieve, and the fppf quotient statement follows from the kernel pair by CategoryTheory.IsKernelPair.isColimitYonedaCofork.

Main results

• CommMon.etale_invariantSubalgebraPresheaf_relativeSpecπ_of_free and CommMon.isFinite_invariantSubalgebraPresheaf_relativeSpecπ_of_free: for a free action, the projection is finite étale.
• CommMon.isPullback_invariantSubalgebraPresheaf_relativeSpecπ_of_free: for a free action, ∐_g Spec_X(A) is the kernel pair of the projection.
• CommMon.isColimitInvariantQuotientFppfYonedaCofork: for a free action, Spec_X(A)/G represents the fppf quotient sheaf of Spec_X(A) by G.

References

• M. Demazure and A. Grothendieck, Schémas en groupes (SGA 3), Exposé V, §4 (free actions and fppf quotients).

theorem CategoryTheory.CommMon.etale_invariantSubalgebraPresheaf_relativeSpecπ_of_free {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] [Finite G] [SheafOfModules.IsQuasicoherent A.X] {ρ : G →* Aut A} (hG : ∀ (U : ↑X.affineOpens) (g : G), g ≠ 1 → Ideal.span (Set.range fun (x : ↑(A.X.presheaf.obj (Opposite.op ↑U))) => (sectionsAlgHom (ρ g).asIso.hom ↑U) x - x) = ⊤) : AlgebraicGeometry.Etale (invariantSubalgebraPresheaf ρ).relativeSpecπ

For a free action, the quotient projection Spec_X(A) ⟶ Spec_X(A)/G is étale.

theorem CategoryTheory.CommMon.isFinite_invariantSubalgebraPresheaf_relativeSpecπ_of_free {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] [Finite G] [SheafOfModules.IsQuasicoherent A.X] {ρ : G →* Aut A} (hG : ∀ (U : ↑X.affineOpens) (g : G), g ≠ 1 → Ideal.span (Set.range fun (x : ↑(A.X.presheaf.obj (Opposite.op ↑U))) => (sectionsAlgHom (ρ g).asIso.hom ↑U) x - x) = ⊤) : AlgebraicGeometry.IsFinite (invariantSubalgebraPresheaf ρ).relativeSpecπ

For a free action, the quotient projection Spec_X(A) ⟶ Spec_X(A)/G is finite, with no finiteness hypothesis on Spec_X(A) over X.

theorem CategoryTheory.CommMon.isPullback_invariantSubalgebraPresheaf_relativeSpecπ_of_free {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] [Finite G] [SheafOfModules.IsQuasicoherent A.X] {ρ : G →* Aut A} (hG : ∀ (U : ↑X.affineOpens) (g : G), g ≠ 1 → Ideal.span (Set.range fun (x : ↑(A.X.presheaf.obj (Opposite.op ↑U))) => (sectionsAlgHom (ρ g).asIso.hom ↑U) x - x) = ⊤) : IsPullback (Limits.Sigma.desc fun (x : G) => CategoryStruct.id A.relativeSpec) (Limits.Sigma.desc fun (g : G) => relativeSpecMap (ρ g).asIso.hom) (invariantSubalgebraPresheaf ρ).relativeSpecπ (invariantSubalgebraPresheaf ρ).relativeSpecπ

The torsor square of a free relative quotient. For a free action, the identity and the action of g on the component of g exhibit ∐_g Spec_X(A) as the kernel pair Spec_X(A) ×_{Spec_X(A)/G} Spec_X(A) of the quotient projection.

noncomputable def CategoryTheory.CommMon.isColimitInvariantQuotientFppfYonedaCofork {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] [Finite G] [SheafOfModules.IsQuasicoherent A.X] {ρ : G →* Aut A} (hG : ∀ (U : ↑X.affineOpens) (g : G), g ≠ 1 → Ideal.span (Set.range fun (x : ↑(A.X.presheaf.obj (Opposite.op ↑U))) => (sectionsAlgHom (ρ g).asIso.hom ↑U) x - x) = ⊤) : Limits.IsColimit (Limits.Cofork.ofπ (AlgebraicGeometry.Scheme.fppfTopology.yoneda.map (invariantSubalgebraPresheaf ρ).relativeSpecπ) ⋯)

The fppf quotient of a free relative action. For a free action, under the Yoneda embedding into fppf sheaves, the quotient projection Spec_X(A) ⟶ Spec_X(A)/G is the coequalizer of the two maps ∐_g Spec_X(A) ⇉ Spec_X(A) given by the identity and by the action of g on the component of g. Thus Spec_X(A)/G represents the fppf quotient sheaf of Spec_X(A) by G.