Linearity of relative bounded-coherent pullback under affine localization

For any scheme over Spec R, including a non-affine one, pullback along the base-change map to Spec A is R-linear for the explicit affine-base actions when A is a localization of R. The proof uses the cartesian square to identify the two global-section scalars, proves linearity of module-sheaf pullback via its adjunction, then transports this through exact derived pullback and the quasi-coherent and bounded-coherent full subcategories.

The supplied derived pullback must preserve the bounded-coherent locus. This does not establish localized Hom sets, object descent, fixed-target arrow extension, or an arbitrary non-flat base-change theorem.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.boundedFunctor_linearOfLocalization {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (M : Submonoid R) [IsLocalization M A] (X : SchemeBaseChange (Spec (CommRingCat.of R))) (P : DqcLeftDerivedPullback (X.baseChangeMap affineAlgebraBaseChange.toIdentityBaseChange)) (h : P.PreservesBoundedCoherent) : let T := affineAlgebraBaseChange; have pSource := CategoryTheory.Over.Hom.left (X.baseChangeSnd (identityBaseChange (Spec (CommRingCat.of R)))); have pTarget := CategoryTheory.Over.Hom.left (X.baseChangeSnd T); CategoryTheory.Functor.Linear R (P.boundedFunctor h)

Relative bounded-coherent derived pullback is linear for the two affine-base actions when the base is localized and pullback preserves the bounded-coherent locus.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.boundedFunctor_additiveOfLocalization {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (M : Submonoid R) [IsLocalization M A] (X : SchemeBaseChange (Spec (CommRingCat.of R))) (P : DqcLeftDerivedPullback (X.baseChangeMap affineAlgebraBaseChange.toIdentityBaseChange)) (h : P.PreservesBoundedCoherent) : (P.boundedFunctor h).Additive

Relative bounded-coherent pullback along an affine localization is additive. Together with boundedFunctor_linearOfLocalization, this makes its actual action on Hom groups available as Functor.mapLinearMap for the affine-base scalar actions. This does not assert that those Hom maps are localizations.