Base-scheme linearity for external-product semiorthogonality

This file refines the source tensor-closure hypothesis used by the first-projection formula to the S-linearity appearing in Proposition 3.15. It exposes both levels of the base action:

• compact objects of Dqc(S), modeling the original Perf(S)-linear decomposition; and
• arbitrary objects of Dqc(S), modeling its presentable quasicoherent extension.

Both act on Dqc(X) by genuine derived pullback along X → S, followed by the K-flat source tensor. A projection coefficient pulled back from the corresponding level on the base then gives the coefficient-local closure required by the semiorthogonality argument.

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.BaseDqc (S : Scheme) : Type (u + 1)

The quasicoherent derived category of the base scheme.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.BaseDqc S = AlgebraicGeometry.DerivedCategory.Dqc.SchemeQuasicoherentDerivedCategory S

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.CompactBaseDqc (S : Scheme) : Type (u + 1)

The compact objects of Dqc(S), modeling Perf(S) in this layer.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.CompactBaseDqc S = CategoryTheory.ObjectProperty.compactObjects.FullSubcategory

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.SourceTensorData.dqcBaseActionInBase {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) (Q : D.SourceTensorData) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) (F : X.SourceDqc) : CategoryTheory.Functor (BaseDqc S) X.SourceDqc

For a fixed source object, the base-variable action functor: pull back from S to X, then tensor on the right.

Equations

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

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.SourceTensorData.dqcBaseActionInBase_obj {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) (Q : D.SourceTensorData) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) (F : X.SourceDqc) (B : BaseDqc S) : (dqcBaseActionInBase D Q pullBase F).obj B = ((derivedTensor D Q).obj F).obj (pullBase.functor.obj B)

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.SourceTensorData.dqcBaseAction {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) (Q : D.SourceTensorData) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) (B : BaseDqc S) : CategoryTheory.Functor X.SourceDqc X.SourceDqc

The action of an arbitrary quasicoherent base object on Dqc(X): pull it back along X → S, then tensor by it on the right.

Equations

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

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.SourceTensorData.dqcBaseAction_obj {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) (Q : D.SourceTensorData) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) (B : BaseDqc S) (F : X.SourceDqc) : (dqcBaseAction D Q pullBase B).obj F = ((derivedTensor D Q).obj F).obj (pullBase.functor.obj B)

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.SourceTensorData.baseAction {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) (Q : D.SourceTensorData) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) (B : CompactBaseDqc S) : CategoryTheory.Functor X.SourceDqc X.SourceDqc

The action of a compact base object on Dqc(X): pull it back along X → S, then tensor by it on the right.

Equations

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

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.SourceTensorData.baseAction_obj {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) (Q : D.SourceTensorData) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) (B : CompactBaseDqc S) (F : X.SourceDqc) : (baseAction D Q pullBase B).obj F = ((derivedTensor D Q).obj F).obj (pullBase.functor.obj B.obj)

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.SourceTensorData.SLinearComponents {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {ι : Type w} [Preorder ι] (Q : D.SourceTensorData) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) : Prop

Paper-level S-linearity of the source semiorthogonal sequence: every component is preserved by the action of every compact object of Dqc(S).

Equations

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

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.SourceTensorData.DqcSLinearComponents {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {ι : Type w} [Preorder ι] (Q : D.SourceTensorData) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) : Prop

Dqc(S)-linearity of the quasicoherent source components. This is the presentable extension of S-linearity used when a projection coefficient on the base is quasicoherent but not necessarily compact.

Equations

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

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.SourceTensorData.PresentableBaseActionData {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) (Q : D.SourceTensorData) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) : Type (u + 1)

Presentability data needed to extend the compact base action to all of Dqc(S).

The base is generated from compact objects by coproducts and extensions, and for each fixed source object the action in the base variable is exact and preserves the relevant small coproducts.

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

  Compact objects generate Dqc(S) under coproducts and extensions.

• actionCommShift (F : X.SourceDqc) : (dqcBaseActionInBase D Q pullBase F).CommShift ℤ

  The action in the base variable commutes with shifts.

• actionTriangulated (F : X.SourceDqc) : (dqcBaseActionInBase D Q pullBase F).IsTriangulated

  The action in the base variable is triangulated.

• actionCocontinuous (F : X.SourceDqc) : (dqcBaseActionInBase D Q pullBase F).PreservesSmallCoproducts

  The action in the base variable preserves scheme-universe coproducts.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.SourceTensorData.PresentableBaseActionData.dqcSLinearComponents {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {ι : Type w} [Preorder ι] (Q : D.SourceTensorData) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) (G : PresentableBaseActionData D Q pullBase) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hA : A.HasTriangulatedComponents) (hIso : ∀ (j : ι), (A.component j).IsClosedUnderIsomorphisms) (hCoprod : ∀ (j : ι) (κ : Type u), (A.component j).IsClosedUnderColimitsOfShape (CategoryTheory.Discrete κ)) (hS : SLinearComponents D Q pullBase A) : DqcSLinearComponents D Q pullBase A

Perf(S)-linearity extends to Dqc(S)-linearity when compact objects generate the base and the base action preserves triangles and coproducts.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.CompactFiberProjectionFormula.BaseCoefficientData {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {H : D.toDerivedBaseChangeData.CompactFiberTensorDuality} {Q : D.SourceTensorData} {pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)} (P : D.CompactFiberProjectionFormula H Q pushFst) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) : Type (u + 1)

Evidence that all source coefficients in a compact-fibre projection formula come by derived pullback from compact objects on the base scheme.

• baseCoefficient : T.CompactDqcFiber → T.CompactDqcFiber → ℤ → ℤ → CompactBaseDqc S

  The compact object on S representing each source coefficient.

• coefficientIso (Gi Gj : T.CompactDqcFiber) (a b : ℤ) : P.coefficient Gi Gj a b ≅ pullBase.functor.obj (self.baseCoefficient Gi Gj a b).obj

  The projection coefficient is the pullback of its representing base object.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.CompactFiberProjectionFormula.DqcBaseCoefficientData {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {H : D.toDerivedBaseChangeData.CompactFiberTensorDuality} {Q : D.SourceTensorData} {pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)} (P : D.CompactFiberProjectionFormula H Q pushFst) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) : Type (u + 1)

Evidence that all projection-formula coefficients are pulled back from quasicoherent objects on the base. Unlike BaseCoefficientData, this does not require those objects to be compact.

• baseCoefficient : T.CompactDqcFiber → T.CompactDqcFiber → ℤ → ℤ → BaseDqc S

  The quasicoherent object on S representing each coefficient.

• coefficientIso (Gi Gj : T.CompactDqcFiber) (a b : ℤ) : P.coefficient Gi Gj a b ≅ pullBase.functor.obj (self.baseCoefficient Gi Gj a b)

  The projection coefficient is the pullback of its representing base object.

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.CompactFiberProjectionFormula.BaseCoefficientData.toDqc {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {H : D.toDerivedBaseChangeData.CompactFiberTensorDuality} {Q : D.SourceTensorData} {pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)} {P : D.CompactFiberProjectionFormula H Q pushFst} {pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange} (C : BaseCoefficientData D P pullBase) : DqcBaseCoefficientData D P pullBase

Compact base coefficients can be forgotten to quasicoherent base coefficients.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.CompactFiberProjectionFormula.preservesSourceComponents_of_sLinear {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {ι : Type w} [Preorder ι] {H : D.toDerivedBaseChangeData.CompactFiberTensorDuality} {Q : D.SourceTensorData} {pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)} (P : D.CompactFiberProjectionFormula H Q pushFst) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) (C : BaseCoefficientData D P pullBase) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hIso : ∀ (j : ι), (A.component j).IsClosedUnderIsomorphisms) (hS : SourceTensorData.SLinearComponents D Q pullBase A) : PreservesSourceComponents D P A

Base coefficients and S-linearity imply the coefficient-local source component preservation required by the projection formula.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.CompactFiberProjectionFormula.preservesSourceComponents_of_dqcSLinear {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {ι : Type w} [Preorder ι] {H : D.toDerivedBaseChangeData.CompactFiberTensorDuality} {Q : D.SourceTensorData} {pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)} (P : D.CompactFiberProjectionFormula H Q pushFst) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) (C : DqcBaseCoefficientData D P pullBase) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hIso : ∀ (j : ι), (A.component j).IsClosedUnderIsomorphisms) (hS : SourceTensorData.DqcSLinearComponents D Q pullBase A) : PreservesSourceComponents D P A

Quasicoherent base coefficients and Dqc(S)-linearity imply the exact coefficient-local preservation required by the projection formula.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.perfectComponentsSemiorthogonal_of_projectionFormula_of_sLinear {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hA : A.HasTriangulatedComponents) (hIso : ∀ (j : ι), (A.component j).IsClosedUnderIsomorphisms) (H : D.toDerivedBaseChangeData.CompactFiberTensorDuality) (Q : D.SourceTensorData) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) (pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)) (adj : D.pullFst.functor ⊣ pushFst.functor) [D.pullFst.functor.Additive] (P : D.CompactFiberProjectionFormula H Q pushFst) (C : CompactFiberProjectionFormula.BaseCoefficientData D P pullBase) (hS : SourceTensorData.SLinearComponents D Q pullBase A) : D.toDerivedBaseChangeData.PerfectComponentsSemiorthogonal A

Compact-fibre duality, a first-projection formula with base coefficients, and S-linearity of the source sequence prove perfect-component semiorthogonality after base change.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.perfectComponentsSemiorthogonal_of_projectionFormula_of_dqcSLinear {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hA : A.HasTriangulatedComponents) (hIso : ∀ (j : ι), (A.component j).IsClosedUnderIsomorphisms) (H : D.toDerivedBaseChangeData.CompactFiberTensorDuality) (Q : D.SourceTensorData) (pullBase : DqcLeftDerivedPullback X.toIdentityBaseChange) (pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)) (adj : D.pullFst.functor ⊣ pushFst.functor) [D.pullFst.functor.Additive] (P : D.CompactFiberProjectionFormula H Q pushFst) (C : CompactFiberProjectionFormula.DqcBaseCoefficientData D P pullBase) (hS : SourceTensorData.DqcSLinearComponents D Q pullBase A) : D.toDerivedBaseChangeData.PerfectComponentsSemiorthogonal A

Compact-fibre duality, a first-projection formula with quasicoherent base coefficients, and Dqc(S)-linearity of the source sequence prove perfect-component semiorthogonality after base change.