A universally stable affine relative-perfect pseudofunctor

The full affine relative-perfect locus has been defined, but showing that every one of its objects remains relative-perfect and universally gluable after arbitrary base change is the main pending geometric theorem.

This file constructs the honest supported sub-pseudofunctor consisting of objects that satisfy the concrete relative-perfect predicate after every base change. Preservation is a theorem of the pseudofunctor compositor, not caller-supplied data. The resulting object property is contained in the full relative-perfect locus by the pseudofunctor unit. Proving the reverse containment is exactly the remaining preservation boundary.

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

The affine relative-perfect objects that satisfy the concrete predicate after every further morphism of test algebras.

Equations

• AlgebraicGeometry.affineFamilyUniversallyStableRelativePerfectCoreProperty X = (AlgebraicGeometry.affineFamilyUniversallyGluableRelativePerfectCoreProperty X).universallyStable

instance AlgebraicGeometry.affineFamilyUniversallyStableRelativePerfectCoreProperty_isClosedUnderMapObj {B : CommRingCat} (X : CategoryTheory.Under B) : (affineFamilyUniversallyStableRelativePerfectCoreProperty X).IsClosedUnderMapObj

noncomputable def AlgebraicGeometry.affineFamilyUniversallyStableRelativePerfectPseudofunctor {B : CommRingCat} (X : CategoryTheory.Under B) : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete (CategoryTheory.Under B)) CategoryTheory.Cat

Universally base-change-stable relative-perfect affine families form an actual groupoid-valued sub-pseudofunctor.

Equations

• AlgebraicGeometry.affineFamilyUniversallyStableRelativePerfectPseudofunctor X = (AlgebraicGeometry.affineFamilyUniversallyStableRelativePerfectCoreProperty X).fullsubcategory

noncomputable def AlgebraicGeometry.affineFamilyUniversallyStableRelativePerfectInclusion {B : CommRingCat} (X : CategoryTheory.Under B) : (affineFamilyUniversallyStableRelativePerfectPseudofunctor X).StrongTrans (DerivedCategory.Dqc.affineFamilyBoundedAboveProjectivePseudofunctor X)

The universally stable relative-perfect pseudofunctor includes in the ambient bounded-projective affine family pseudofunctor.

Equations

• AlgebraicGeometry.affineFamilyUniversallyStableRelativePerfectInclusion X = (AlgebraicGeometry.affineFamilyUniversallyStableRelativePerfectCoreProperty X).ι

theorem AlgebraicGeometry.affineFamilyUniversallyStableRelativePerfect_le_fullLocus {B : CommRingCat} (X : CategoryTheory.Under B) (A : CategoryTheory.LocallyDiscrete (CategoryTheory.Under B)) : (affineFamilyUniversallyStableRelativePerfectCoreProperty X).prop A ≤ (affineFamilyUniversallyGluableRelativePerfectCoreProperty X).prop A

Every universally base-change-stable object satisfies the concrete relative-perfect and universally-gluable predicate in its original fiber.

theorem AlgebraicGeometry.affineFamilyUniversallyStableRelativePerfect_eq_fullLocus {B : CommRingCat} (X : CategoryTheory.Under B) [(affineFamilyUniversallyGluableRelativePerfectCoreProperty X).IsClosedUnderMapObj] (A : CategoryTheory.LocallyDiscrete (CategoryTheory.Under B)) : (affineFamilyUniversallyStableRelativePerfectCoreProperty X).prop A = (affineFamilyUniversallyGluableRelativePerfectCoreProperty X).prop A

Once arbitrary affine pullback is proved to preserve the full concrete relative-perfect locus, the supported universally stable locus agrees with it fiberwise.