Representable quotient problems and the zero parameter space

A quotient problem is represented only when its functor of points is isomorphic to a Yoneda functor. This is the universal property that prevents an arbitrary scheme from being called a Quot scheme.

At the current Mathlib pin no general Quot-scheme or Grassmannian representability theorem is available. The supported construction here is the zero quotient: its functor has exactly one quotient over every test scheme and is represented by the terminal object S ⟶ S of Over S. The parameter is finite type and its zero complex realizes the boundedness witness from SF8.3.

structure AlgebraicGeometry.RepresentableQuotientProblem (S : Scheme) : Type (u + 1)

A quotient problem on schemes over S, together with a representing scheme and the full Yoneda universal property.

• problem : CategoryTheory.Functor (DerivedCategory.Families.SchemeBaseChange S)ᵒᵖ (Type u)

  The functor of quotient families.

• parameter : DerivedCategory.Families.SchemeBaseChange S

  The representing parameter scheme over S.

• representation : CategoryTheory.yoneda.obj self.parameter ≅ self.problem

  The universal property of the parameter scheme.

def AlgebraicGeometry.RepresentableQuotientProblem.universal {S : Scheme} (Q : RepresentableQuotientProblem S) : Q.problem.obj (Opposite.op Q.parameter)

The universal quotient-family element, obtained from the identity of the representing scheme by Yoneda.

Equations

• Q.universal = (CategoryTheory.ConcreteCategory.hom (Q.representation.hom.app (Opposite.op Q.parameter))) (CategoryTheory.CategoryStruct.id Q.parameter)

structure AlgebraicGeometry.FiniteTypeQuotientParameterSpace (S : Scheme) extends AlgebraicGeometry.RepresentableQuotientProblem S : Type (u + 1)

A representable quotient problem whose actual parameter morphism is of finite type.

• problem : CategoryTheory.Functor (DerivedCategory.Families.SchemeBaseChange S)ᵒᵖ (Type u)
• parameter : DerivedCategory.Families.SchemeBaseChange S
• representation : CategoryTheory.yoneda.obj self.parameter ≅ self.problem
• finiteType : DerivedCategory.Families.IsFiniteTypeBaseChange self.parameter

  The structure morphism is locally of finite type and quasi-compact.

def AlgebraicGeometry.zeroQuotientProblem (S : Scheme) : CategoryTheory.Functor (DerivedCategory.Families.SchemeBaseChange S)ᵒᵖ (Type u)

The functor with one supported zero quotient over every test scheme.

Equations

• AlgebraicGeometry.zeroQuotientProblem S = (CategoryTheory.Functor.const (AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange S)ᵒᵖ).obj PUnit.{?u.1 + 1}

def AlgebraicGeometry.zeroQuotientRepresentation (S : Scheme) : CategoryTheory.yoneda.obj (identityRelativePerfectBaseChange S) ≅ zeroQuotientProblem S

The zero quotient functor is represented by the terminal identity scheme over S.

Equations

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

def AlgebraicGeometry.zeroFiniteTypeQuotientParameterSpace (S : Scheme) : FiniteTypeQuotientParameterSpace S

The finite-type parameter space representing the zero quotient problem.

Equations

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

noncomputable def AlgebraicGeometry.zeroQuotientRealization {S : Scheme} (T : DerivedCategory.Families.SchemeBaseChange S) : (zeroQuotientProblem S).obj (Opposite.op T) → ModuleQuotient 0

Realize the unique supported zero quotient over an actual test scheme.

Equations

• AlgebraicGeometry.zeroQuotientRealization T x✝ = AlgebraicGeometry.ModuleQuotient.zero (CategoryTheory.Over.left T)

theorem AlgebraicGeometry.zeroQuotient_universal_eq (S : Scheme) : (zeroFiniteTypeQuotientParameterSpace S).universal = PUnit.unit

The universal element classified by the representing identity scheme is the unique zero-quotient point.

noncomputable def AlgebraicGeometry.zeroQuotientToRelativePerfect {S : Scheme} (T : DerivedCategory.Families.SchemeBaseChange S) : (zeroQuotientProblem S).obj (Opposite.op T) → RelativePerfectModuliFiber T

The supported zero quotient maps to the actual relative-perfect moduli fiber by the zero complex.

Equations

• AlgebraicGeometry.zeroQuotientToRelativePerfect T x✝ = AlgebraicGeometry.relativePerfectZeroObject T

noncomputable def AlgebraicGeometry.zeroQuotientRelativePerfectModuliProblem (S : Scheme) : RelativePerfectModuliProblem S PUnit.{u_1 + 1}

On the identity parameter scheme, the zero quotient produces the concrete relative-perfect moduli problem from SF8.2.

Equations

• AlgebraicGeometry.zeroQuotientRelativePerfectModuliProblem S = AlgebraicGeometry.identityRelativePerfectModuliProblem (AlgebraicGeometry.identityRelativePerfectBaseChange S)

noncomputable def AlgebraicGeometry.zeroQuotientFiniteTypeBoundednessWitness (S : Scheme) : FiniteTypeBoundednessWitness (zeroRelativePerfectModuliSelector S)

The finite-type zero Quot parameter realizes the honest boundedness witness from SF8.3, including geometric-point coverage.

Equations

• AlgebraicGeometry.zeroQuotientFiniteTypeBoundednessWitness S = AlgebraicGeometry.zeroFiniteTypeBoundednessWitness S

theorem AlgebraicGeometry.zeroQuotient_isGeometricallyBounded (S : Scheme) : (relativePerfectGeometricBoundednessProblem S).IsBounded (zeroRelativePerfectModuliSelector S)

Consequently the supported zero Quot construction inhabits the SF8.3 geometric boundedness predicate.