Denominator scalars on relative bounded-coherent pullback

Let X be any scheme over Spec R, with no affineness requirement on X or its fibre product with Spec A. When A localizes R, a denominator acts invertibly on the target of a bounded-coherent derived pullback. The action is the explicit affine-base action on bounded-coherent Dqc, installed only in the theorem's scope. Bounded-coherent preservation remains an input.

This is the denominator-isomorphism premise of the categorical fixed-target arrow mechanism. It does not prove linearity of derived pullback, localization of Homs, coherent object descent, or arrow extension.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.affineAlgebraBaseChange {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] : SchemeBaseChange (Spec (CommRingCat.of R))

The scheme Spec A over Spec R for an R-algebra A. This is an abbreviation of the existing Over object, not a new base-change carrier.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.affineAlgebraBaseChange = CategoryTheory.Over.mk (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R A)))

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.boundedFunctor_isIso_smul_denominator {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (M : Submonoid R) [IsLocalization M A] (X : SchemeBaseChange (Spec (CommRingCat.of R))) (pull : DqcLeftDerivedPullback (X.baseChangeMap affineAlgebraBaseChange.toIdentityBaseChange)) (hBounded : pull.PreservesBoundedCoherent) (s : ↥M) (E : Dqc.SchemeBoundedCoherentDqcCategory (CategoryTheory.Over.left (X ⨯ identityBaseChange (Spec (CommRingCat.of R))))) : CategoryTheory.IsIso (↑s • CategoryTheory.CategoryStruct.id ((pull.boundedFunctor hBounded).obj E))

Localized denominators act invertibly on the image of relative bounded-coherent pullback. The total space X ×_Spec R Spec A may be non-affine. The scalar action is the one induced by the second projection to Spec A, not an arbitrary R-module instance.