Relative invariant quotients by finite groups

Let A be a quasi-coherent commutative 𝒪ₓ-algebra on a scheme X, so that Y = Spec_X(A) is an arbitrary scheme affine over X, and let a finite group G act on A by algebra automorphisms ρ : G →* Aut A, that is, on Y by automorphisms over X. This file constructs the quotient Y/G over X by gluing the affine invariant quotients over the affine opens of X.

Over each open U of X, the sections of A fixed by every g : G form a Γ(X, U)-subalgebra CommMon.invariantSections ρ U of Γ(A.X, U). Over a basic open X.basicOpen r of an affine open U, these invariants are the localization away from r of the invariants over U: a section x / rⁿ fixed by every g satisfies rᵐ (g • x - x) = 0 for some m depending on g, and since G is finite a single m works for all g, so that rᵐ x is invariant. Hence the presheaf of invariant subalgebras Q = CommMon.invariantSubalgebraPresheaf ρ is coequifibered, and the affine schemes Spec (CommMon.invariantSections ρ U) glue, with Mathlib's relative gluing on the small affine Zariski site, to its relative spectrum Q.relativeSpec, affine over X (CommMon.SubalgebraPresheaf.relativeSpec). The inclusions of the invariants glue to the quotient projection Q.relativeSpecπ : Spec_X(A) ⟶ Q.relativeSpec over X, which is invariant under the action of G on Spec_X(A).

Over every affine open U of X, the projection is the affine invariant quotient Spec Γ(A.X, U) ⟶ Spec Γ(A.X, U)ᴳ (CommMon.SubalgebraPresheaf.isPullback_relativeSpecπ). Since G is finite, Γ(A.X, U) is integral over its invariants, so the projection is integral and surjective, and it is finite when Spec_X(A) is of finite type over X. Without freeness, flatness of the projection can fail; for free actions the projection is finite étale (TauCeti.AlgebraicGeometry.Quotient.FiniteGroup.Relative.Fppf).

The construction needs no hypothesis on X, and in particular the quotient of a scheme affine over a non-affine base is obtained without choosing a global invariant affine cover: the preimages of the affine opens of X form one.

The projection is a categorical quotient in the category of all schemes: every G-invariant morphism f : Spec_X(A) ⟶ Z to an arbitrary scheme Z factors uniquely through it (CommMon.existsUnique_relativeSpecπ_comp_eq). Over each affine open U of X, the base change of f descends by the universal property of the affine invariant quotient, TauCeti.AffineInvariantQuotient.existsUnique_desc_of_finite. The stalk maps of the projection are injective, because they are on each affine chart, so the projection stays an epimorphism after base change to every open subscheme of Spec_X(A)/G; hence the local descents agree on overlaps and glue (AlgebraicGeometry.Scheme.Hom.exists_comp_eq_of_openCover).

The points of the quotient with values in a field are the orbits of G on such points of Spec_X(A): a point of Spec_X(A) with values in a field lies over a single affine open U of X, hence factors through the chart Spec Γ(A.X, U), where this is the affine statement TauCeti.AffineInvariantQuotient.exists_comp_specComap_eq.

The localization statement is a case of TauCeti.FixedPoints.isLocalization_of_mem_range_iff, which also gives TauCeti.FixedPoints.isLocalization, and the gluing is the relative spectrum of a presheaf of subalgebras, which also gives the relative spectrum of an equalizer, CommMon.equalizerSubalgebraPresheaf.

Main definitions

• CommMon.sectionsAction ρ U: the action of G on Γ(A.X, U) by Γ(X, U)-algebra automorphisms.
• CommMon.sectionsMulSemiringAction ρ U: the same action as a MulSemiringAction, not an instance since it depends on ρ.
• CommMon.invariantSections ρ U: the invariant sections over U, which are FixedPoints.subalgebra Γ(X, U) Γ(A.X, U) G for that action (CommMon.invariantSections_eq_fixedPoints).
• CommMon.invariantSubalgebraPresheaf ρ: the presheaf of invariant subalgebras, whose relative spectrum is the relative invariant quotient Spec_X(A)/G and whose relativeSpecπ is the quotient projection.
• CommMon.quotientIsoSpecInvariantSections ρ U: the identification of the affine invariant quotient of Γ(A.X, U) with the spectrum of the invariant sections over U.
• CommMon.invariantQuotientDesc f hf: the morphism Spec_X(A)/G ⟶ Z induced by a G-invariant morphism f : Spec_X(A) ⟶ Z.

Main results

• CommMon.isLocalization_invariantSections_basicOpen: invariants commute with localization at a basic open of an affine open, so that CommMon.invariantSubalgebraPresheaf ρ is coequifibered (CommMon.isCoequifibered_invariantSubalgebraPresheaf).
• CommMon.relativeSpecMap_invariantSubalgebraPresheaf_relativeSpecπ: the projection is G-invariant.
• CommMon.isPullback_projection_relativeSpecπ: over an affine open U of X, the projection restricts to the affine invariant quotient projection of Γ(A.X, U).
• CommMon.isIntegral_invariantSections: the sections are integral over the invariant sections.
• The projection is integral and surjective, and CommMon.isFinite_invariantSubalgebraPresheaf_relativeSpecπ: it is finite when Spec_X(A) is locally of finite type over X.
• CommMon.stalkMap_invariantSubalgebraPresheaf_relativeSpecπ_injective: the stalk maps of the projection are injective, so the projection is an epimorphism of schemes.
• CommMon.existsUnique_relativeSpecπ_comp_eq: the universal property of the quotient for arbitrary target schemes.
• CommMon.exists_comp_relativeSpecMap_eq: two points of Spec_X(A) with values in a field and the same image in the quotient differ by the action of an element of G.

References

• M. Demazure and A. Grothendieck, Schémas en groupes (SGA 3), Exposé V, §1 (quotients of affine schemes by finite groups).
• D. Mumford, Abelian Varieties, §7, Theorem 1 (quotients by finite groups as categorical quotients).
• The Stacks Project, Tag 01LL (relative spectrum via gluing).

noncomputable def CategoryTheory.CommMon.sectionsAction {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) (U : X.Opens) : G →* ↑(A.X.presheaf.obj (Opposite.op U)) ≃ₐ[↑(X.presheaf.obj (Opposite.op U))] ↑(A.X.presheaf.obj (Opposite.op U))

The action of G on the sections of A over U through ρ, by Γ(X, U)-algebra automorphisms.

@[simp]

theorem CategoryTheory.CommMon.sectionsAction_apply {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) (U : X.Opens) (g : G) (x : ↑(A.X.presheaf.obj (Opposite.op U))) : ((sectionsAction ρ U) g) x = (sectionsAlgHom (ρ g).asIso.hom U) x

@[instance_reducible]

noncomputable def CategoryTheory.CommMon.sectionsMulSemiringAction {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) (U : X.Opens) : MulSemiringAction G ↑(A.X.presheaf.obj (Opposite.op U))

The action of G on the sections of A over U through ρ, as a MulSemiringAction. It is not an instance, since ρ does not occur in the type Γ(A.X, U).

@[simp]

theorem CategoryTheory.CommMon.sectionsMulSemiringAction_smul {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) (U : X.Opens) (g : G) (x : ↑(A.X.presheaf.obj (Opposite.op U))) : g • x = (sectionsAlgHom (ρ g).asIso.hom U) x

theorem CategoryTheory.CommMon.smulCommClass_sectionsMulSemiringAction {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) (U : X.Opens) : SMulCommClass G ↑(X.presheaf.obj (Opposite.op U)) ↑(A.X.presheaf.obj (Opposite.op U))

The action of G on the sections over U commutes with the action of Γ(X, U).

noncomputable def CategoryTheory.CommMon.invariantSections {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) (U : X.Opens) : Subalgebra ↑(X.presheaf.obj (Opposite.op U)) ↑(A.X.presheaf.obj (Opposite.op U))

The Γ(X, U)-subalgebra of sections of A over U fixed by every element of G.

@[simp]

theorem CategoryTheory.CommMon.mem_invariantSections {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] {ρ : G →* Aut A} {U : X.Opens} {x : ↑(A.X.presheaf.obj (Opposite.op U))} : x ∈ invariantSections ρ U ↔ ∀ (g : G), (sectionsAlgHom (ρ g).asIso.hom U) x = x

theorem CategoryTheory.CommMon.invariantSections_eq_fixedPoints {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) (U : X.Opens) : invariantSections ρ U = FixedPoints.subalgebra (↑(X.presheaf.obj (Opposite.op U))) (↑(A.X.presheaf.obj (Opposite.op U))) G

The invariant sections over U are the fixed points of sectionsMulSemiringAction ρ U, the form in which the affine invariant quotient AffineInvariantQuotient is stated.

theorem CategoryTheory.CommMon.restrictSections_mem_invariantSections {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) {U V : X.Opens} (i : V ⟶ U) {x : ↑(A.X.presheaf.obj (Opposite.op U))} (hx : x ∈ invariantSections ρ U) : (A.restrictSections i) x ∈ invariantSections ρ V

Restriction of sections preserves invariant sections.

noncomputable def CategoryTheory.CommMon.invariantSubalgebraPresheaf {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) : A.SubalgebraPresheaf

The presheaf of subalgebras of invariant sections of A.

@[simp]

theorem CategoryTheory.CommMon.invariantSubalgebraPresheaf_sections {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) (U : X.Opens) : (invariantSubalgebraPresheaf ρ).sections U = invariantSections ρ U

noncomputable def CategoryTheory.CommMon.quotientIsoSpecInvariantSections {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) (U : X.Opens) : TauCeti.AffineInvariantQuotient.quotient (↑(A.X.presheaf.obj (Opposite.op U))) G ≅ AlgebraicGeometry.Spec ↧↥((invariantSubalgebraPresheaf ρ).sections U)

The spectrum of the invariant sections over U, the chart of the quotient over U, is the affine invariant quotient of the sections, through the identification of the invariant sections with the fixed subalgebra.

theorem CategoryTheory.CommMon.specMap_invariantSections {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] {ρ : G →* Aut A} (U : X.Opens) : AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap ↥((invariantSubalgebraPresheaf ρ).sections U) ↑(A.X.presheaf.obj (Opposite.op U)))) = CategoryStruct.comp (TauCeti.AffineInvariantQuotient.projection (↑(A.X.presheaf.obj (Opposite.op U))) G) (quotientIsoSpecInvariantSections ρ U).hom

Spec of the inclusion of the invariant sections over U is the affine invariant quotient projection of the sections over U, up to quotientIsoSpecInvariantSections.

theorem CategoryTheory.CommMon.isLocalization_invariantSections_basicOpen {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) [Finite G] [SheafOfModules.IsQuasicoherent A.X] {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (r : ↑(X.presheaf.obj (Opposite.op U))) : IsLocalization.Away ((algebraMap ↑(X.presheaf.obj (Opposite.op U)) ↥(invariantSections ρ U)) r) ↥(invariantSections ρ (X.basicOpen r))

Over the basic open X.basicOpen r of an affine open U, the invariant sections of A are the localization away from r of those over U. This is the counterpart of CommMon.isLocalization_basicOpen for invariants, and uses that G is finite.

instance CategoryTheory.CommMon.isCoequifibered_invariantSubalgebraPresheaf {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) [Finite G] [SheafOfModules.IsQuasicoherent A.X] : (invariantSubalgebraPresheaf ρ).IsCoequifibered

On the affine opens of X, the presheaf of invariant sections is coequifibered over the structure presheaf: its sections over basic opens are localizations.

instance CategoryTheory.CommMon.isIntegral_invariantSections {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) [Finite G] (U : X.Opens) : Algebra.IsIntegral ↥(invariantSections ρ U) ↑(A.X.presheaf.obj (Opposite.op U))

The sections of A are integral over the invariant sections, since G is finite.

@[simp]

theorem CategoryTheory.CommMon.relativeSpecMap_invariantSubalgebraPresheaf_relativeSpecπ {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) [Finite G] [SheafOfModules.IsQuasicoherent A.X] (g : G) : CategoryStruct.comp (relativeSpecMap (ρ g).asIso.hom) (invariantSubalgebraPresheaf ρ).relativeSpecπ = (invariantSubalgebraPresheaf ρ).relativeSpecπ

The quotient projection Spec_X(A) ⟶ Spec_X(A)/G is invariant under the action of G on Spec_X(A).

@[simp]

theorem CategoryTheory.CommMon.relativeSpecMap_invariantSubalgebraPresheaf_relativeSpecπ_assoc {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) [Finite G] [SheafOfModules.IsQuasicoherent A.X] (g : G) {Z : AlgebraicGeometry.Scheme} (h : (invariantSubalgebraPresheaf ρ).relativeSpec ⟶ Z) : CategoryStruct.comp (relativeSpecMap (ρ g).asIso.hom) (CategoryStruct.comp (invariantSubalgebraPresheaf ρ).relativeSpecπ h) = CategoryStruct.comp (invariantSubalgebraPresheaf ρ).relativeSpecπ h

The quotient projection Spec_X(A) ⟶ Spec_X(A)/G is invariant under the action of G on Spec_X(A).

instance CategoryTheory.CommMon.instIsIntegralHomRelativeSpecπInvariantSubalgebraPresheaf {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) [Finite G] [SheafOfModules.IsQuasicoherent A.X] : AlgebraicGeometry.IsIntegralHom (invariantSubalgebraPresheaf ρ).relativeSpecπ

The quotient projection is integral.

instance CategoryTheory.CommMon.instSurjectiveRelativeSpecπInvariantSubalgebraPresheaf {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) [Finite G] [SheafOfModules.IsQuasicoherent A.X] : AlgebraicGeometry.Surjective (invariantSubalgebraPresheaf ρ).relativeSpecπ

The quotient projection is surjective.

instance CategoryTheory.CommMon.isFinite_invariantSubalgebraPresheaf_relativeSpecπ {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] (ρ : G →* Aut A) [Finite G] [SheafOfModules.IsQuasicoherent A.X] [AlgebraicGeometry.LocallyOfFiniteType A.relativeSpecToBase] : AlgebraicGeometry.IsFinite (invariantSubalgebraPresheaf ρ).relativeSpecπ

The quotient projection is finite when Spec_X(A) is locally of finite type over X.

The universal property of the quotient

theorem CategoryTheory.CommMon.isPullback_projection_relativeSpecπ {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] {ρ : G →* Aut A} [Finite G] [SheafOfModules.IsQuasicoherent A.X] (U : X.AffineZariskiSite) : IsPullback (CategoryStruct.comp (TauCeti.AffineInvariantQuotient.projection (↑(A.X.presheaf.obj (Opposite.op U.toOpens))) G) (quotientIsoSpecInvariantSections ρ U.toOpens).hom) (A.relativeSpecCover.f U) ((invariantSubalgebraPresheaf ρ).relativeSpecCover.f U) (invariantSubalgebraPresheaf ρ).relativeSpecπ

Over an affine open U of X, the quotient projection is the affine invariant quotient projection of the sections over U.

theorem CategoryTheory.CommMon.specComap_relativeSpecCover_f {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] {ρ : G →* Aut A} [SheafOfModules.IsQuasicoherent A.X] (U : X.AffineZariskiSite) (g : G) : CategoryStruct.comp (TauCeti.AffineInvariantQuotient.specComap (↑(A.X.presheaf.obj (Opposite.op U.toOpens))) G g) (A.relativeSpecCover.f U) = CategoryStruct.comp (A.relativeSpecCover.f U) (relativeSpecMap (ρ g).asIso.hom)

On an affine chart, the action of g on Spec_X(A) is the action on the spectrum of the sections.

theorem CategoryTheory.CommMon.exists_comp_relativeSpecMap_eq {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] {ρ : G →* Aut A} [Finite G] [SheafOfModules.IsQuasicoherent A.X] {K : Type u} [Field K] {x₁ x₂ : AlgebraicGeometry.Spec ↧K ⟶ A.relativeSpec} (h : CategoryStruct.comp x₁ (invariantSubalgebraPresheaf ρ).relativeSpecπ = CategoryStruct.comp x₂ (invariantSubalgebraPresheaf ρ).relativeSpecπ) : ∃ (g : G), CategoryStruct.comp x₁ (relativeSpecMap (ρ g).asIso.hom) = x₂

Points of the relative invariant quotient are orbits. Two morphisms from the spectrum of a field to Spec_X(A) with the same image in Spec_X(A)/G differ by the action of an element of G.

theorem CategoryTheory.CommMon.stalkMap_invariantSubalgebraPresheaf_relativeSpecπ_injective {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] {ρ : G →* Aut A} [Finite G] [SheafOfModules.IsQuasicoherent A.X] (x : ↥A.relativeSpec) : Function.Injective ⇑(ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap (invariantSubalgebraPresheaf ρ).relativeSpecπ x))

The stalk maps of the quotient projection Spec_X(A) ⟶ Spec_X(A)/G are injective.

instance CategoryTheory.CommMon.instEpiSchemeRelativeSpecπInvariantSubalgebraPresheaf {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] {ρ : G →* Aut A} [Finite G] [SheafOfModules.IsQuasicoherent A.X] : Epi (invariantSubalgebraPresheaf ρ).relativeSpecπ

The quotient projection Spec_X(A) ⟶ Spec_X(A)/G is an epimorphism of schemes.

noncomputable def CategoryTheory.CommMon.invariantQuotientDesc {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] {ρ : G →* Aut A} [Finite G] [SheafOfModules.IsQuasicoherent A.X] {Z : AlgebraicGeometry.Scheme} (f : A.relativeSpec ⟶ Z) (hf : ∀ (g : G), CategoryStruct.comp (relativeSpecMap (ρ g).asIso.hom) f = f) : (invariantSubalgebraPresheaf ρ).relativeSpec ⟶ Z

The morphism Spec_X(A)/G ⟶ Z induced by a G-invariant morphism Spec_X(A) ⟶ Z to an arbitrary scheme.

@[simp]

theorem CategoryTheory.CommMon.relativeSpecπ_invariantQuotientDesc {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] {ρ : G →* Aut A} [Finite G] [SheafOfModules.IsQuasicoherent A.X] {Z : AlgebraicGeometry.Scheme} (f : A.relativeSpec ⟶ Z) (hf : ∀ (g : G), CategoryStruct.comp (relativeSpecMap (ρ g).asIso.hom) f = f) : CategoryStruct.comp (invariantSubalgebraPresheaf ρ).relativeSpecπ (invariantQuotientDesc f hf) = f

The induced morphism factors the given invariant morphism through the quotient projection.

@[simp]

theorem CategoryTheory.CommMon.relativeSpecπ_invariantQuotientDesc_assoc {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] {ρ : G →* Aut A} [Finite G] [SheafOfModules.IsQuasicoherent A.X] {Z : AlgebraicGeometry.Scheme} (f : A.relativeSpec ⟶ Z) (hf : ∀ (g : G), CategoryStruct.comp (relativeSpecMap (ρ g).asIso.hom) f = f) {Z✝ : AlgebraicGeometry.Scheme} (h : Z ⟶ Z✝) : CategoryStruct.comp (invariantSubalgebraPresheaf ρ).relativeSpecπ (CategoryStruct.comp (invariantQuotientDesc f hf) h) = CategoryStruct.comp f h

The induced morphism factors the given invariant morphism through the quotient projection.

theorem CategoryTheory.CommMon.invariantQuotient_hom_ext {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] {ρ : G →* Aut A} [Finite G] [SheafOfModules.IsQuasicoherent A.X] {Z : AlgebraicGeometry.Scheme} {h₁ h₂ : (invariantSubalgebraPresheaf ρ).relativeSpec ⟶ Z} (e : CategoryStruct.comp (invariantSubalgebraPresheaf ρ).relativeSpecπ h₁ = CategoryStruct.comp (invariantSubalgebraPresheaf ρ).relativeSpecπ h₂) : h₁ = h₂

Morphisms from the quotient Spec_X(A)/G to an arbitrary scheme are determined by their composition with the quotient projection.

theorem CategoryTheory.CommMon.invariantQuotient_hom_ext_iff {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] {ρ : G →* Aut A} [Finite G] [SheafOfModules.IsQuasicoherent A.X] {Z : AlgebraicGeometry.Scheme} {h₁ h₂ : (invariantSubalgebraPresheaf ρ).relativeSpec ⟶ Z} : h₁ = h₂ ↔ CategoryStruct.comp (invariantSubalgebraPresheaf ρ).relativeSpecπ h₁ = CategoryStruct.comp (invariantSubalgebraPresheaf ρ).relativeSpecπ h₂

theorem CategoryTheory.CommMon.existsUnique_relativeSpecπ_comp_eq {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] {ρ : G →* Aut A} [Finite G] [SheafOfModules.IsQuasicoherent A.X] {Z : AlgebraicGeometry.Scheme} (f : A.relativeSpec ⟶ Z) (hf : ∀ (g : G), CategoryStruct.comp (relativeSpecMap (ρ g).asIso.hom) f = f) : ∃! h : (invariantSubalgebraPresheaf ρ).relativeSpec ⟶ Z, CategoryStruct.comp (invariantSubalgebraPresheaf ρ).relativeSpecπ h = f

The universal property of the relative invariant quotient by a finite group. Every G-invariant morphism from Spec_X(A) to an arbitrary scheme factors uniquely through the quotient projection Spec_X(A) ⟶ Spec_X(A)/G.

@[simp]

theorem CategoryTheory.CommMon.invariantQuotientDesc_relativeSpecπ_comp {X : AlgebraicGeometry.Scheme} {A : CommMon X.Modules} {G : Type v} [Group G] {ρ : G →* Aut A} [Finite G] [SheafOfModules.IsQuasicoherent A.X] {Z : AlgebraicGeometry.Scheme} (h : (invariantSubalgebraPresheaf ρ).relativeSpec ⟶ Z) : invariantQuotientDesc (CategoryStruct.comp (invariantSubalgebraPresheaf ρ).relativeSpecπ h) ⋯ = h

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