Linearity and the projection formula for derived base change

This file states the two compatibility isomorphisms needed for linearity of base-change functors, using the supplied derived tensor and derived pullback/pushforward interfaces constructed in the preceding files. K-flat resolutions are only one producer of these operations.

The pullback tensorator says that pulling back after tensoring agrees with tensoring the two pullbacks. The projection formula says that pushing forward after tensoring by a pulled-back object agrees with tensoring the pushforward. These are geometric proof obligations rather than new functor slots.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.PullbackTensorCompatibility {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) : Type (u + 1)

Linearity of derived pullback with respect to the supplied derived tensors. For each twist B, this is the natural isomorphism (B ⊗ -) ⋙ Lf^* ≅ Lf^* ⋙ (Lf^* B ⊗ -).

• iso (B : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ U))) : (DU.derivedTensor.obj B).comp pull.functor ≅ pull.functor.comp (DT.derivedTensor.obj (pull.functor.obj B))

  Pullback commutes with left tensor twists.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.ProjectionFormula {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) : Type (u + 1)

The projection formula for the supplied derived tensors and derived pullback/pushforward: Rf_*(Lf^* B ⊗ A) ≅ B ⊗ Rf_* A, naturally in A.

• iso (B : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ U))) : (DT.derivedTensor.obj (pull.functor.obj B)).comp push.functor ≅ push.functor.comp (DU.derivedTensor.obj B)

  The projection-formula isomorphism for each target twist.

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.TensorPreservesQuasicoherentComponent {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (B : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) : Prop

A derived pullback preserves a component after twisting when the corresponding derived tensor endofunctor maps that component to itself.

Equations

• D.TensorPreservesQuasicoherentComponent P B = (D.quasicoherentComponent P ≤ (D.quasicoherentComponent P).inverseImage (D.derivedTensor.obj B))

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentTensor {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (B : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) (hB : D.TensorPreservesQuasicoherentComponent P B) : CategoryTheory.Functor (D.QuasicoherentCategory P) (D.QuasicoherentCategory P)

Tensor by B restricted to the constructed quasicoherent base-change component.

Equations

• D.quasicoherentTensor P B hB = CategoryTheory.ObjectProperty.liftOfLE (D.derivedTensor.obj B) hB

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentTensorCompInclusion {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (B : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) (hB : D.TensorPreservesQuasicoherentComponent P B) : (D.quasicoherentTensor P B hB).comp (D.quasicoherentComponent P).ι ≅ (D.quasicoherentComponent P).ι.comp (D.derivedTensor.obj B)

Forgetting component witnesses recovers tensor by B on Dqc.

Equations

• D.quasicoherentTensorCompInclusion P B hB = (D.quasicoherentComponent P).liftCompιIso ((D.quasicoherentComponent P).ι.comp (D.derivedTensor.obj B)) ⋯

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentPullbackTensorIso {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (hPull : DT.PullbackPreservesQuasicoherentComponent DU P pull) (hTensor : DT.PullbackTensorCompatibility DU pull) (B : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ U))) (hBU : DU.TensorPreservesQuasicoherentComponent P B) (hBT : DT.TensorPreservesQuasicoherentComponent P (pull.functor.obj B)) : (DU.quasicoherentTensor P B hBU).comp (DT.quasicoherentPullback DU P pull hPull) ≅ (DT.quasicoherentPullback DU P pull hPull).comp (DT.quasicoherentTensor P (pull.functor.obj B) hBT)

Pullback tensor compatibility restricted to the constructed quasicoherent base-change components. This is the linearity isomorphism for pullback.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.quasicoherentProjectionFormulaIso {S : Scheme} {X T U : SchemeBaseChange S} {f : T ⟶ U} (DT : X.DerivedBaseChangeData T) (DU : X.DerivedBaseChangeData U) (P : CategoryTheory.ObjectProperty (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left X))) (pull : DqcLeftDerivedPullback (X.baseChangeMap f)) (push : DqcRightDerivedPushforward (X.baseChangeMap f)) (hPush : DT.PushforwardPreservesQuasicoherentComponent DU P push) (hProjection : DT.ProjectionFormula DU pull push) (B : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ U))) (hBT : DT.TensorPreservesQuasicoherentComponent P (pull.functor.obj B)) (hBU : DU.TensorPreservesQuasicoherentComponent P B) : (DT.quasicoherentTensor P (pull.functor.obj B) hBT).comp (DT.quasicoherentPushforward DU P push hPush) ≅ (DT.quasicoherentPushforward DU P push hPush).comp (DU.quasicoherentTensor P B hBU)

The projection formula restricted to the constructed quasicoherent base-change components. This is the linearity isomorphism for pushforward.

Equations

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