The universal property of the affine invariant quotient by a finite group

Let a finite group G act on a commutative ring A. This file shows that the invariant-spectrum projection π : Spec A ⟶ Spec Aᴳ is a categorical quotient in the category of all schemes: every morphism f : Spec A ⟶ X to an arbitrary scheme X which is invariant under the action of G factors uniquely through π. The case of an affine X, where only a monoid action is needed, is TauCeti.AffineInvariantQuotient.existsUnique_desc.

Uniqueness holds because π is an epimorphism of schemes: it is surjective, and its stalk maps (Aᴳ)_P → A_Q are injective (TauCeti.FixedPoints.localRingHom_injective).

For existence, f is constant on the fibres of π, which are the G-orbits, so it descends to a continuous map b : Spec Aᴳ → X because π is a topological quotient map. Cover Spec Aᴳ by basic opens D(r) with r invariant and b(D(r)) inside an affine open V of X. Over D(r), the projection is the affine invariant quotient of the localization A[1/r]: invariants commute with this localization (TauCeti.FixedPoints.isLocalization), so the square formed by Spec A[1/r] ⟶ Spec A, the two projections and Spec A[1/r]ᴳ ⟶ Spec Aᴳ is a pullback square (TauCeti.AffineInvariantQuotient.isPullback_away). The restriction of f to Spec A[1/r] lands in V, so it descends by the affine universal property. The local descents agree on overlaps because π remains an epimorphism over every open subscheme of Spec Aᴳ, and they glue (AlgebraicGeometry.Scheme.Hom.exists_comp_eq_of_openCover).

The construction follows the proof of Mathlib's AlgebraicGeometry.isRegularEpi_of_flat_of_surjective_of_isAffine, where flat descent plays the role of the affine invariant quotient.

Main definitions

• TauCeti.AffineInvariantQuotient.descOfFinite: the morphism Spec Aᴳ ⟶ X induced by an invariant morphism Spec A ⟶ X.

Main results

• TauCeti.AffineInvariantQuotient.stalkMap_projection_injective: the stalk maps of the projection are injective.
• TauCeti.AffineInvariantQuotient.instEpiProjection: the projection is an epimorphism of schemes.
• TauCeti.AffineInvariantQuotient.isPullback_away: over the basic open D(r), the projection is the projection of A[1/r].
• TauCeti.AffineInvariantQuotient.hom_ext_of_finite: morphisms out of the quotient to an arbitrary scheme are determined by their composition with the projection.
• TauCeti.AffineInvariantQuotient.existsUnique_desc_of_finite: the universal property for arbitrary target schemes.

References

• M. Demazure and A. Grothendieck, Schémas en groupes (SGA 3), Exposé V, §1.
• D. Mumford, Abelian Varieties, §7, Theorem 1.

theorem TauCeti.AffineInvariantQuotient.stalkMap_projection_injective (A : Type u) (G : Type v) [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] (x : ↥(AlgebraicGeometry.Spec ↧A)) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap (projection A G) x))

The stalk maps (Aᴳ)_P → A_Q of the invariant-spectrum projection are injective for a finite group action.

instance TauCeti.AffineInvariantQuotient.instEpiProjection (A : Type u) (G : Type v) [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] : CategoryTheory.Epi (projection A G)

The invariant-spectrum projection of a finite group action is an epimorphism of schemes.

theorem TauCeti.AffineInvariantQuotient.isPullback_away {A : Type u} (G : Type v) [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] (r : ↥(FixedPoints.subring A G)) : CategoryTheory.IsPullback (AlgebraicGeometry.Spec.algebraMap A (Localization (Algebra.algebraMapSubmonoid A (Submonoid.powers r)))) (projection (Localization (Algebra.algebraMapSubmonoid A (Submonoid.powers r))) G) (projection A G) (AlgebraicGeometry.Spec.algebraMap ↥(FixedPoints.subring A G) ↥(FixedPoints.subring (Localization (Algebra.algebraMapSubmonoid A (Submonoid.powers r))) G))

Over the basic open D(r) of an invariant r, the invariant-spectrum projection is the projection of the localization A[1/r]: the square formed by the two projections and the maps induced by A → A[1/r] and Aᴳ → A[1/r]ᴳ is a pullback square.

instance TauCeti.AffineInvariantQuotient.isOpenImmersion_away {A : Type u} (G : Type v) [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] (r : ↥(FixedPoints.subring A G)) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.algebraMap ↥(FixedPoints.subring A G) ↥(FixedPoints.subring (Localization (Algebra.algebraMapSubmonoid A (Submonoid.powers r))) G))

The map Spec A[1/r]ᴳ ⟶ Spec Aᴳ is an open immersion.

theorem TauCeti.AffineInvariantQuotient.range_specAlgebraMap_away {A : Type u} (G : Type v) [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] (r : ↥(FixedPoints.subring A G)) : Set.range ⇑(AlgebraicGeometry.Spec.algebraMap ↥(FixedPoints.subring A G) ↥(FixedPoints.subring (Localization (Algebra.algebraMapSubmonoid A (Submonoid.powers r))) G)) = ↑(PrimeSpectrum.basicOpen r)

The image of Spec A[1/r]ᴳ ⟶ Spec Aᴳ is the basic open D(r).

theorem TauCeti.AffineInvariantQuotient.specComap_comp_specAlgebraMap_away {A : Type u} {G : Type v} [CommRing A] [Group G] [MulSemiringAction G A] (r : ↥(FixedPoints.subring A G)) (g : G) : CategoryTheory.CategoryStruct.comp (specComap (Localization (Algebra.algebraMapSubmonoid A (Submonoid.powers r))) G g) (AlgebraicGeometry.Spec.algebraMap A (Localization (Algebra.algebraMapSubmonoid A (Submonoid.powers r)))) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.algebraMap A (Localization (Algebra.algebraMapSubmonoid A (Submonoid.powers r)))) (specComap A G g)

The map Spec A[1/r] ⟶ Spec A is equivariant.

theorem TauCeti.AffineInvariantQuotient.specComap_comp_specAlgebraMap_away_assoc {A : Type u} {G : Type v} [CommRing A] [Group G] [MulSemiringAction G A] (r : ↥(FixedPoints.subring A G)) (g : G) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧A ⟶ Z) : CategoryTheory.CategoryStruct.comp (specComap (Localization (Algebra.algebraMapSubmonoid A (Submonoid.powers r))) G g) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.algebraMap A (Localization (Algebra.algebraMapSubmonoid A (Submonoid.powers r)))) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.algebraMap A (Localization (Algebra.algebraMapSubmonoid A (Submonoid.powers r)))) (CategoryTheory.CategoryStruct.comp (specComap A G g) h)

The map Spec A[1/r] ⟶ Spec A is equivariant.

noncomputable def TauCeti.AffineInvariantQuotient.descOfFinite {A : Type u} {G : Type v} [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] {X : AlgebraicGeometry.Scheme} (f : AlgebraicGeometry.Spec ↧A ⟶ X) (hf : ∀ (g : G), CategoryTheory.CategoryStruct.comp (specComap A G g) f = f) : quotient A G ⟶ X

The morphism Spec Aᴳ ⟶ X induced by a G-invariant morphism Spec A ⟶ X to an arbitrary scheme, for a finite group G.

theorem TauCeti.AffineInvariantQuotient.hom_ext_of_finite {A : Type u} {G : Type v} [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] {X : AlgebraicGeometry.Scheme} {f h : quotient A G ⟶ X} (e : CategoryTheory.CategoryStruct.comp (projection A G) f = CategoryTheory.CategoryStruct.comp (projection A G) h) : f = h

Morphisms from the invariant quotient by a finite group to an arbitrary scheme are determined by their composition with the projection.

theorem TauCeti.AffineInvariantQuotient.hom_ext_of_finite_iff {A : Type u} {G : Type v} [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] {X : AlgebraicGeometry.Scheme} {f h : quotient A G ⟶ X} : f = h ↔ CategoryTheory.CategoryStruct.comp (projection A G) f = CategoryTheory.CategoryStruct.comp (projection A G) h

@[simp]

theorem TauCeti.AffineInvariantQuotient.projection_descOfFinite {A : Type u} {G : Type v} [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] {X : AlgebraicGeometry.Scheme} (f : AlgebraicGeometry.Spec ↧A ⟶ X) (hf : ∀ (g : G), CategoryTheory.CategoryStruct.comp (specComap A G g) f = f) : CategoryTheory.CategoryStruct.comp (projection A G) (descOfFinite f hf) = f

The induced morphism factors the given invariant morphism.

@[simp]

theorem TauCeti.AffineInvariantQuotient.projection_descOfFinite_assoc {A : Type u} {G : Type v} [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] {X : AlgebraicGeometry.Scheme} (f : AlgebraicGeometry.Spec ↧A ⟶ X) (hf : ∀ (g : G), CategoryTheory.CategoryStruct.comp (specComap A G g) f = f) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (projection A G) (CategoryTheory.CategoryStruct.comp (descOfFinite f hf) h) = CategoryTheory.CategoryStruct.comp f h

The induced morphism factors the given invariant morphism.

theorem TauCeti.AffineInvariantQuotient.existsUnique_desc_of_finite {A : Type u} {G : Type v} [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] {X : AlgebraicGeometry.Scheme} (f : AlgebraicGeometry.Spec ↧A ⟶ X) (hf : ∀ (g : G), CategoryTheory.CategoryStruct.comp (specComap A G g) f = f) : ∃! h : quotient A G ⟶ X, CategoryTheory.CategoryStruct.comp (projection A G) h = f

The universal property of the affine invariant quotient by a finite group. Every G-invariant morphism from Spec A to an arbitrary scheme factors uniquely through the projection Spec A ⟶ Spec Aᴳ.

@[simp]

theorem TauCeti.AffineInvariantQuotient.descOfFinite_projection {A : Type u} {G : Type v} [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] {X : AlgebraicGeometry.Scheme} (f : quotient A G ⟶ X) : descOfFinite (CategoryTheory.CategoryStruct.comp (projection A G) f) ⋯ = f

Descending the composite of the projection with a morphism to an arbitrary scheme recovers that morphism.

theorem TauCeti.AffineInvariantQuotient.descOfFinite_eq_desc {A : Type u} {G : Type v} [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] (f : AlgebraicGeometry.Spec ↧A ⟶ X) (hf : ∀ (g : G), CategoryTheory.CategoryStruct.comp (specComap A G g) f = f) : descOfFinite f hf = desc f hf

For an affine target, descOfFinite is the affine descent desc.