Conditional fixed-target arrow extension on bounded base-change components

The existing bounded pullback supplies an inclusion comparison, but not a comparison with chosen right projectors. The first theorem retains a supplied projector comparison and counit equation. Under triangulatedness and explicit preservation of the right orthogonal, the later theorems construct both from the canonical adjunction mate and apply the categorical transfer theorem.

It does not prove that geometric pullback preserves the right orthogonal, that ambient bounded-coherent arrows descend, or any Noetherianity assertion.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPullback_fixedTargetArrowExtension_of_ambient {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)) (hDqc : DT.PullbackPreservesQuasicoherentComponent DU P pull) (hBounded : pull.PreservesBoundedCoherent) (pU : (DU.boundedComponent P).RightProjectionData) (pT : (DT.boundedComponent P).RightProjectionData) (projectorIso : (pull.boundedFunctor hBounded).comp pT.projection ≅ pU.projection.comp (DT.boundedPullback DU P pull hDqc hBounded)) (counit_compat : ∀ (Y : Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ U))), pT.counitApp ((pull.boundedFunctor hBounded).obj Y) = CategoryTheory.CategoryStruct.comp ((DT.boundedComponent P).ι.map (projectorIso.app Y).hom) (CategoryTheory.CategoryStruct.comp ((DT.boundedPullbackCompInclusion DU P pull hDqc hBounded).app (pU.project Y)).hom ((pull.boundedFunctor hBounded).map (pU.counitApp Y)))) (E : DU.BoundedCategory P) (hExt : CategoryTheory.Subobject.FixedTargetArrowExtension (pull.boundedFunctor hBounded) ((DU.boundedComponent P).ι.obj E)) : CategoryTheory.Subobject.FixedTargetArrowExtension (DT.boundedPullback DU P pull hDqc hBounded) E

An ambient bounded-coherent arrow lift transfers to the bounded base-change component when pullback commutes, as a mate, with the chosen right projectors. Both the ambient lift and this commutation are inputs.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPullbackProjectionMateIso {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)) (hDqc : DT.PullbackPreservesQuasicoherentComponent DU P pull) (hBounded : pull.PreservesBoundedCoherent) (pU : (DU.boundedComponent P).RightProjectionData) (pT : (DT.boundedComponent P).RightProjectionData) [(Dqc.schemeBoundedCoherentCohomology (CategoryTheory.Over.left (X ⨯ U))).IsTriangulated] [(Dqc.schemeBoundedCoherentCohomology (CategoryTheory.Over.left (X ⨯ T))).IsTriangulated] [(pull.boundedFunctor hBounded).CommShift ℤ] [(pull.boundedFunctor hBounded).IsTriangulated] (hU : (DU.boundedComponent P).IsTriangulated) (hT : (DT.boundedComponent P).IsTriangulated) (horth : (DU.boundedComponent P).rightOrthogonal ≤ (DT.boundedComponent P).rightOrthogonal.inverseImage (pull.boundedFunctor hBounded)) : (pull.boundedFunctor hBounded).comp pT.projection ≅ pU.projection.comp (DT.boundedPullback DU P pull hDqc hBounded)

Relative bounded pullback commutes with the chosen component projections when it carries the source right orthogonal into the target right orthogonal. This constructs the comparison as an adjunction mate, rather than requiring the comparison as input.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPullbackProjectionMateIso_counit {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)) (hDqc : DT.PullbackPreservesQuasicoherentComponent DU P pull) (hBounded : pull.PreservesBoundedCoherent) (pU : (DU.boundedComponent P).RightProjectionData) (pT : (DT.boundedComponent P).RightProjectionData) [(Dqc.schemeBoundedCoherentCohomology (CategoryTheory.Over.left (X ⨯ U))).IsTriangulated] [(Dqc.schemeBoundedCoherentCohomology (CategoryTheory.Over.left (X ⨯ T))).IsTriangulated] [(pull.boundedFunctor hBounded).CommShift ℤ] [(pull.boundedFunctor hBounded).IsTriangulated] (hU : (DU.boundedComponent P).IsTriangulated) (hT : (DT.boundedComponent P).IsTriangulated) (horth : (DU.boundedComponent P).rightOrthogonal ≤ (DT.boundedComponent P).rightOrthogonal.inverseImage (pull.boundedFunctor hBounded)) (Y : Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ U))) : pT.counitApp ((pull.boundedFunctor hBounded).obj Y) = CategoryTheory.CategoryStruct.comp ((DT.boundedComponent P).ι.map ((DT.boundedPullbackProjectionMateIso DU P pull hDqc hBounded pU pT hU hT horth).app Y).hom) (CategoryTheory.CategoryStruct.comp ((DT.boundedPullbackCompInclusion DU P pull hDqc hBounded).app (pU.project Y)).hom ((pull.boundedFunctor hBounded).map (pU.counitApp Y)))

The bounded-pullback projector comparison is the mate of the canonical component-inclusion comparison, with its counit compatibility explicit.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.DerivedBaseChangeData.boundedPullback_fixedTargetArrowExtension_of_orthogonalPreservation {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)) (hDqc : DT.PullbackPreservesQuasicoherentComponent DU P pull) (hBounded : pull.PreservesBoundedCoherent) (pU : (DU.boundedComponent P).RightProjectionData) (pT : (DT.boundedComponent P).RightProjectionData) [(Dqc.schemeBoundedCoherentCohomology (CategoryTheory.Over.left (X ⨯ U))).IsTriangulated] [(Dqc.schemeBoundedCoherentCohomology (CategoryTheory.Over.left (X ⨯ T))).IsTriangulated] [(pull.boundedFunctor hBounded).CommShift ℤ] [(pull.boundedFunctor hBounded).IsTriangulated] (hU : (DU.boundedComponent P).IsTriangulated) (hT : (DT.boundedComponent P).IsTriangulated) (horth : (DU.boundedComponent P).rightOrthogonal ≤ (DT.boundedComponent P).rightOrthogonal.inverseImage (pull.boundedFunctor hBounded)) (E : DU.BoundedCategory P) (hExt : CategoryTheory.Subobject.FixedTargetArrowExtension (pull.boundedFunctor hBounded) ((DU.boundedComponent P).ι.obj E)) : CategoryTheory.Subobject.FixedTargetArrowExtension (DT.boundedPullback DU P pull hDqc hBounded) E

Orthogonal preservation and an ambient fixed-target arrow lift suffice for a fixed-target arrow lift on the actual bounded base-change component. Neither projector commutation nor its counit equation is assumed.