Generation and fullness after scheme base change

This file isolates the generation inputs in Proposition 3.15 from the semiorthogonality construction. The bundled derived external products define a generator property on the compact carrier. A K-flat resolution is only one producer of the bundle; if the resulting objects classically generate, the perfect base-change sequence is full.

For Dqc, compact generation reduces fullness to two formal compatibility facts: perfect filtrations remain quasicoherent filtrations after forgetting compactness, and the resulting total envelope is closed under coproducts. Neither fact is replaced by a prepackaged fullness assumption.

The SF11.1 follow-up keeps these facts as geometry-owner inputs: the formal theorem below propagates them to Dqc fullness, but the structure fields are not themselves proofs that compact generation or filtration compatibility holds for every scheme base change.

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectCategoryExternalProductGenerators {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) : CategoryTheory.ObjectProperty (X.TargetPerfect T)

Bundled derived external products, regarded as objects of the compact carrier of Dqc(X_T).

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectCategoryExternalProductGenerators_le_total {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (horth : D.PerfectComponentsSemiorthogonal A) : D.perfectCategoryExternalProductGenerators A ≤ (D.perfectCategorySequence A horth).total

Every external-product generator lies in the total property of the perfect base-change sequence.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectCategorySequence_isFull_of_externalProducts {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (horth : D.PerfectComponentsSemiorthogonal A) (hgen : (D.perfectCategoryExternalProductGenerators A).IsClassicalTriangulatedGenerator) : (D.perfectCategorySequence A horth).IsFull

External-product generation implies fullness of the perfect base-change sequence.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.QuasicoherentFullnessPropagationData {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hcompact : D.PreservesCompactObjects) (horth : D.PerfectComponentsSemiorthogonal A) : Prop

The compatibility data needed to propagate perfect fullness to Dqc.

perfectToQuasicoherent is a filtration comparison, not a fullness field: it only says that a finite perfect filtration remains a finite filtration after forgetting compactness. Compact generation and coproduct closure then prove quasicoherent fullness.

• targetCompactlyGenerated : CategoryTheory.ObjectProperty.compactObjects.coprodClosure = ⊤

  Compact objects generate the target Dqc category.

• perfectToQuasicoherent (E : X.TargetPerfect T) : (D.perfectCategorySequence A horth).total.triangEnvelope E → (D.quasicoherentSequence A hcompact horth).total.triangEnvelope E.obj

  Perfect filtrations remain filtrations by the quasicoherent components after applying the compact-object inclusion.

• quasicoherentEnvelopeCoproducts (κ : Type u) : (D.quasicoherentSequence A hcompact horth).total.triangEnvelope.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete κ)

  The finite envelope of the quasicoherent components is closed under scheme-universe coproducts.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.QuasicoherentFullnessPropagationData.quasicoherentSequence_isFull {S : Scheme} {X T : SchemeBaseChange S} {D : X.DerivedBaseChangeData T} {ι : Type w} [Preorder ι] {A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι} {hcompact : D.PreservesCompactObjects} {horth : D.PerfectComponentsSemiorthogonal A} (G : D.QuasicoherentFullnessPropagationData A hcompact horth) (hperfect : (D.perfectCategorySequence A horth).IsFull) : (D.quasicoherentSequence A hcompact horth).IsFull

Perfect fullness propagates to quasicoherent fullness through compact generation and the stated filtration/coproduct compatibilities.