Semiorthogonal sequences after scheme base change

This file assembles the componentwise derived operations into the three ordered families appearing in Proposition 3.15 and Theorem 3.17 of arXiv:1902.08184:

• the perfect-envelope sequence on Dqc(X_T);
• its coproduct-and-extension closure, the quasicoherent sequence;
• the inverse-image sequence on the intrinsic bounded-coherent locus.

The geometric semiorthogonality input is split into an additive Hom reduction (ExternalProductHomReduction) and the statement that its source-side objects remain in the later component (PreservesSourceComponents). Source semiorthogonality then proves Hom-vanishing between shifts of the supplied external products. Formal closure extends this first to the perfect envelopes and then, using compactness, to the quasicoherent components. Faithfulness of the bounded-coherent inclusion reflects it to the bounded components.

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.SourceDqc {S : Scheme} (X : SchemeBaseChange S) : Type (u + 1)

Dqc(X) for a scheme over the base, the source side of base change.

Equations

• X.SourceDqc = AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X)

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.TargetDqc {S : Scheme} (X T : SchemeBaseChange S) : Type (u + 1)

Dqc(X_T) on the fibre product, the target side of base change.

Equations

• X.TargetDqc T = AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.TargetPerfect {S : Scheme} (X T : SchemeBaseChange S) : Type (u + 1)

The compact-object model for Perf(X_T).

Equations

• X.TargetPerfect T = CategoryTheory.ObjectProperty.compactObjects.FullSubcategory

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.targetPerfectToDqc {S : Scheme} (X T : SchemeBaseChange S) : CategoryTheory.Functor (X.TargetPerfect T) (X.TargetDqc T)

The canonical inclusion of the compact-object model of Perf(X_T) into Dqc(X_T).

Equations

• X.targetPerfectToDqc T = CategoryTheory.ObjectProperty.compactObjects.ι

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.shiftedPerfectGenerators_triangEnvelope_eq {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) [P.ContainsZero] : (D.shiftedPerfectGenerators P).triangEnvelope = D.perfectEnvelope P

Closing the shifted derived generators under triangles and retracts gives the same perfect envelope as closing the unshifted generators.

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

The geometric Hom-vanishing statement on the supplied derived external products. It is quantified over shifts because the perfect components are their triangulated envelopes.

Equations

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

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.ExternalProductHomReduction {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) : Type (max (u + 1) w)

A tensor-duality/adjunction reduction for morphisms between derived external products.

The reduced object is deliberately separate from any component-membership claim. In a geometric construction, homEquiv is the composite of tensor duality and pullback-pushforward adjunction; preservation of components is the additional S-linearity/projection-formula input below.

• reductionObject ⦃j : ι⦄ : X.SourcePerfectPartCategory (A.component j) → T.CompactDqcFiber → T.CompactDqcFiber → ℤ → ℤ → X.SourceDqc

  The source-side object representing morphisms out of the earlier external-product factor.

• homEquiv ⦃i j : ι⦄ (Fi : X.SourcePerfectPartCategory (A.component i)) (Gi : T.CompactDqcFiber) (Fj : X.SourcePerfectPartCategory (A.component j)) (Gj : T.CompactDqcFiber) (a b : ℤ) : ((CategoryTheory.shiftFunctor (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) a).obj (((D.externalProduct (A.component i)).obj Fi).obj Gi) ⟶ (CategoryTheory.shiftFunctor (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) b).obj (((D.externalProduct (A.component j)).obj Fj).obj Gj)) ≃+ (Fi.obj ⟶ self.reductionObject Fj Gi Gj a b)

  The additive Hom equivalence obtained from duality and adjunction.

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

The source-side reductions stay in the component of their later external-product factor. This is the S-linearity/projection-formula half of the geometric argument.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.ExternalProductHomReduction.hom_eq_zero {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (R : D.ExternalProductHomReduction A) (hR : PreservesSourceComponents D A R) ⦃i j : ι⦄ (hij : i < j) (Fi : X.SourcePerfectPartCategory (A.component i)) (Gi : T.CompactDqcFiber) (Fj : X.SourcePerfectPartCategory (A.component j)) (Gj : T.CompactDqcFiber) (a b : ℤ) (f : (CategoryTheory.shiftFunctor (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) a).obj (((D.externalProduct (A.component i)).obj Fi).obj Gi) ⟶ (CategoryTheory.shiftFunctor (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) b).obj (((D.externalProduct (A.component j)).obj Fj).obj Gj)) : f = 0

Source semiorthogonality kills every target morphism after an additive Hom reduction whose reduced objects remain in the later component.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectExternalProductsSemiorthogonal_of_homReduction {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (R : D.ExternalProductHomReduction A) (hR : ExternalProductHomReduction.PreservesSourceComponents D A R) : D.PerfectExternalProductsSemiorthogonal A

Tensor-duality/adjunction Hom reduction plus source-component preservation proves the derived external-product semiorthogonality obligation.

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

The generator-level geometric Hom-vanishing input: every shifted external-product generator from a later component is right orthogonal to every shifted external-product generator from an earlier component.

Equations

• D.ShiftedPerfectGeneratorsSemiorthogonal A = ∀ ⦃i j : ι⦄, i < j → D.shiftedPerfectGenerators (A.component j) ≤ (D.shiftedPerfectGenerators (A.component i)).rightOrthogonal

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.shiftedPerfectGeneratorsSemiorthogonal_of_externalProducts {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (horth : D.PerfectExternalProductsSemiorthogonal A) : D.ShiftedPerfectGeneratorsSemiorthogonal A

Morphism-level vanishing for the derived external products implies semiorthogonality of their shift-and-isomorphism closures.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectExternalProductsSemiorthogonal_of_shiftedGenerators {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (horth : D.ShiftedPerfectGeneratorsSemiorthogonal A) : D.PerfectExternalProductsSemiorthogonal A

Shifted-generator semiorthogonality implies the derived morphism-level vanishing statement.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectExternalProductsSemiorthogonal_iff_shiftedGenerators {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) : D.PerfectExternalProductsSemiorthogonal A ↔ D.ShiftedPerfectGeneratorsSemiorthogonal A

The paper-facing Hom-vanishing statement is exactly shifted-generator semiorthogonality.

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

The geometric Hom-vanishing input between the perfect base-change envelopes. This obligation is isolated from the formal closure arguments.

Equations

• D.PerfectComponentsSemiorthogonal A = ∀ ⦃i j : ι⦄, i < j → D.perfectEnvelope (A.component j) ≤ (D.perfectEnvelope (A.component i)).rightOrthogonal

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectComponentsSemiorthogonal_of_shiftedGenerators {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hA : A.HasTriangulatedComponents) (horth : D.ShiftedPerfectGeneratorsSemiorthogonal A) : D.PerfectComponentsSemiorthogonal A

Generator-level semiorthogonality implies semiorthogonality of the perfect base-change envelopes. All closure under shifts, cones, and retracts is discharged formally.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectComponentsSemiorthogonal_of_externalProducts {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hA : A.HasTriangulatedComponents) (horth : D.PerfectExternalProductsSemiorthogonal A) : D.PerfectComponentsSemiorthogonal A

Supplied shifted external-product Hom-vanishing implies semiorthogonality of the perfect base-change envelopes.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectComponentsSemiorthogonal_of_homReduction {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hA : A.HasTriangulatedComponents) (R : D.ExternalProductHomReduction A) (hR : ExternalProductHomReduction.PreservesSourceComponents D A R) : D.PerfectComponentsSemiorthogonal A

A tensor-duality/adjunction Hom reduction whose reduced objects stay in the later source component implies semiorthogonality of the perfect base-change envelopes.

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

The sequence of perfect base-change envelopes on Dqc(X_T).

Equations

• D.perfectSequence A horth = { component := fun (i : ι) => D.perfectEnvelope (A.component i), semiorthogonal := horth }

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectSequence_component {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (horth : D.PerfectComponentsSemiorthogonal A) (i : ι) : (D.perfectSequence A horth).component i = D.perfectEnvelope (A.component i)

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

The perfect base-change sequence on the compact-object model of Perf(X_T), obtained by restricting the ambient perfect-envelope sequence.

Equations

• D.perfectCategorySequence A horth = (D.perfectSequence A horth).inverseImage (X.targetPerfectToDqc T)

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectCategorySequence_component {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (horth : D.PerfectComponentsSemiorthogonal A) (i : ι) : (D.perfectCategorySequence A horth).component i = (D.perfectEnvelope (A.component i)).inverseImage (X.targetPerfectToDqc T)

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectCategorySequence_compatible {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (horth : D.PerfectComponentsSemiorthogonal A) : (D.perfectCategorySequence A horth).CompatibleWith (X.targetPerfectToDqc T) (D.perfectSequence A horth)

The compact-object inclusion is compatible with the perfect-category and ambient perfect-envelope sequences.

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

Triangulated source components give triangulated perfect base-change components on the compact-object carrier.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentComponentsSemiorthogonal {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) ⦃i j : ι⦄ : i < j → D.quasicoherentComponent (A.component j) ≤ (D.quasicoherentComponent (A.component i)).rightOrthogonal

Compactness propagates perfect-envelope semiorthogonality to the quasicoherent base-change components.

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentSequence {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) : CategoryTheory.Triangulated.SemiorthogonalSequence (X.TargetDqc T) ι

The quasicoherent base-change sequence (Dqc)_T.

Equations

• D.quasicoherentSequence A hcompact horth = { component := fun (i : ι) => D.quasicoherentComponent (A.component i), semiorthogonal := ⋯ }

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentSequence_component {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) (i : ι) : (D.quasicoherentSequence A hcompact horth).component i = D.quasicoherentComponent (A.component i)

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentSequence_hasTriangulatedComponents {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hA : A.HasTriangulatedComponents) (hcompact : D.PreservesCompactObjects) (horth : D.PerfectComponentsSemiorthogonal A) : (D.quasicoherentSequence A hcompact horth).HasTriangulatedComponents

Triangulated source components give triangulated quasicoherent base-change components.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedSequence {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) : CategoryTheory.Triangulated.SemiorthogonalSequence (Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ T))) ι

The bounded-coherent base-change sequence D_T, obtained by restricting the quasicoherent sequence along the canonical fully faithful inclusion.

Equations

• D.boundedSequence A hcompact horth = (D.quasicoherentSequence A hcompact horth).inverseImage (X.boundedCoherentFiberToDqc T)

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedSequence_component {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) (i : ι) : (D.boundedSequence A hcompact horth).component i = D.boundedComponent (A.component i)

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedSequence_hasTriangulatedComponents {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hA : A.HasTriangulatedComponents) (hcompact : D.PreservesCompactObjects) (horth : D.PerfectComponentsSemiorthogonal A) [(Dqc.schemeBoundedCoherentCohomology (CategoryTheory.Over.left (X ⨯ T))).IsTriangulated] : (D.boundedSequence A hcompact horth).HasTriangulatedComponents

If bounded coherent cohomology is triangulated on the fibre product, then triangulated source components give triangulated bounded base-change components.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedSequence_compatible {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) : (D.boundedSequence A hcompact horth).CompatibleWith (X.boundedCoherentFiberToDqc T) (D.quasicoherentSequence A hcompact horth)

The bounded-coherent inclusion is compatible with the bounded and quasicoherent base-change sequences.