The relative-perfect moduli presheaf

This file packages universally-gluable relative-perfect complexes and their isomorphisms as a groupoid-valued pseudofunctor on an actual diagram of scheme base changes. A RelativePerfectModuliProblem does not choose unrelated fiber categories: its fiber over T is definitionally the core of SchemeUniversallyGluableCategory T.hom, and every transition functor comes with a natural comparison to an actual left-derived pullback.

The explicit system boundary is necessary at the current stage. Exact and arbitrary left-derived pullback interfaces have been constructed, but preservation of pseudo-coherence, finite Tor amplitude, and fiberwise negative Ext is not yet available for arbitrary scheme morphisms. Thus this file neither installs such a theorem nor asserts descent or algebraicity. It constructs the moduli pseudofunctor from proved restriction data and gives a concrete identity system and zero objects, including on geometric-point fibers.

@[reducible, inline]

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

The category underlying the relative-perfect moduli groupoid over one scheme base change. Its arrows are only isomorphisms.

Equations

• AlgebraicGeometry.RelativePerfectModuliFiber T = CategoryTheory.Core (AlgebraicGeometry.SchemeUniversallyGluableCategory (CategoryTheory.Over.hom T))

noncomputable def AlgebraicGeometry.relativePerfectModuliForget {S : Scheme} (T : DerivedCategory.Families.SchemeBaseChange S) : CategoryTheory.Functor (RelativePerfectModuliFiber T) T.DerivedFiber

Forget a relative-perfect moduli groupoid to the ambient derived category.

Equations

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

noncomputable def AlgebraicGeometry.RelativePerfectPullback.coreFunctor {S : Scheme} {T U : DerivedCategory.Families.SchemeBaseChange S} {f : T ⟶ U} (P : RelativePerfectPullback f) : CategoryTheory.Functor (RelativePerfectModuliFiber U) (RelativePerfectModuliFiber T)

The pullback induced on the cores of the relative-perfect loci.

Equations

• P.coreFunctor = P.functor.core

noncomputable def AlgebraicGeometry.RelativePerfectPullback.coreComparison {S : Scheme} {T U : DerivedCategory.Families.SchemeBaseChange S} {f : T ⟶ U} (P : RelativePerfectPullback f) : P.coreFunctor.comp (relativePerfectModuliForget T) ≅ (relativePerfectModuliForget U).comp P.ambient.functor

On moduli groupoids, the core of a lifted relative-perfect pullback still agrees with ambient left-derived pullback after forgetting.

Equations

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

structure AlgebraicGeometry.RelativePerfectModuliProblem (S : Scheme) (B : Type v) [CategoryTheory.Category.{w, v} B] : Type (max (max (u + 2) v) w)

A groupoid-valued relative-perfect moduli problem on a contravariant diagram of actual scheme base changes.

The pseudofunctor itself owns the unit, compositor, triangle, and pentagon laws. fiberEquivalence identifies each of its fibers with the actual core of universally-gluable relative-perfect complexes. pullback supplies the actual lifted relative-perfect pullback functor, while transitionComparison identifies its core with the pseudofunctor transition.

• base : CategoryTheory.Functor Bᵒᵖ (DerivedCategory.Families.SchemeBaseChange S)

  The contravariant diagram of actual scheme base changes.

• presheaf : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete B) CategoryTheory.Cat

  The coherent groupoid-valued presheaf.

• fiberEquivalence (X : B) : ↑(self.presheaf.obj { as := X }) ≌ RelativePerfectModuliFiber (self.base.obj (Opposite.op X))

  Identification of every abstract pseudofunctor fiber with the actual relative-perfect moduli groupoid.

• pullback {X Y : B} (f : X ⟶ Y) : RelativePerfectPullback (self.base.map f.op)

  The actual lifted relative-perfect pullback attached to every arrow.

• transitionComparison {X Y : B} (f : X ⟶ Y) : (self.fiberEquivalence X).functor.comp (self.pullback f).coreFunctor ≅ (self.presheaf.map { as := f }).toFunctor.comp (self.fiberEquivalence Y).functor

  The lifted pullback on concrete moduli groupoids agrees with the transition of the abstract pseudofunctor.

instance AlgebraicGeometry.RelativePerfectModuliProblem.presheaf_obj_isGroupoid {S : Scheme} {B : Type v} [CategoryTheory.Category.{w, v} B] (M : RelativePerfectModuliProblem S B) (X : CategoryTheory.LocallyDiscrete B) : CategoryTheory.IsGroupoid ↑(M.presheaf.obj X)

Every fiber of a relative-perfect moduli problem is a groupoid.

noncomputable def AlgebraicGeometry.RelativePerfectModuliProblem.ambientComparison {S : Scheme} {B : Type v} [CategoryTheory.Category.{w, v} B] (M : RelativePerfectModuliProblem S B) {X Y : B} (f : X ⟶ Y) : (M.fiberEquivalence X).functor.comp ((relativePerfectModuliForget (M.base.obj (Opposite.op X))).comp (M.pullback f).ambient.functor) ≅ (M.presheaf.map { as := f }).toFunctor.comp ((M.fiberEquivalence Y).functor.comp (relativePerfectModuliForget (M.base.obj (Opposite.op Y))))

The pseudofunctor transition is the actual left-derived pullback after transport to the concrete moduli groupoids and forgetting to the ambient derived categories.

Equations

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

noncomputable def AlgebraicGeometry.RelativePerfectModuliProblem.exactAmbientComparison {S : Scheme} {B : Type v} [CategoryTheory.Category.{w, v} B] (M : RelativePerfectModuliProblem S B) {X Y : B} (f : X ⟶ Y) [DerivedCategory.Families.SchemeBaseChange.IsExactPullback (M.base.map f.op)] : (M.fiberEquivalence X).functor.comp ((relativePerfectModuliForget (M.base.obj (Opposite.op X))).comp (DerivedCategory.Families.SchemeBaseChange.derivedPullback (M.base.map f.op))) ≅ (M.presheaf.map { as := f }).toFunctor.comp ((M.fiberEquivalence Y).functor.comp (relativePerfectModuliForget (M.base.obj (Opposite.op Y))))

On an exact arrow, the transition comparison specializes canonically to the repository's exact derived pullback.

Equations

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

@[reducible, inline]

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

Isomorphism classes of universally-gluable relative-perfect objects over one scheme base change.

Equations

• AlgebraicGeometry.RelativePerfectIsomorphismClasses T = Quotient (CategoryTheory.isIsomorphicSetoid (AlgebraicGeometry.SchemeUniversallyGluableCategory (CategoryTheory.Over.hom T)))

noncomputable def AlgebraicGeometry.relativePerfectIsomorphismClass {S : Scheme} {T : DerivedCategory.Families.SchemeBaseChange S} (E : SchemeUniversallyGluableCategory (CategoryTheory.Over.hom T)) : RelativePerfectIsomorphismClasses T

The isomorphism class represented by one moduli object.

Equations

• AlgebraicGeometry.relativePerfectIsomorphismClass E = ⟦E⟧

@[reducible, inline]

abbrev AlgebraicGeometry.RelativePerfectGeometricFiber {S : Scheme} (T : DerivedCategory.Families.SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) : Type (u + 1)

The relative-perfect moduli groupoid on the geometric-point base change Spec κ(x) ⟶ S.

Equations

• AlgebraicGeometry.RelativePerfectGeometricFiber T x = AlgebraicGeometry.RelativePerfectModuliFiber (T.residue x)

noncomputable def AlgebraicGeometry.relativePerfectZeroObject {S : Scheme} (T : DerivedCategory.Families.SchemeBaseChange S) : RelativePerfectModuliFiber T

The zero complex as an object of the relative-perfect moduli groupoid.

Equations

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

theorem AlgebraicGeometry.relativePerfectModuliFiber_nonempty {S : Scheme} (T : DerivedCategory.Families.SchemeBaseChange S) : Nonempty (RelativePerfectModuliFiber T)

Every scheme base change has a nonempty relative-perfect moduli groupoid.

noncomputable def AlgebraicGeometry.relativePerfectGeometricZeroObject {S : Scheme} (T : DerivedCategory.Families.SchemeBaseChange S) (x : ↥(CategoryTheory.Over.left T)) : RelativePerfectGeometricFiber T x

Every geometric-point fiber has the concrete zero object.

Equations

• AlgebraicGeometry.relativePerfectGeometricZeroObject T x = AlgebraicGeometry.relativePerfectZeroObject (T.residue x)

The concrete identity moduli problem

This is the smallest geometric model of the interface: one actual scheme base change, identity derived pullback, and the full moduli groupoid at that base. It proves that the pseudofunctor package is inhabited without asserting preservation along any nonidentity morphism.

def AlgebraicGeometry.identityBaseChangeDiagram {S : Scheme} (T : DerivedCategory.Families.SchemeBaseChange S) : CategoryTheory.Functor PUnit.{u_1 + 1}ᵒᵖ (DerivedCategory.Families.SchemeBaseChange S)

The constant diagram at one scheme base change.

Equations

• AlgebraicGeometry.identityBaseChangeDiagram T = (CategoryTheory.Functor.const PUnit.{?u.1 + 1}ᵒᵖ).obj T

noncomputable def AlgebraicGeometry.constantRelativePerfectPresheaf {S : Scheme} (T : DerivedCategory.Families.SchemeBaseChange S) : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete PUnit.{u_1 + 1}) CategoryTheory.Cat

The constant groupoid-valued pseudofunctor at one relative-perfect moduli fiber.

Equations

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

noncomputable def AlgebraicGeometry.identityRelativePerfectModuliProblem {S : Scheme} (T : DerivedCategory.Families.SchemeBaseChange S) : RelativePerfectModuliProblem S PUnit.{u_1 + 1}

The coherent identity moduli problem at one scheme base change.

Equations

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