Affine-base scalars on intrinsic bounded-coherent Dqc

A map Y ⟶ Spec A acts on module sheaves through global sections of Y. Restriction along R → A gives an R-linear structure on the intrinsic bounded-coherent Dqc category of Y. It is returned as a value, not installed as an instance: a category can carry several base-ring actions.

For a localization R → A, every localized denominator acts invertibly on every object. This uses no affineness of Y, object descent, or Hom localization.

@[reducible]

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.boundedCoherentLinearOfAffineMap {R A : Type u} [CommRing R] [CommRing A] (φ : R →+* A) {Y : Scheme} (p : Y ⟶ Spec (CommRingCat.of A)) : CategoryTheory.Linear R (SchemeBoundedCoherentDqcCategory Y)

The canonical R-action on bounded-coherent Dqc over an affine base, obtained from R → A → Γ(Y, 𝒪_Y). Use it with letI; it is not a global instance.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Dqc.boundedCoherentLinearOfAffineMap_smul {R A : Type u} [CommRing R] [CommRing A] (φ : R →+* A) {Y : Scheme} (p : Y ⟶ Spec (CommRingCat.of A)) {E F : SchemeBoundedCoherentDqcCategory Y} (r : R) (g : E ⟶ F) : r • g = (CommRingCat.Hom.hom (Scheme.Hom.appTop p)) ((CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of A)).inv) (φ r)) • g

The chosen R-action is multiplication by the pulled-back global section. This identifies the action rather than merely asserting its existence.

theorem AlgebraicGeometry.DerivedCategory.Dqc.isIso_smul_id_of_isLocalization {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (M : Submonoid R) [IsLocalization M A] {Y : Scheme} (p : Y ⟶ Spec (CommRingCat.of A)) (s : ↥M) (E : SchemeBoundedCoherentDqcCategory Y) : CategoryTheory.IsIso (↑s • CategoryTheory.CategoryStruct.id E)

A denominator of R → A acts by an isomorphism on any bounded-coherent Dqc object over any scheme Y → Spec A, including a non-affine Y.