The source quasicoherent sequence of a compact source sequence

Theorem 3.17 of arXiv:1902.08184 starts from a strong semiorthogonal component 𝒟 ⊆ Dᵇ(X) and works throughout with its quasicoherent companion 𝒟qc ⊆ Dqc(X). Every theorem in the base-change layer so far takes that companion as an input A : SemiorthogonalSequence (SourceDqc X) ι, and carries three standing hypotheses about it: triangulated components, repleteness, and closure under coproducts in the scheme universe.

This file removes all three for the sequence the paper actually uses. Given a semiorthogonal sequence of compact source components -- the perfect side -- closing each component under coproducts and extensions produces the source sequence, and the three hypotheses become theorems. BaseChangeCategory.lean named this construction as one of the remaining layers of Theorem 3.17.

The geometry is in the other direction, and is not proved here. Recovering the compact part of the closure as the original component is compact generation: Dqc.PerfectObjectsAreCompactInDqc is the repository's name for the comparison that would identify these compact objects with perfect complexes, and it is deliberately uninhabited. Only the inclusion that is formal is recorded -- a compact component sits inside the perfect part of its own closure.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.sourceQuasicoherentSequence {S : Scheme} {X : SchemeBaseChange S} {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hcompact : ∀ (i : ι), A.component i ≤ CategoryTheory.ObjectProperty.compactObjects) : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι

The source quasicoherent sequence 𝒟qc, generated by a semiorthogonal sequence of compact source components.

Semiorthogonality of the closure is not assumed: it follows from semiorthogonality of the compact components, because compactness carries Hom-vanishing across the coproducts being adjoined.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.sourceQuasicoherentSequence A hcompact = A.coprodClosure hcompact

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.sourceQuasicoherentSequence_component {S : Scheme} {X : SchemeBaseChange S} {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hcompact : ∀ (i : ι), A.component i ≤ CategoryTheory.ObjectProperty.compactObjects) (i : ι) : (sourceQuasicoherentSequence A hcompact).component i = (A.component i).coprodClosure

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.sourceQuasicoherentSequence_hasTriangulatedComponents {S : Scheme} {X : SchemeBaseChange S} {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hcompact : ∀ (i : ι), A.component i ≤ CategoryTheory.ObjectProperty.compactObjects) (hA : A.HasTriangulatedComponents) : (sourceQuasicoherentSequence A hcompact).HasTriangulatedComponents

Triangulated components, the first of the three standing hypotheses.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.sourceQuasicoherentSequence_isClosedUnderIsomorphisms {S : Scheme} {X : SchemeBaseChange S} {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hcompact : ∀ (i : ι), A.component i ≤ CategoryTheory.ObjectProperty.compactObjects) (i : ι) : ((sourceQuasicoherentSequence A hcompact).component i).IsClosedUnderIsomorphisms

Repleteness, the second standing hypothesis, with no input at all.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.sourceQuasicoherentSequence_isClosedUnderColimitsOfShape {S : Scheme} {X : SchemeBaseChange S} {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hcompact : ∀ (i : ι), A.component i ≤ CategoryTheory.ObjectProperty.compactObjects) (i : ι) (κ : Type u) : ((sourceQuasicoherentSequence A hcompact).component i).IsClosedUnderColimitsOfShape (CategoryTheory.Discrete κ)

Closure under coproducts in the scheme universe, the third standing hypothesis, with no input at all.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.le_sourcePerfectPart_sourceQuasicoherentSequence {S : Scheme} {X : SchemeBaseChange S} {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hcompact : ∀ (i : ι), A.component i ≤ CategoryTheory.ObjectProperty.compactObjects) (i : ι) : A.component i ≤ X.sourcePerfectPart ((sourceQuasicoherentSequence A hcompact).component i)

A compact source component lies in the perfect part of its own closure.

The reverse inclusion -- that the closure adjoins no new compact objects -- is compact generation, and is a geometric input rather than a consequence.