Big-Zariski presentations of selected relative-perfect moduli problems

This file connects the SF8 relative-perfect and boundedness layers to the SF9 stack-presentation layer without postulating an Artin representability theorem. A presentation contains big-Zariski stack data over the base and equivalences from its geometric fibers to the selected full subgroupoids of universally-gluable relative-perfect complexes. It is not an algebraic-stack structure: fppf or étale descent has not yet been proved.

The bounded refinement turns the universal family of an SF8 finite-type boundedness witness into an actual object of the corresponding stack fiber. Open relative-perfect presentations retain an actual representable open immersion and a commuting structural triangle.

The supported zero subproblem is constructed explicitly: the identity stack over a locally Noetherian base has contractible fibers, as does the full groupoid of zero relative-perfect objects. This is a genuine bounded big-Zariski presentation, but it is not claimed to be an algebraic stack or the full relative-perfect moduli stack.

@[reducible, inline]

abbrev AlgebraicGeometry.RelativePerfectModuliSelector.Fiber {S : Scheme} (P : RelativePerfectModuliSelector S) (T : DerivedCategory.Families.SchemeBaseChange S) : Type (u + 1)

The full subgroupoid selected inside one relative-perfect moduli fiber. This construction is fiberwise only: it does not provide transition functors and is not itself a subprestack.

Equations

• P.Fiber T = (P.familyLocus T).FullSubcategory

instance AlgebraicGeometry.RelativePerfectModuliSelector.fiber_isGroupoid {S : Scheme} (P : RelativePerfectModuliSelector S) (T : DerivedCategory.Families.SchemeBaseChange S) : CategoryTheory.IsGroupoid (P.Fiber T)

def AlgebraicGeometry.FiniteTypeBoundednessWitness.universalObject {S : Scheme} {P : RelativePerfectModuliSelector S} (W : FiniteTypeBoundednessWitness P) : P.Fiber W.parameter

Regard the universal family in a boundedness witness as an object of the selected full moduli subgroupoid.

Equations

• W.universalObject = { obj := W.universalFamily, property := ⋯ }

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

A big-Zariski presentation of a selected relative-perfect moduli problem.

For every locally Noetherian base change T ⟶ S, the fiber of the actual structure morphism over that map is equivalent to the selected full subgroupoid of universally-gluable relative-perfect complexes on T. Restricting this field to the currently supported locally Noetherian locus keeps the unresolved arbitrary-scheme Dqc comparison visible.

• presentation : ZariskiStackPresentationOver S

  The big-Zariski presentation locally of finite presentation over S.

• fiberEquivalence (T : DerivedCategory.Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left T)] : self.presentation.structureMorphism.FiberCategory (representableZariskiObject (CategoryTheory.Over.hom T)) (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (CategoryTheory.Over.left T))) ≌ P.Fiber T

  Identification of each supported stack fiber with the selected relative-perfect moduli groupoid.

@[reducible, inline]

abbrev AlgebraicGeometry.RelativePerfectZariskiPresentation.stack {S : Scheme} {P : RelativePerfectModuliSelector S} (A : RelativePerfectZariskiPresentation S P) : ZariskiStackPresentation

The big-Zariski stack presentation underlying a relative-perfect presentation.

Equations

• A.stack = A.presentation.toZariskiStackPresentation

theorem AlgebraicGeometry.RelativePerfectZariskiPresentation.locallyOfFinitePresentation {S : Scheme} {P : RelativePerfectModuliSelector S} (A : RelativePerfectZariskiPresentation S P) : StackMorphism.IsLocallyOfFinitePresentation A.presentation.structureMorphism

The actual locally-finitely-presented structure morphism underlying a relative-perfect big-Zariski presentation.

structure AlgebraicGeometry.BoundedRelativePerfectZariskiPresentation (S : Scheme) (P : RelativePerfectModuliSelector S) extends AlgebraicGeometry.RelativePerfectZariskiPresentation S P : Type (u + 1)

A bounded big-Zariski presentation co-locates an actual finite-type SF8 boundedness witness with the SF9 stack presentation of the same selected relative-perfect moduli problem.

• presentation : ZariskiStackPresentationOver S
• fiberEquivalence (T : DerivedCategory.Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left T)] : self.presentation.structureMorphism.FiberCategory (representableZariskiObject (CategoryTheory.Over.hom T)) (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (CategoryTheory.Over.left T))) ≌ P.Fiber T
• boundedness : FiniteTypeBoundednessWitness P

  The actual finite-type parameter scheme and its universal family.

def AlgebraicGeometry.BoundedRelativePerfectZariskiPresentation.universalStackObject {S : Scheme} {P : RelativePerfectModuliSelector S} (A : BoundedRelativePerfectZariskiPresentation S P) [IsLocallyNoetherian (CategoryTheory.Over.left A.boundedness.parameter)] : A.presentation.structureMorphism.FiberCategory (representableZariskiObject (CategoryTheory.Over.hom A.boundedness.parameter)) (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id (CategoryTheory.Over.left A.boundedness.parameter)))

The SF8 universal family, lifted through the proved fiber equivalence to an actual object of the SF9 big-Zariski stack over the parameter scheme.

Equations

• A.universalStackObject = (A.fiberEquivalence A.boundedness.parameter).inverse.obj A.boundedness.universalObject

noncomputable def AlgebraicGeometry.BoundedRelativePerfectZariskiPresentation.universalFamilyIso {S : Scheme} {P : RelativePerfectModuliSelector S} (A : BoundedRelativePerfectZariskiPresentation S P) [IsLocallyNoetherian (CategoryTheory.Over.left A.boundedness.parameter)] : (A.fiberEquivalence A.boundedness.parameter).functor.obj A.universalStackObject ≅ A.boundedness.universalObject

The lifted stack object realizes precisely the boundedness witness's universal relative-perfect family.

Equations

• A.universalFamilyIso = (A.fiberEquivalence A.boundedness.parameter).counitIso.app A.boundedness.universalObject

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

An open relative-perfect presentation keeps both moduli interpretations, an actual representable open immersion of their big-Zariski stacks, and the commuting triangle over the base. familyLocus_le states that the open fiberwise locus selects only objects of the ambient problem.

• ambient : RelativePerfectZariskiPresentation S ambientProblem

  Big-Zariski presentation of the ambient selected problem.

• openPresentation : RelativePerfectZariskiPresentation S openProblem

  Big-Zariski presentation of the open selected problem.

• familyLocus_le {T : DerivedCategory.Families.SchemeBaseChange S} {E : RelativePerfectModuliFiber T} : openProblem.familyLocus T E → ambientProblem.familyLocus T E

  The open family locus is contained in the ambient fiberwise locus.

• inclusion : CategoryTheory.StackMorphism self.openPresentation.stack.toStackInGroupoids self.ambient.stack.toStackInGroupoids

  The actual morphism from the open stack to the ambient stack.

• isOpenImmersion : StackMorphism.IsOpenImmersion self.inclusion

  Every scheme representing a fiber of the inclusion is an open subscheme of the test scheme.

• overBase (T : Scheme) : (self.inclusion.app T).comp (self.ambient.presentation.structureMorphism.app T) ≅ self.openPresentation.presentation.structureMorphism.app T

  The inclusion commutes with the actual structure morphisms to S.

The supported zero presentation

noncomputable def AlgebraicGeometry.zeroRelativePerfectZariskiPresentation (S : Scheme) : RelativePerfectZariskiPresentation S (zeroRelativePerfectModuliSelector S)

The zero relative-perfect subproblem has an actual big-Zariski presentation: the identity stack over S. Its fibers and the groupoids of selected zero objects are both proved contractible.

Equations

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

noncomputable def AlgebraicGeometry.zeroBoundedRelativePerfectZariskiPresentation (S : Scheme) : BoundedRelativePerfectZariskiPresentation S (zeroRelativePerfectModuliSelector S)

The identity parameter scheme and universal zero family make the supported zero big-Zariski presentation genuinely finite-type bounded.

Equations

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

noncomputable def AlgebraicGeometry.integerZeroBoundedRelativePerfectZariskiPresentation : BoundedRelativePerfectZariskiPresentation (Spec (CommRingCat.of ℤ)) (zeroRelativePerfectModuliSelector (Spec (CommRingCat.of ℤ)))

A concrete positive-dimensional supported case: Spec ℤ carries the bounded big-Zariski presentation of its zero relative-perfect subproblem.

Equations

• AlgebraicGeometry.integerZeroBoundedRelativePerfectZariskiPresentation = AlgebraicGeometry.zeroBoundedRelativePerfectZariskiPresentation (AlgebraicGeometry.Spec (CommRingCat.of ℤ))