Shift compatibility for exact derived pullback coherence

The localization factors, complex-level unit and compositor, and their localized forms commute with the integer shift. Consequently the unit and compositor of exact derived pullback commute with shift as well.

The compositor proof treats the two parenthesizations of a composite explicitly: the corresponding CategoryTheory.Functor.CommShift structures are not definitionally the same, even though the underlying composite functors are. Naturality of the final pullback's shift isomorphism bridges that distinction before localization extensionality completes the proof.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullbackFactors_commShift {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback f] : CategoryTheory.NatTrans.CommShift (derivedPullbackFactors f).hom ℤ

The localization comparison for exact derived pullback commutes with shift.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPullbackId_commShift {S : Scheme} (T : SchemeBaseChange S) : CategoryTheory.NatTrans.CommShift T.complexPullbackId.hom ℤ

The complex-level identity pullback isomorphism commutes with shift.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPullbackComp_commShift {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) : CategoryTheory.NatTrans.CommShift (complexPullbackComp f g).hom ℤ

The complex-level pullback compositor commutes with shift.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPullbackIdLocalized_commShift {S : Scheme} (T : SchemeBaseChange S) : CategoryTheory.NatTrans.CommShift T.complexPullbackIdLocalized.hom ℤ

The localized complex-level identity isomorphism commutes with shift.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.complexPullbackCompLocalized_commShift {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) [IsExactPullback f] : CategoryTheory.NatTrans.CommShift (complexPullbackCompLocalized f g).hom ℤ

The localized complex-level pullback compositor commutes with shift.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullbackId_commShift {S : Scheme} (T : SchemeBaseChange S) : CategoryTheory.NatTrans.CommShift T.derivedPullbackId.hom ℤ

The unit isomorphism for exact derived pullback commutes with shift.

instance AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullbackComp_commShift {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) [IsExactPullback f] [IsExactPullback g] : CategoryTheory.NatTrans.CommShift (derivedPullbackComp f g).hom ℤ

The compositor isomorphism for exact derived pullback commutes with shift.