Compact-fibre tensor duality after base change

This file realizes the tensor-duality half of the external-product Hom reduction as an adjunction for the supplied derived tensor. For a compact object G of Dqc(T), shiftedFiberTensor D G a tensors on the right by its pullback to X_T and then shifts by a. A right adjoint to this functor is the precise duality input needed to expose the earlier source factor in a Hom between shifted external products.

No global monoidal structure on unbounded Dqc is assumed. This keeps the interface at the level currently supplied by the repository. A K-flat resolution is one producer of the bundled tensor, but the duality witness itself is stated for whatever derived tensor the bundle carries.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.fiberTensor {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (G : T.CompactDqcFiber) : CategoryTheory.Functor (X.TargetDqc T) (X.TargetDqc T)

Tensor on the right by the pullback of a compact object of Dqc(T).

Equations

• D.fiberTensor G = D.derivedTensor.flip.obj (D.pullSnd.functor.obj G.obj)

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.fiberTensor_obj {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (G : T.CompactDqcFiber) (E : X.TargetDqc T) : (D.fiberTensor G).obj E = (D.derivedTensor.obj E).obj (D.pullSnd.functor.obj G.obj)

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.shiftedFiberTensor {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (G : T.CompactDqcFiber) (a : ℤ) : CategoryTheory.Functor (X.TargetDqc T) (X.TargetDqc T)

Tensor by a pulled-back compact fibre object and then shift.

Equations

• D.shiftedFiberTensor G a = (D.fiberTensor G).comp (CategoryTheory.shiftFunctor (X.TargetDqc T) a)

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.shiftedFiberTensor_obj {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (G : T.CompactDqcFiber) (a : ℤ) (E : X.TargetDqc T) : (D.shiftedFiberTensor G a).obj E = (CategoryTheory.shiftFunctor (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) a).obj ((D.derivedTensor.obj E).obj (D.pullSnd.functor.obj G.obj))

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.shiftedFiberTensor_obj_pullFst {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) (P : CategoryTheory.ObjectProperty X.SourceDqc) (F : X.SourcePerfectPartCategory P) (G : T.CompactDqcFiber) (a : ℤ) : (D.shiftedFiberTensor G a).obj (D.pullFst.functor.obj F.obj) = (CategoryTheory.shiftFunctor (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) a).obj (((D.externalProduct P).obj F).obj G)

On a pulled-back source object, shiftedFiberTensor is definitionally the shifted derived external product used to generate the base-change component.

Not a simp lemma: shiftedFiberTensor_obj already rewrites this left-hand side, so it could never fire. It stays as the named definitional bridge.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.CompactFiberTensorDuality {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) : Type (u + 1)

Duality for compact fibre factors, expressed as a right adjoint to the supplied shifted derived tensor twist.

Additivity is recorded explicitly because the downstream semiorthogonality argument uses an additive Hom equivalence, while the current unbounded tensor API does not yet bundle exactness or monoidal coherence.

• rightAdjoint (G : T.CompactDqcFiber) (a : ℤ) : CategoryTheory.Functor (X.TargetDqc T) (X.TargetDqc T)

  The dual tensor-and-shift functor.

• left_additive (G : T.CompactDqcFiber) (a : ℤ) : (D.shiftedFiberTensor G a).Additive

  Tensoring by the compact factor and shifting is additive.

• adjunction (G : T.CompactDqcFiber) (a : ℤ) : D.shiftedFiberTensor G a ⊣ self.rightAdjoint G a

  The tensor-duality adjunction.

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

A compact-fibre tensor adjunction supplies the target-side Hom reduction for every source semiorthogonal sequence.

Equations

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

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

The remaining geometric obligation after compact-fibre duality: pushing the dualized later external product to X preserves its source component.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.CompactFiberTensorDuality.toExternalProductTensorDuality_preservesSourceComponents {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (H : D.CompactFiberTensorDuality) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)) (hH : PushforwardPreservesSourceComponents D H A pushFst) : ExternalProductTensorDuality.PushforwardPreservesSourceComponents D A (toExternalProductTensorDuality D H A) pushFst

The compact-fibre pushforward obligation is exactly the preservation condition required by the induced target-side Hom reduction.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectComponentsSemiorthogonal_of_compactFiberTensorDuality {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hA : A.HasTriangulatedComponents) (H : D.CompactFiberTensorDuality) (pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)) (adj : D.pullFst.functor ⊣ pushFst.functor) [D.pullFst.functor.Additive] (hH : CompactFiberTensorDuality.PushforwardPreservesSourceComponents D H A pushFst) : D.PerfectComponentsSemiorthogonal A

Compact-fibre tensor duality, pullback-pushforward adjunction, and the remaining pushforward-membership input prove semiorthogonality of the perfect base-change envelopes.