Testing bounded pullback orthogonality on shifted external products

Vanishing of maps from every integer shift of each target external-product generator extends through the triangulated perfect envelope. The hypothesis is still geometric: no relative Hom base-change theorem or preservation of right orthogonals is inferred from component-image preservation.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.perfectEnvelope_hom_eq_zero_of_shiftedExternalProducts {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)) (hShifted : ∀ (Y : Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ U))), (DU.boundedComponent P).rightOrthogonal Y → ∀ (F : X.SourcePerfectPartCategory P) (G : T.CompactDqcFiber) (n : ℤ) (g : (CategoryTheory.shiftFunctor (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) n).obj (((DT.externalProduct P).obj F).obj G) ⟶ pull.functor.obj Y.obj), g = 0) (Y : Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ U))) : (DU.boundedComponent P).rightOrthogonal Y → ∀ (K : Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))), DT.perfectEnvelope P K → ∀ (g : K ⟶ pull.functor.obj Y.obj), g = 0

Vanishing for all shifts of the external-product generators implies vanishing for their whole target perfect envelope. The shifted hypothesis is essential for the triangulated-envelope step.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPullback_rightOrthogonal_of_shiftedExternalProducts {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)) (hBounded : pull.PreservesBoundedCoherent) (hShifted : ∀ (Y : Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ U))), (DU.boundedComponent P).rightOrthogonal Y → ∀ (F : X.SourcePerfectPartCategory P) (G : T.CompactDqcFiber) (n : ℤ) (g : (CategoryTheory.shiftFunctor (Dqc.SchemeQuasicoherentDerivedCategory (CategoryTheory.Over.left (X ⨯ T))) n).obj (((DT.externalProduct P).obj F).obj G) ⟶ pull.functor.obj Y.obj), g = 0) : (DU.boundedComponent P).rightOrthogonal ≤ (DT.boundedComponent P).rightOrthogonal.inverseImage (pull.boundedFunctor hBounded)

The shifted-generator test supplies the explicit perfect-envelope vanishing premise of boundedPullback_rightOrthogonal_of_perfectEnvelope.