Pushforward on affine quasi-coherent derived categories

For a ring map R → S, module-sheaf pushforward along Spec S → Spec R preserves quasi-coherence. Restricted to the genuine abelian categories of quasi-coherent sheaves, it is exact: left exactness comes from ordinary pushforward, while right exactness follows from affine pushforward preserving epimorphisms between quasi-coherent sheaves. It therefore induces an exact functor on derived categories.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesInclusion_full (R : CommRingCat) : (affineQuasicoherentSheavesInclusion R).Full

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesInclusion_faithful (R : CommRingCat) : (affineQuasicoherentSheavesInclusion R).Faithful

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesPushforward {R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.Functor (AffineQuasicoherentSheaves S) (AffineQuasicoherentSheaves R)

Module-sheaf pushforward along a morphism of affine spectra, restricted to genuine quasi-coherent sheaves.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesPushforwardCompInclusion {R S : CommRingCat} (f : R ⟶ S) : (affineQuasicoherentSheavesPushforward f).comp (affineQuasicoherentSheavesInclusion R) ≅ (affineQuasicoherentSheavesInclusion S).comp (Scheme.Modules.pushforward (Spec.map f))

Forgetting quasi-coherence recovers ordinary module-sheaf pushforward.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesPushforwardGammaIso {R S : CommRingCat} (f : R ⟶ S) : (affineQuasicoherentSheavesPushforward f).comp (affineQuasicoherentSheavesEquiv R).inverse ≅ (affineQuasicoherentSheavesEquiv S).inverse.comp (ModuleCat.restrictScalars (CommRingCat.Hom.hom f))

Affine global sections identify quasi-coherent pushforward with restriction of scalars.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesPushforwardComparison {R S : CommRingCat} (f : R ⟶ S) : affineQuasicoherentSheavesPushforward f ≅ CategoryTheory.Pseudofunctor.equivalenceTransportFunctor (affineQuasicoherentSheavesEquiv S) (affineQuasicoherentSheavesEquiv R) (ModuleCat.restrictScalars (CommRingCat.Hom.hom f))

Geometric affine quasi-coherent pushforward is restriction of scalars transported through the affine equivalences.

Equations

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

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesPushforward_preservesFiniteLimits {R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.Limits.PreservesFiniteLimits (affineQuasicoherentSheavesPushforward f)

Affine quasi-coherent pushforward preserves finite limits.

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesPushforward_additive {R S : CommRingCat} (f : R ⟶ S) : (affineQuasicoherentSheavesPushforward f).Additive

Affine quasi-coherent pushforward is additive.

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesPushforward_preservesEpimorphisms {R S : CommRingCat} (f : R ⟶ S) : (affineQuasicoherentSheavesPushforward f).PreservesEpimorphisms

Affine quasi-coherent pushforward preserves epimorphisms.

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesPushforward_preservesFiniteColimits {R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.Limits.PreservesFiniteColimits (affineQuasicoherentSheavesPushforward f)

Affine quasi-coherent pushforward preserves finite colimits.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedPushforward {R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.Functor (AffineQuasicoherentDerivedCategory S) (AffineQuasicoherentDerivedCategory R)

Exact pushforward on affine quasi-coherent derived categories.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedPushforward f = (AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesPushforward f).mapDerivedCategory

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedPushforward_bounded {R S : CommRingCat} (f : R ⟶ S) (E : AffineQuasicoherentDerivedCategory S) (hE : DerivedCategory.TStructure.t.bounded E) : DerivedCategory.TStructure.t.bounded ((affineQuasicoherentDerivedPushforward f).obj E)

Affine quasi-coherent derived pushforward preserves cohomologically bounded objects.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedPushforward {R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.Functor (AffineQuasicoherentBoundedDerivedCategory S) (AffineQuasicoherentBoundedDerivedCategory R)

Geometric affine derived pushforward restricted to cohomologically bounded quasi-coherent complexes.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedPushforwardCompInclusion {R S : CommRingCat} (f : R ⟶ S) : (affineQuasicoherentBoundedDerivedPushforward f).comp DerivedCategory.Bounded.ι ≅ DerivedCategory.Bounded.ι.comp (affineQuasicoherentDerivedPushforward f)

Forgetting boundedness recovers geometric affine derived pushforward.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedPushforwardGammaIso {R S : CommRingCat} (f : R ⟶ S) : (affineQuasicoherentDerivedPushforward f).comp (affineGammaDerivedFunctor R) ≅ (affineGammaDerivedFunctor S).comp (ModuleCat.restrictScalars (CommRingCat.Hom.hom f)).mapDerivedCategory

On derived categories, affine global sections identify geometric pushforward with derived restriction of scalars.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedPushforwardComparison {R S : CommRingCat} (f : R ⟶ S) : affineQuasicoherentDerivedPushforward f ≅ CategoryTheory.Pseudofunctor.equivalenceTransportFunctor (affineQuasicoherentDerivedEquivalence S) (affineQuasicoherentDerivedEquivalence R) (ModuleCat.restrictScalars (CommRingCat.Hom.hom f)).mapDerivedCategory

Geometric affine derived pushforward is the transport of derived restriction of scalars through the affine derived equivalences.

Equations

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