Affine invariant quotients

For a monoid acting on a commutative ring A, the affine invariant quotient is Spec (Aᴳ), with projection induced by the inclusion of the fixed subring. This file proves its universal property for affine target schemes. For group actions, the contravariant spectrum maps are isomorphisms and act on prime ideals by the inverse element.

The universal property for affine targets requires only a monoid action. This file does not construct the fppf sheaf quotient or prove the universal property for non-affine targets. The finite-group properties of the projection are developed in TauCeti.AlgebraicGeometry.Quotient.FiniteGroup.Affine.

Main definitions

• quotient: the spectrum of the fixed subring.
• projection: the invariant-spectrum projection.
• specComap: the contravariant spectrum map of an action element.
• desc: descent of an invariant morphism to an affine target.

Main results

• existsUnique_desc and hom_ext: the affine-target universal property.
• projection_specAlgebraMap: the projection lies over every invariant base ring.
• specComap_base_apply: the point map of a group element is the inverse spectrum action.

References

• M. Demazure and A. Grothendieck, Schémas en groupes (SGA 3), Exposé V, §1.

@[reducible, inline]

noncomputable abbrev TauCeti.AffineInvariantQuotient.quotient (A : Type u) (G : Type v) [CommRing A] [Monoid G] [MulSemiringAction G A] : AlgebraicGeometry.Scheme

The spectrum of the fixed subring, the affine invariant quotient of Spec A.

Equations

• TauCeti.AffineInvariantQuotient.quotient A G = AlgebraicGeometry.Spec ↧↥(FixedPoints.subring A G)

noncomputable def TauCeti.AffineInvariantQuotient.projection (A : Type u) (G : Type v) [CommRing A] [Monoid G] [MulSemiringAction G A] : AlgebraicGeometry.Spec ↧A ⟶ quotient A G

The quotient projection, induced by the inclusion of invariant functions.

Equations

• TauCeti.AffineInvariantQuotient.projection A G = AlgebraicGeometry.Spec.algebraMap (↥(FixedPoints.subring A G)) A

theorem TauCeti.AffineInvariantQuotient.projection_def (A : Type u) (G : Type v) [CommRing A] [Monoid G] [MulSemiringAction G A] : projection A G = AlgebraicGeometry.Spec.algebraMap (↥(FixedPoints.subring A G)) A

The defining equation for the quotient projection.

@[simp]

theorem TauCeti.AffineInvariantQuotient.projection_base_apply (A : Type u) (G : Type v) [CommRing A] [Monoid G] [MulSemiringAction G A] (x : PrimeSpectrum A) : (projection A G) x = PrimeSpectrum.comap (algebraMap (↥(FixedPoints.subring A G)) A) x

The projection contracts prime ideals to the fixed subring.

@[simp]

theorem TauCeti.AffineInvariantQuotient.projection_specAlgebraMap (A : Type u) (G : Type v) [CommRing A] [Monoid G] [MulSemiringAction G A] (R : Type u) [CommRing R] [Algebra R A] [SMulCommClass G R A] : CategoryTheory.CategoryStruct.comp (projection A G) (AlgebraicGeometry.Spec.algebraMap R ↥(FixedPoints.subalgebra R A G)) = AlgebraicGeometry.Spec.algebraMap R A

The quotient projection lies over every invariant base ring.

theorem TauCeti.AffineInvariantQuotient.projection_specAlgebraMap_assoc (A : Type u) (G : Type v) [CommRing A] [Monoid G] [MulSemiringAction G A] (R : Type u) [CommRing R] [Algebra R A] [SMulCommClass G R A] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (projection A G) (AlgebraicGeometry.Spec.algebraMap R ↥(FixedPoints.subalgebra R A G))) h = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.algebraMap R A) h

The quotient projection lies over every invariant base ring.

noncomputable def TauCeti.AffineInvariantQuotient.specComap (A : Type u) (G : Type v) [CommRing A] [Monoid G] [MulSemiringAction G A] (g : G) : AlgebraicGeometry.Spec ↧A ⟶ AlgebraicGeometry.Spec ↧A

The contravariant spectrum map induced by an element of the acting monoid.

Equations

• TauCeti.AffineInvariantQuotient.specComap A G g = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (MulSemiringAction.toRingHom G A g))

theorem TauCeti.AffineInvariantQuotient.specComap_def (A : Type u) (G : Type v) [CommRing A] [Monoid G] [MulSemiringAction G A] (g : G) : specComap A G g = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (MulSemiringAction.toRingHom G A g))

The defining equation for the contravariant spectrum map.

@[simp]

theorem TauCeti.AffineInvariantQuotient.preimage_specComap (A : Type u) (G : Type v) [CommRing A] [Monoid G] [MulSemiringAction G A] (g : G) : AlgebraicGeometry.Spec.preimage (specComap A G g) = CommRingCat.ofHom (MulSemiringAction.toRingHom G A g)

Pullback on global sections recovers the ring homomorphism of the action element.

@[simp]

theorem TauCeti.AffineInvariantQuotient.specComap_one (A : Type u) (G : Type v) [CommRing A] [Monoid G] [MulSemiringAction G A] : specComap A G 1 = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧A)

@[simp]

theorem TauCeti.AffineInvariantQuotient.specComap_mul (A : Type u) (G : Type v) [CommRing A] [Monoid G] [MulSemiringAction G A] (g h : G) : specComap A G (g * h) = CategoryTheory.CategoryStruct.comp (specComap A G g) (specComap A G h)

Pullback reverses composition: these morphisms form a right action on the spectrum.

@[simp]

theorem TauCeti.AffineInvariantQuotient.specComap_projection (A : Type u) (G : Type v) [CommRing A] [Monoid G] [MulSemiringAction G A] (g : G) : CategoryTheory.CategoryStruct.comp (specComap A G g) (projection A G) = projection A G

The quotient projection is invariant under every element of the acting monoid.

@[simp]

theorem TauCeti.AffineInvariantQuotient.specComap_projection_assoc (A : Type u) (G : Type v) [CommRing A] [Monoid G] [MulSemiringAction G A] (g : G) {Z : AlgebraicGeometry.Scheme} (h : quotient A G ⟶ Z) : CategoryTheory.CategoryStruct.comp (specComap A G g) (CategoryTheory.CategoryStruct.comp (projection A G) h) = CategoryTheory.CategoryStruct.comp (projection A G) h

The quotient projection is invariant under every element of the acting monoid.

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

Descend an invariant morphism to an affine target through the fixed-subring spectrum.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AffineInvariantQuotient.projection_desc {A : Type u} {G : Type v} [CommRing A] [Monoid G] [MulSemiringAction G A] {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : AlgebraicGeometry.Spec ↧A ⟶ Y) (hf : ∀ (g : G), CategoryTheory.CategoryStruct.comp (specComap A G g) f = f) : CategoryTheory.CategoryStruct.comp (projection A G) (desc f hf) = f

The descended morphism factors the given invariant morphism.

@[simp]

theorem TauCeti.AffineInvariantQuotient.projection_desc_assoc {A : Type u} {G : Type v} [CommRing A] [Monoid G] [MulSemiringAction G A] {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : AlgebraicGeometry.Spec ↧A ⟶ Y) (hf : ∀ (g : G), CategoryTheory.CategoryStruct.comp (specComap A G g) f = f) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (projection A G) (CategoryTheory.CategoryStruct.comp (desc f hf) h) = CategoryTheory.CategoryStruct.comp f h

The descended morphism factors the given invariant morphism.

theorem TauCeti.AffineInvariantQuotient.hom_ext {A : Type u} {G : Type v} [CommRing A] [Monoid G] [MulSemiringAction G A] {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] {f h : quotient A G ⟶ Y} (hfh : CategoryTheory.CategoryStruct.comp (projection A G) f = CategoryTheory.CategoryStruct.comp (projection A G) h) : f = h

Morphisms from the invariant quotient to an affine target are determined by their composition with the projection.

theorem TauCeti.AffineInvariantQuotient.hom_ext_iff {A : Type u} {G : Type v} [CommRing A] [Monoid G] [MulSemiringAction G A] {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] {f h : quotient A G ⟶ Y} : f = h ↔ CategoryTheory.CategoryStruct.comp (projection A G) f = CategoryTheory.CategoryStruct.comp (projection A G) h

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

The affine-target universal property: every invariant morphism factors uniquely through the invariant quotient.

@[simp]

theorem TauCeti.AffineInvariantQuotient.desc_projection {A : Type u} {G : Type v} [CommRing A] [Monoid G] [MulSemiringAction G A] {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] (f : quotient A G ⟶ Y) : desc (CategoryTheory.CategoryStruct.comp (projection A G) f) ⋯ = f

Descending the pullback of an affine-target morphism recovers that morphism.

instance TauCeti.AffineInvariantQuotient.instIsIsoSchemeSpecComap (A : Type u) (G : Type v) [CommRing A] [Group G] [MulSemiringAction G A] (g : G) : CategoryTheory.IsIso (specComap A G g)

Every contravariant spectrum map of a group element is an isomorphism.

@[simp]

theorem TauCeti.AffineInvariantQuotient.specComap_base_apply (A : Type u) (G : Type v) [CommRing A] [Group G] [MulSemiringAction G A] (g : G) (x : PrimeSpectrum A) : (specComap A G g) x = g⁻¹ • x

The contravariant spectrum map of g is the standard spectrum action by g⁻¹.