Tensor-duality and adjunction Hom reductions after base change

This file splits the geometric Hom reduction for external products into two composable inputs. ExternalProductTensorDuality moves the earlier pullback factor out of the source external product, leaving a morphism out of pullFst.obj Fi. The pullback-pushforward adjunction then returns that Hom to the source category.

The remaining component-membership statement is isolated as PushforwardPreservesSourceComponents; geometrically, this is where S-linearity and a projection formula enter. Together these inputs imply the perfect-component semiorthogonality required by the base-change sequence.

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.ExternalProductTensorDuality {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) : Type (max (u + 1) w)

The target-side tensor-duality part of the external-product Hom reduction.

The object dualizedTarget Fj Gi Gj a b packages the later external product, the dual of the earlier compact fibre factor, and the two shifts. Its precise geometric construction is left independent of the formal adjunction step.

• dualizedTarget ⦃j : ι⦄ : X.SourcePerfectPartCategory (A.component j) → T.CompactDqcFiber → T.CompactDqcFiber → ℤ → ℤ → X.TargetDqc T

  The target-side object left after tensor duality exposes the first pullback factor.

• homEquiv ⦃i j : ι⦄ (Fi : X.SourcePerfectPartCategory (A.component i)) (Gi : T.CompactDqcFiber) (Fj : X.SourcePerfectPartCategory (A.component j)) (Gj : T.CompactDqcFiber) (a b : ℤ) : ((CategoryTheory.shiftFunctor (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) a).obj (((D.externalProduct (A.component i)).obj Fi).obj Gi) ⟶ (CategoryTheory.shiftFunctor (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) b).obj (((D.externalProduct (A.component j)).obj Fj).obj Gj)) ≃+ (D.pullFst.functor.obj Fi.obj ⟶ self.dualizedTarget Fj Gi Gj a b)

  Tensor duality rewrites a Hom between external products as a Hom out of the pullback of the earlier source factor.

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

The pushforwards of the tensor-dualized target objects remain in the source component of their later external-product factor.

This is the component-membership input expected from S-linearity and a projection formula.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.ExternalProductTensorDuality.toHomReduction {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (H : D.ExternalProductTensorDuality A) (pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)) (adj : D.pullFst.functor ⊣ pushFst.functor) [D.pullFst.functor.Additive] : D.ExternalProductHomReduction A

Compose target-side tensor duality with pullback-pushforward adjunction to obtain the source-side external-product Hom reduction.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.ExternalProductTensorDuality.toHomReduction_preservesSourceComponents {S : Scheme} {X T : SchemeBaseChange S} (D : X.DerivedBaseChangeData T) {ι : Type w} [Preorder ι] (A : CategoryTheory.Triangulated.SemiorthogonalSequence X.SourceDqc ι) (H : D.ExternalProductTensorDuality A) (pushFst : DqcRightDerivedPushforward (X.baseChangeFst T)) (adj : D.pullFst.functor ⊣ pushFst.functor) [D.pullFst.functor.Additive] (hH : PushforwardPreservesSourceComponents D A H pushFst) : ExternalProductHomReduction.PreservesSourceComponents D A (toHomReduction D A H pushFst adj)

The explicit pushforward-membership obligation is exactly the component preservation required by the resulting source-side Hom reduction.

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

Tensor duality, the pullback-pushforward adjunction, and preservation of the later source component prove semiorthogonality of the supplied external products.

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

Tensor duality, the pullback-pushforward adjunction, and preservation of the later source component imply semiorthogonality of the perfect base-change envelopes.