The relative-perfect locus in affine derived families

This file cuts out the honest relative-perfect, universally-gluable locus in the affine family pseudofunctor. For a fixed affine morphism X : B ⟶ R and a test B-algebra A, the predicate is evaluated on the derived category of the actual base-changed total space Spec (R ⊔_B A) relative to Spec A.

Only the object locus is constructed here. In particular, this file does not install a Pseudofunctor.ObjectProperty.IsClosedUnderMapObj instance: that instance is precisely the pending theorem that arbitrary derived base change preserves pseudo-coherence, finite Tor amplitude, and fiberwise negative Ext vanishing. Once those results are proved, Mathlib's Pseudofunctor.ObjectProperty.fullsubcategory packages the restricted pseudofunctor and all of its coherence automatically.

def AlgebraicGeometry.affineFamilyUniversallyGluableRelativePerfect {B : CommRingCat} (X A : CategoryTheory.Under B) : CategoryTheory.ObjectProperty (DerivedCategory.Dqc.AffineBoundedAboveProjectiveQuasicoherentDerivedCategory (DerivedCategory.Dqc.AffineFamilyCoordinateRing X A))

The affine bounded-projective objects whose realization on the actual base-changed total space is relative-perfect and universally gluable over the test scheme.

Equations

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

instance AlgebraicGeometry.affineFamilyUniversallyGluableRelativePerfect_isClosedUnderIsomorphisms {B : CommRingCat} (X A : CategoryTheory.Under B) : (affineFamilyUniversallyGluableRelativePerfect X A).IsClosedUnderIsomorphisms

@[reducible, inline]

abbrev AlgebraicGeometry.AffineFamilyUniversallyGluableRelativePerfectCategory {B : CommRingCat} (X A : CategoryTheory.Under B) : Type (u + 1)

The full derived category of bounded-projective affine family objects that are genuinely relative-perfect and universally gluable.

Equations

• AlgebraicGeometry.AffineFamilyUniversallyGluableRelativePerfectCategory X A = (AlgebraicGeometry.affineFamilyUniversallyGluableRelativePerfect X A).FullSubcategory

noncomputable def AlgebraicGeometry.affineFamilyUniversallyGluableRelativePerfectCoreProperty {B : CommRingCat} (X : CategoryTheory.Under B) : (DerivedCategory.Dqc.affineFamilyBoundedAboveProjectivePseudofunctor X).ObjectProperty

The relative-perfect condition as an object property on every fiber of the affine family moduli-groupoid pseudofunctor.

Equations

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

instance AlgebraicGeometry.affineFamilyUniversallyGluableRelativePerfectCoreProperty_isClosed {B : CommRingCat} (X : CategoryTheory.Under B) : (affineFamilyUniversallyGluableRelativePerfectCoreProperty X).IsClosedUnderIsomorphisms

@[reducible, inline]

abbrev AlgebraicGeometry.AffineFamilyUniversallyGluableRelativePerfectModuliFiber {B : CommRingCat} (X A : CategoryTheory.Under B) : Type (u + 1)

The actual groupoid fiber of relative-perfect, universally-gluable affine families over the test B-algebra A.

Equations

• AlgebraicGeometry.AffineFamilyUniversallyGluableRelativePerfectModuliFiber X A = CategoryTheory.Core (AlgebraicGeometry.AffineFamilyUniversallyGluableRelativePerfectCategory X A)

instance AlgebraicGeometry.affineFamilyUniversallyGluableRelativePerfectModuliFiber_isGroupoid {B : CommRingCat} (X A : CategoryTheory.Under B) : CategoryTheory.IsGroupoid (AffineFamilyUniversallyGluableRelativePerfectModuliFiber X A)

noncomputable def AlgebraicGeometry.affineFamilyUniversallyGluableRelativePerfectCoreInclusion {B : CommRingCat} (X A : CategoryTheory.Under B) : CategoryTheory.Functor (AffineFamilyUniversallyGluableRelativePerfectModuliFiber X A) (DerivedCategory.Dqc.AffineFamilyBoundedAboveProjectiveModuliFiber X A)

Include the relative-perfect affine-family moduli groupoid in the ambient bounded-projective moduli groupoid.

Equations

• AlgebraicGeometry.affineFamilyUniversallyGluableRelativePerfectCoreInclusion X A = (AlgebraicGeometry.affineFamilyUniversallyGluableRelativePerfect X A).ι.core

noncomputable def AlgebraicGeometry.affineFamilyUniversallyGluableRelativePerfectModuliForget {B : CommRingCat} (X A : CategoryTheory.Under B) : CategoryTheory.Functor (AffineFamilyUniversallyGluableRelativePerfectModuliFiber X A) (DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory (Spec (DerivedCategory.Dqc.AffineFamilyCoordinateRing X A)))

Forget a relative-perfect affine family to the honest Dqc category of its base-changed total space.

Equations

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