Base-change components of scheme-derived categories #

This file starts the construction of the categories D_T and (Dqc)_T from Section 3 of arXiv:1902.08184v4 without imposing a Noetherian hypothesis on T or on the fibre product X_T.

If X and T are schemes over S, their product in Over S is the ordinary fibre product X_T. A source component is represented by an object property P in Dqc(X). Its perfect part is the intersection with the canonical compact-object property. Given the geometric external-product functor on those compact factors, the paper's construction is then expressed by the existing object-property closure operators:

take the triangulated envelope of the external products in Dqc(X_T);
take its coproduct-and-extension closure to obtain (Dqc)_T;
restrict (Dqc)_T to the intrinsic bounded-coherent cohomology locus to obtain D_T.

The use of compact objects is deliberate. Under the quasi-compact affine- diagonal hypotheses of Proposition 3.15 they are the perfect complexes, while the repository's current SchemePerfectDerivedCategory is built from D(Coh -) and therefore requires local Noetherianity. Using it for T would silently strengthen Theorem 3.17. The eventual compact-equals-perfect theorem will identify this construction with the paper's notation rather than change its carrier.

No new category hierarchy is introduced: every category below is an abbreviation for ObjectProperty.FullSubcategory. A DqcLeftDerivedPullback refines the repository's existing universal-property object LeftDerivedPullback by proving that its functor preserves quasi-coherent cohomology. The external product is assembled from those lifts along the two fibre-product projections and a supplied tensor bifunctor on Dqc(X_T). The compactness layer below isolates the exact preservation statements needed to put the resulting generators, and hence their thick envelope, inside the compact objects of Dqc(X_T).

The three layers of Theorem 3.17 this paragraph used to name as next are now available in the current API. The K-flat derived tensor in KFlatBaseChange.lean is one source-faithful producer for the root operation; the source Dqc component is the coproduct-and-extension closure of a compact source sequence in BaseChangeSourceSequence.lean; and pullback/pushforward functoriality is lifted to whole sequences in BaseChangeSequenceFunctoriality.lean. What remains of 3.17 is not the formal closure construction but inhabitation: the compactness preservation statements isolated below, and compact generation on the source, are still supplied rather than proved.

Main definitions #

SchemeBaseChange.CompactDqcFiber: compact objects of Dqc on a base change;
SchemeBaseChange.DqcLeftDerivedPullback: an actual left-derived pullback which preserves the Dqc locus;
SchemeBaseChange.baseChangeExternalProduct: the functor (F, G) ↦ Lφ'^*F ⊗ Lg'^*G;
SchemeBaseChange.DqcLeftDerivedPullback.PreservesCompactObjects and SchemeBaseChange.TensorPreservesCompactObjects: the exact compactness obligations on the supplied geometric operations;
SchemeBaseChange.sourcePerfectPart: the compact part of a source component;
SchemeBaseChange.perfectBaseChangeGenerators and perfectBaseChangeEnvelope: the external-product construction;
SchemeBaseChange.quasicoherentBaseChangeComponent and QuasicoherentBaseChangeCategory: (Dqc)_T;
SchemeBaseChange.boundedBaseChangeComponent and BoundedBaseChangeCategory: D_T.

Reference #

arXiv:1902.08184v4, Proposition 3.15, Theorem 3.17, and Lemma 3.18.