Decomposition data for base-changed sequences

The sequence constructors isolate semiorthogonality formally. This file packages the remaining geometric content of Proposition 3.15 of arXiv:1902.08184: generation, admissible component projections, and cocontinuity of the Dqc projections.

No field is manufactured from the K-flat construction. In particular, fullness and right adjoints remain explicit obligations. Once supplied, the generic projection API turns the chosen adjoints into paper-strong semiorthogonal decompositions.

For the bounded-coherent restriction, triangulatedness of the intrinsic bounded-coherent locus is an explicit typeclass hypothesis. This is essential over a non-Noetherian scheme: finite-presentation cohomology is not closed under cones without additional geometry.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.DecompositionData {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) : Type (max (u + 1) w)

The remaining geometric data making the perfect and quasicoherent base-change sequences into full strong decompositions.

• sourceComponentsTriangulated : A.HasTriangulatedComponents

  Each source component is triangulated. The corresponding perfect and quasicoherent base-change components are then triangulated formally.

• perfectFull : (D.perfectCategorySequence A horth).IsFull

  The perfect components generate the compact-object carrier.

• perfectProjections : (D.perfectCategorySequence A horth).RightProjectionData

  Chosen right projections onto all perfect components.

• quasicoherentFull : (D.quasicoherentSequence A hcompact horth).IsFull

  The quasicoherent components generate Dqc(X_T).

• quasicoherentProjections : (D.quasicoherentSequence A hcompact horth).RightProjectionData

  Chosen right projections onto all quasicoherent components.

• quasicoherentProjectionCocontinuous (i : ι) : (self.quasicoherentProjections.ambientProjection i).PreservesSmallCoproducts

  The ambient Dqc projection endofunctors preserve all coproducts in the scheme universe.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.DecompositionData.perfectIsStrong {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} (B : D.DecompositionData A hcompact horth) : (D.perfectCategorySequence A horth).IsStrong

The perfect-category sequence is strong in the paper's sense.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.DecompositionData.quasicoherentIsStrong {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} (B : D.DecompositionData A hcompact horth) : (D.quasicoherentSequence A hcompact horth).IsStrong

The quasicoherent sequence is strong in the paper's sense.

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.DecompositionData.boundedLocus {S : Scheme} {X T : SchemeBaseChange S} : CategoryTheory.ObjectProperty (X.TargetDqc T)

The bounded-coherent object property on the fibre product.

Equations

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

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.DecompositionData.BoundedData {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} (B : D.DecompositionData A hcompact horth) [boundedLocus.IsTriangulated] : Prop

Additional data needed to restrict the quasicoherent decomposition to the bounded-coherent locus.

• projectionsPreserveBounded : B.quasicoherentProjections.Preserves boundedLocus

  Every quasicoherent projector preserves bounded coherent cohomology.

• full : (D.boundedSequence A hcompact horth).IsFull

  The restricted components generate the bounded-coherent carrier.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.DecompositionData.BoundedData.projections {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} (B : D.DecompositionData A hcompact horth) [boundedLocus.IsTriangulated] (BB : B.BoundedData) : (D.boundedSequence A hcompact horth).RightProjectionData

The chosen component projections restricted to bounded coherent cohomology.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.DecompositionData.BoundedData.isStrong {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} (B : D.DecompositionData A hcompact horth) [boundedLocus.IsTriangulated] (BB : B.BoundedData) : (D.boundedSequence A hcompact horth).IsStrong

The bounded sequence is strong once the quasicoherent projectors preserve bounded coherent cohomology.