Testing bounded pullback orthogonality on the perfect envelope

The quasicoherent base-change component is the coproduct-and-extension closure of its perfect envelope. Thus vanishing of maps from perfect-envelope objects into a pulled-back bounded object extends to maps from the whole quasicoherent component. The fully faithful bounded-coherent inclusion then reflects the vanishing needed for the bounded right orthogonal.

The perfect-envelope vanishing is an explicit geometric hypothesis here. This file does not establish relative Hom base change or derive that hypothesis from pullback preservation of components.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPullback_rightOrthogonal_of_perfectEnvelope {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) (hPerfect : ∀ (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) : (DU.boundedComponent P).rightOrthogonal ≤ (DT.boundedComponent P).rightOrthogonal.inverseImage (pull.boundedFunctor hBounded)

Vanishing against the target perfect envelope suffices for bounded pullback to carry the source right orthogonal into the target right orthogonal. The vanishing premise is not supplied by component preservation alone.