Projection formula for external-product Hom reductions

This file separates the last component-membership input in the semiorthogonality proof into a projection-formula isomorphism and source tensor closure.

The source tensor is constructed from the same K-flat resolution on X that the base-change datum uses for the first pullback. A CompactFiberProjectionFormula identifies the pushforward of a dualized external product with the later source factor tensored by a coefficient on X. Membership then follows either from closure under these coefficients or from the stronger condition that every source component is a right tensor ideal.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.SourceTensorData {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) : Prop

The additional quasicoherence input needed to use the first K-flat resolution as the derived tensor on the source Dqc(X).

• tensorQuasicoherent : D.fstResolution.ResolvedTensorPreservesQuasicoherentCohomology

  Resolved tensor on X preserves quasicoherent cohomology.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.SourceTensorData.derivedTensor {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) (Q : D.SourceTensorData) : CategoryTheory.Functor X.SourceDqc (CategoryTheory.Functor X.SourceDqc X.SourceDqc)

The source K-flat derived tensor selected by SourceTensorData.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.SourceTensorData.derivedTensor D Q = D.fstResolution.derivedTensorToDqc ⋯

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.SourceTensorData.derivedTensor_obj_obj_obj {S : Scheme} {X T : SchemeBaseChange S} (D : X.KFlatBaseChangeData T) (Q : D.SourceTensorData) (E F : X.SourceDqc) : (((derivedTensor D Q).obj E).obj F).obj = (D.fstResolution.derivedTensor.obj E.obj).obj F.obj

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

Every source component is closed under tensoring on the right by an arbitrary object of Dqc(X).

This strong form is useful as a generic sufficient condition. The projection formula below also exposes a weaker coefficient-local condition.

Equations

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

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

Projection formula for the dualized external products used in the Hom reduction.

The coefficient depends only on the two compact fibre factors and shifts. The isomorphism is stated for every source object, independently of a chosen semiorthogonal sequence.

• coefficient : T.CompactDqcFiber → T.CompactDqcFiber → ℤ → ℤ → X.SourceDqc

  The source-side coefficient left after duality and pushforward.

• iso (F : X.SourceDqc) (Gi Gj : T.CompactDqcFiber) (a b : ℤ) : pushFst.functor.obj ((H.rightAdjoint Gi a).obj ((D.toDerivedBaseChangeData.shiftedFiberTensor Gj b).obj (D.pullFst.functor.obj F))) ≅ ((SourceTensorData.derivedTensor D Q).obj F).obj (self.coefficient Gi Gj a b)

  Pushing forward a dualized shifted external tensor is tensoring its source factor by the corresponding coefficient.

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.CompactFiberProjectionFormula.PreservesSourceComponents {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) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) : Prop

The exact source-linearity condition needed for a particular projection formula: its coefficient twists preserve the corresponding source components.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.CompactFiberProjectionFormula.preservesSourceComponents_of_rightTensorClosed {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) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hA : SourceTensorData.RightTensorClosedComponents D Q A) : PreservesSourceComponents D P A

Closure of all source components under right tensor twists implies the coefficient-local source-linearity condition.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.CompactFiberProjectionFormula.pushforwardPreservesSourceComponents {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) (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (hIso : ∀ (j : ι), (A.component j).IsClosedUnderIsomorphisms) (hP : PreservesSourceComponents D P A) : DerivedBaseChangeData.CompactFiberTensorDuality.PushforwardPreservesSourceComponents D.toDerivedBaseChangeData H A pushFst

The projection-formula isomorphism transports source tensor closure back to the pushforward object required by compact-fibre duality.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.perfectComponentsSemiorthogonal_of_projectionFormula {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) (pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)) (adj : D.pullFst.functor ⊣ pushFst.functor) [D.pullFst.functor.Additive] (P : D.CompactFiberProjectionFormula H Q pushFst) (hP : CompactFiberProjectionFormula.PreservesSourceComponents D P A) : D.toDerivedBaseChangeData.PerfectComponentsSemiorthogonal A

Compact-fibre duality, the first-projection formula, and coefficient-local source tensor closure prove perfect-component semiorthogonality.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatBaseChangeData.perfectComponentsSemiorthogonal_of_projectionFormula_of_rightTensorClosed {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) (pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)) (adj : D.pullFst.functor ⊣ pushFst.functor) [D.pullFst.functor.Additive] (P : D.CompactFiberProjectionFormula H Q pushFst) (hTensor : SourceTensorData.RightTensorClosedComponents D Q A) : D.toDerivedBaseChangeData.PerfectComponentsSemiorthogonal A

The same conclusion under the stronger, sequence-wide assumption that every source component is closed under every right tensor twist on Dqc(X).