Functoriality of base-changed semiorthogonal sequences

This file lifts the componentwise pullback, pushforward, and tensor interfaces to the full base-changed sequences of Proposition 3.15 of arXiv:1902.08184. It does not assert new geometric preservation results: the relevant componentwise or perfect-envelope hypotheses remain explicit.

The linearity and projection-formula isomorphisms are likewise assembled as families indexed by the components of the original sequence.

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.PullbackPreservesQuasicoherentSequence {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} {ι : Type w} [Preorder ι] (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) : Prop

Pullback preserves every quasicoherent component of a base-changed sequence.

Equations

• DT.PullbackPreservesQuasicoherentSequence DU A pull = ∀ (i : ι), DT.PullbackPreservesQuasicoherentComponent DU (A.component i) pull

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.PullbackMapsPerfectSequence {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} {ι : Type w} [Preorder ι] (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) : Prop

Pullback maps every perfect envelope into the corresponding target quasicoherent component.

Equations

• DT.PullbackMapsPerfectSequence DU A pull = ∀ (i : ι), DT.PullbackMapsPerfectEnvelope DU (A.component i) pull

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.pullback_preservesQuasicoherentSequence_of_perfectSequence {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} {ι : Type w} [Preorder ι] (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) [pull.functor.CommShift ℤ] [pull.functor.IsTriangulated] (hCoproducts : pull.functor.PreservesSmallCoproducts) (hPerfect : DT.PullbackMapsPerfectSequence DU A pull) : DT.PullbackPreservesQuasicoherentSequence DU A pull

Perfect-envelope preservation and cocontinuity imply preservation of all quasicoherent components at once.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentSequence_pullback_compatible {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} {ι : Type w} [Preorder ι] (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hcompactT : DT.PreservesCompactObjects) (hcompactU : DU.PreservesCompactObjects) (horthT : DT.PerfectComponentsSemiorthogonal A) (horthU : DU.PerfectComponentsSemiorthogonal A) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (hPull : DT.PullbackPreservesQuasicoherentSequence DU A pull) : (DU.quasicoherentSequence A hcompactU horthU).CompatibleWith pull.functor (DT.quasicoherentSequence A hcompactT horthT)

Pullback is compatible with the two quasicoherent base-change sequences.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedSequence_pullback_compatible {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} {ι : Type w} [Preorder ι] (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hcompactT : DT.PreservesCompactObjects) (hcompactU : DU.PreservesCompactObjects) (horthT : DT.PerfectComponentsSemiorthogonal A) (horthU : DU.PerfectComponentsSemiorthogonal A) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (hPull : DT.PullbackPreservesQuasicoherentSequence DU A pull) (hBounded : pull.PreservesBoundedCoherent) : (DU.boundedSequence A hcompactU horthU).CompatibleWith (pull.boundedFunctor hBounded) (DT.boundedSequence A hcompactT horthT)

Pullback is compatible with the bounded base-change sequences whenever it preserves intrinsic bounded-coherent cohomology.

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.PushforwardPreservesQuasicoherentSequence {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} {ι : Type w} [Preorder ι] (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) : Prop

Pushforward preserves every quasicoherent component of a base-changed sequence.

Equations

• DT.PushforwardPreservesQuasicoherentSequence DU A push = ∀ (i : ι), DT.PushforwardPreservesQuasicoherentComponent DU (A.component i) push

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.PushforwardMapsPerfectSequence {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} {ι : Type w} [Preorder ι] (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) : Prop

Pushforward maps every perfect envelope into the corresponding target quasicoherent component.

Equations

• DT.PushforwardMapsPerfectSequence DU A push = ∀ (i : ι), DT.PushforwardMapsPerfectEnvelope DU (A.component i) push

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.pushforward_preservesQuasicoherentSequence_of_perfectSequence {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} {ι : Type w} [Preorder ι] (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) [push.functor.CommShift ℤ] [push.functor.IsTriangulated] (hCoproducts : push.functor.PreservesSmallCoproducts) (hPerfect : DT.PushforwardMapsPerfectSequence DU A push) : DT.PushforwardPreservesQuasicoherentSequence DU A push

Perfect-envelope preservation and cocontinuity imply preservation of all quasicoherent components under pushforward.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentSequence_pushforward_compatible {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} {ι : Type w} [Preorder ι] (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hcompactT : DT.PreservesCompactObjects) (hcompactU : DU.PreservesCompactObjects) (horthT : DT.PerfectComponentsSemiorthogonal A) (horthU : DU.PerfectComponentsSemiorthogonal A) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) (hPush : DT.PushforwardPreservesQuasicoherentSequence DU A push) : (DT.quasicoherentSequence A hcompactT horthT).CompatibleWith push.functor (DU.quasicoherentSequence A hcompactU horthU)

Pushforward is compatible with the two quasicoherent base-change sequences.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedSequence_pushforward_compatible {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} {ι : Type w} [Preorder ι] (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hcompactT : DT.PreservesCompactObjects) (hcompactU : DU.PreservesCompactObjects) (horthT : DT.PerfectComponentsSemiorthogonal A) (horthU : DU.PerfectComponentsSemiorthogonal A) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) (hPush : DT.PushforwardPreservesQuasicoherentSequence DU A push) (hBounded : push.PreservesBoundedCoherent) : (DT.boundedSequence A hcompactT horthT).CompatibleWith (push.boundedFunctor hBounded) (DU.boundedSequence A hcompactU horthU)

Pushforward is compatible with the bounded base-change sequences whenever it preserves intrinsic bounded-coherent cohomology.

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

Tensor by B preserves every quasicoherent component of the sequence.

Equations

• D.TensorPreservesQuasicoherentSequence A B = ∀ (i : ι), D.TensorPreservesQuasicoherentComponent (A.component i) B

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentSequence_tensor_compatible {S : Scheme} {X T : SchemeBaseChange S} {ι : Type w} [Preorder ι] (D : X.DerivedBaseChangeData T) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hcompact : D.PreservesCompactObjects) (horth : D.PerfectComponentsSemiorthogonal A) (B : X.TargetDqc T) (hTensor : D.TensorPreservesQuasicoherentSequence A B) : (D.quasicoherentSequence A hcompact horth).CompatibleWith (D.derivedTensor.obj B) (D.quasicoherentSequence A hcompact horth)

Tensor by B is compatible with the quasicoherent base-change sequence.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentSequencePullbackTensorIso {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} {ι : Type w} [Preorder ι] (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (hPull : DT.PullbackPreservesQuasicoherentSequence DU A pull) (hTensor : DT.PullbackTensorCompatibility DU pull) (B : X.TargetDqc U) (hBU : DU.TensorPreservesQuasicoherentSequence A B) (hBT : DT.TensorPreservesQuasicoherentSequence A (pull.functor.obj B)) (i : ι) : (DU.quasicoherentTensor (A.component i) B ⋯).comp (DT.quasicoherentPullback DU (A.component i) pull ⋯) ≅ (DT.quasicoherentPullback DU (A.component i) pull ⋯).comp (DT.quasicoherentTensor (A.component i) (pull.functor.obj B) ⋯)

Pullback linearity, simultaneously parameterized by every component of the base-changed sequence.

Equations

• DT.quasicoherentSequencePullbackTensorIso DU A pull hPull hTensor B hBU hBT i = DT.quasicoherentPullbackTensorIso DU (A.component i) pull ⋯ hTensor B ⋯ ⋯

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentSequenceProjectionFormulaIso {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} {ι : Type w} [Preorder ι] (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) (hPush : DT.PushforwardPreservesQuasicoherentSequence DU A push) (hProjection : DT.ProjectionFormula DU pull push) (B : X.TargetDqc U) (hBT : DT.TensorPreservesQuasicoherentSequence A (pull.functor.obj B)) (hBU : DU.TensorPreservesQuasicoherentSequence A B) (i : ι) : (DT.quasicoherentTensor (A.component i) (pull.functor.obj B) ⋯).comp (DT.quasicoherentPushforward DU (A.component i) push ⋯) ≅ (DT.quasicoherentPushforward DU (A.component i) push ⋯).comp (DU.quasicoherentTensor (A.component i) B ⋯)

The projection formula, simultaneously parameterized by every component of the base-changed sequence.

Equations

• DT.quasicoherentSequenceProjectionFormulaIso DU A pull push hPush hProjection B hBT hBU i = DT.quasicoherentProjectionFormulaIso DU (A.component i) pull push ⋯ hProjection B ⋯ ⋯