Finite-type boundedness witnesses for relative-perfect complexes

This file replaces a caller-selected boundedness proposition by geometric data. A witness consists of an actual scheme over the base whose structure morphism is locally of finite type and quasi-compact, a universally-gluable relative-perfect family on that scheme, and geometric fibers covering the chosen subproblem up to isomorphism.

The current derived-pullback API does not yet construct the geometric fiber of every relative-perfect family along every residue-field morphism. Thus a witness records those fibers explicitly and its coverage statement compares objects only after an equality of the actual residue-field base changes. The zero family below inhabits this interface without postulating a general base-change theorem. General semistable-object boundedness and Quot parameter spaces remain later results.

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

Two fiberwise, replete loci used to state a relative-perfect boundedness problem. familyLocus specifies which total families are admitted, while geometricLocus specifies the objects that a finite-type parameter family must cover.

This is deliberately a selector, not a subprestack: it supplies neither an ambient pseudofunctor nor preservation under restriction. A genuine subprestack must separately use Pseudofunctor.ObjectProperty and prove IsClosedUnderMapObj.

• familyLocus (T : DerivedCategory.Families.SchemeBaseChange S) : CategoryTheory.ObjectProperty (RelativePerfectModuliFiber T)

  Admissible total families on every actual base change.

• geometricLocus (T : DerivedCategory.Families.SchemeBaseChange S) : CategoryTheory.ObjectProperty (RelativePerfectModuliFiber T)

  The selected geometric objects.

• familyLocus_iso (T : DerivedCategory.Families.SchemeBaseChange S) : (self.familyLocus T).IsClosedUnderIsomorphisms

  Family membership is invariant under isomorphism.

• geometricLocus_iso (T : DerivedCategory.Families.SchemeBaseChange S) : (self.geometricLocus T).IsClosedUnderIsomorphisms

  Geometric membership is invariant under isomorphism.

instance AlgebraicGeometry.RelativePerfectModuliSelector.familyLocus_isClosedUnderIsomorphisms {S : Scheme} (P : RelativePerfectModuliSelector S) (T : DerivedCategory.Families.SchemeBaseChange S) : (P.familyLocus T).IsClosedUnderIsomorphisms

instance AlgebraicGeometry.RelativePerfectModuliSelector.geometricLocus_isClosedUnderIsomorphisms {S : Scheme} (P : RelativePerfectModuliSelector S) (T : DerivedCategory.Families.SchemeBaseChange S) : (P.geometricLocus T).IsClosedUnderIsomorphisms

structure AlgebraicGeometry.RelativePerfectModuliSelector.MonotoneTo {S : Scheme} (P Q : RelativePerfectModuliSelector S) : Prop

Data sufficient to transport a boundedness witness from P to Q. Admissible families may be enlarged, while the geometric target may be shrunk.

• familyLocus {T : DerivedCategory.Families.SchemeBaseChange S} {E : RelativePerfectModuliFiber T} : P.familyLocus T E → Q.familyLocus T E

  Every P-family is admitted by Q.

• geometricLocus {T : DerivedCategory.Families.SchemeBaseChange S} {E : RelativePerfectModuliFiber T} : Q.geometricLocus T E → P.geometricLocus T E

  Every geometric object requested by Q was already requested by P.

def AlgebraicGeometry.castRelativePerfectModuliObject {S : Scheme} {T U : DerivedCategory.Families.SchemeBaseChange S} (h : T = U) (E : RelativePerfectModuliFiber T) : RelativePerfectModuliFiber U

Transport a moduli object across an equality of actual scheme base changes.

Equations

• AlgebraicGeometry.castRelativePerfectModuliObject h E = h ▸ E

structure AlgebraicGeometry.FiniteTypeBoundednessWitness {S : Scheme} (P : RelativePerfectModuliSelector S) : Type (u + 1)

An actual finite-type parameter family covering a selected relative- perfect moduli boundedness problem.

• parameter : DerivedCategory.Families.SchemeBaseChange S

  The parameter scheme with its structure morphism to S.

• finiteType : DerivedCategory.Families.IsFiniteTypeBaseChange self.parameter

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

• universalFamily : RelativePerfectModuliFiber self.parameter

  The universal relative-perfect, universally-gluable family.

• universalFamily_mem : P.familyLocus self.parameter self.universalFamily

  The universal family belongs to the selected family locus.

• geometricFiber (x : ↥(CategoryTheory.Over.left self.parameter)) : RelativePerfectModuliFiber (self.parameter.residue x)

  A chosen geometric fiber over every point of the parameter scheme.

• covers {T : DerivedCategory.Families.SchemeBaseChange S} (E : RelativePerfectModuliFiber T) : P.geometricLocus T E → ∃ (x : ↥(CategoryTheory.Over.left self.parameter)) (h : T = self.parameter.residue x), Nonempty (castRelativePerfectModuliObject h E ≅ self.geometricFiber x)

  Every selected geometric object occurs as one of the chosen fibers, up to an isomorphism in the relative-perfect moduli groupoid.

def AlgebraicGeometry.FiniteTypeBoundednessWitness.monotone {S : Scheme} {P Q : RelativePerfectModuliSelector S} (W : FiniteTypeBoundednessWitness P) (h : P.MonotoneTo Q) : FiniteTypeBoundednessWitness Q

Boundedness is monotone under enlargement of the allowed family class and restriction of the geometric target.

Equations

• W.monotone h = { parameter := W.parameter, finiteType := ⋯, universalFamily := W.universalFamily, universalFamily_mem := ⋯, geometricFiber := W.geometricFiber, covers := ⋯ }

def AlgebraicGeometry.relativePerfectGeometricBoundednessProblem (S : Scheme) : CategoryTheory.Moduli.BoundednessProblem (RelativePerfectModuliSelector S)

The geometric boundedness problem attached to relative-perfect moduli selectors. Its predicate is existence of actual finite-type parameter data, rather than a caller-chosen proposition.

Equations

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

theorem AlgebraicGeometry.universalRelativePerfectBoundedness_of_witnesses (S : Scheme) (h : ∀ (P : RelativePerfectModuliSelector S), Nonempty (FiniteTypeBoundednessWitness P)) : CategoryTheory.Moduli.UniversalBoundedness (relativePerfectGeometricBoundednessProblem S)

Finite-type witnesses for every selected locus selector discharge the boundedness clause of Definition 21.15(5).

A nonempty finite-type model: the zero family

def AlgebraicGeometry.identityRelativePerfectBaseChange (S : Scheme) : DerivedCategory.Families.SchemeBaseChange S

The identity scheme base change, used as the parameter scheme for the zero family.

Equations

• AlgebraicGeometry.identityRelativePerfectBaseChange S = CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id S)

def AlgebraicGeometry.zeroRelativePerfectModuliSelector (S : Scheme) : RelativePerfectModuliSelector S

The supported zero selector. Total families must be zero after forgetting to the ambient derived category. Its geometric objects are zero objects over residue-field base changes of actual points of S.

Equations

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

theorem AlgebraicGeometry.relativePerfectZeroObject_mem_zeroFamilyLocus {S : Scheme} (T : DerivedCategory.Families.SchemeBaseChange S) : (zeroRelativePerfectModuliSelector S).familyLocus T (relativePerfectZeroObject T)

The universal zero family is a selected family.

noncomputable def AlgebraicGeometry.zeroRelativePerfectGeometricFiber (S : Scheme) (x : ↥S) : RelativePerfectModuliFiber ((identityRelativePerfectBaseChange S).residue x)

The chosen zero fiber over a point of the identity parameter scheme.

Equations

• AlgebraicGeometry.zeroRelativePerfectGeometricFiber S x = AlgebraicGeometry.relativePerfectZeroObject ((AlgebraicGeometry.identityRelativePerfectBaseChange S).residue x)

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

The identity parameter scheme and zero universal family form an actual finite-type boundedness witness.

Equations

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

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

The zero selector is geometrically bounded by an inhabited finite-type witness, not by a constant-true predicate.

theorem AlgebraicGeometry.zeroRelativePerfectBoundedness_afterBaseChange {S S' : Scheme} : ∀ (x : S' ⟶ S), (relativePerfectGeometricBoundednessProblem S').IsBounded (zeroRelativePerfectModuliSelector S')

The supported zero boundedness construction is available after every change of base. This deliberately does not claim a general pullback theorem for nonzero universal families.

def AlgebraicGeometry.zeroRelativePerfectBoundednessProblem (S : Scheme) : CategoryTheory.Moduli.BoundednessProblem PUnit.{u_1 + 1}

The Definition 21.15(5) adapter for the single supported zero subproblem.

Equations

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

theorem AlgebraicGeometry.universalBoundedness_zeroRelativePerfect (S : Scheme) : CategoryTheory.Moduli.UniversalBoundedness (zeroRelativePerfectBoundednessProblem S)

The supported zero model unconditionally satisfies its honest geometric boundedness problem.