Affine invariant quotients by finite groups

For a finite group acting on a commutative ring A, the invariant-spectrum projection is integral and surjective, and its topological fibres are precisely the orbits of prime ideals. If A is of finite type over its fixed subring, the projection is finite; in particular, this holds when A is of finite type over an invariant base semiring R. These results supplement the affine-target universal property in TauCeti.AlgebraicGeometry.Quotient.Affine.

Neither flatness nor finite presentation of the quotient projection is asserted.

Main results

• The projection is integral and surjective for finite groups.
• isFinite_projection: the projection is finite when A is of finite type over its fixed subring.
• isFinite_projection_of_finiteType: finiteness over an invariant base semiring suffices.
• isQuotientMap_projection: the projection is a topological quotient map.
• projection_eq_iff_exists_smul: its fibres are prime-ideal orbits.

References

• Formal sources: Mathlib's Algebra.IsInvariant.isIntegral and Algebra.IsInvariant.exists_smul_of_under_eq.
• M. Demazure and A. Grothendieck, Schémas en groupes (SGA 3), Exposé V, §1.

instance TauCeti.AffineInvariantQuotient.instIsIntegralHomProjection (A : Type u) (G : Type v) [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] : AlgebraicGeometry.IsIntegralHom (projection A G)

The invariant-spectrum projection is integral for a finite group action.

instance TauCeti.AffineInvariantQuotient.instSurjectiveProjection (A : Type u) (G : Type v) [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] : AlgebraicGeometry.Surjective (projection A G)

The quotient projection is surjective for a finite group action.

theorem TauCeti.AffineInvariantQuotient.isFinite_projection (A : Type u) (G : Type v) [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] [Algebra.FiniteType (↥(FixedPoints.subring A G)) A] : AlgebraicGeometry.IsFinite (projection A G)

The quotient projection is finite when A is of finite type over its fixed subring.

theorem TauCeti.AffineInvariantQuotient.isFinite_projection_of_finiteType (A : Type u) (G : Type v) [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] (R : Type w) [CommSemiring R] [Algebra R A] [SMulCommClass G R A] [Algebra.FiniteType R A] : AlgebraicGeometry.IsFinite (projection A G)

The quotient projection is finite when A is of finite type over an invariant base R.

theorem TauCeti.AffineInvariantQuotient.isQuotientMap_projection (A : Type u) (G : Type v) [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] : Topology.IsQuotientMap ⇑(projection A G)

The projection is a quotient map of topological spaces.

theorem TauCeti.AffineInvariantQuotient.projection_eq_iff_exists_smul (A : Type u) (G : Type v) [CommRing A] [Group G] [MulSemiringAction G A] [Finite G] (x y : PrimeSpectrum A) : (projection A G) x = (projection A G) y ↔ ∃ (g : G), y = g • x

Two points have the same image exactly when they are in the same spectrum orbit.