Pullback on affine quasi-coherent sheaves

For a ring map R → S, extension of scalars transports through the affine equivalences to a functor from quasi-coherent sheaves on Spec R to those on Spec S. Its adjunction with the geometric affine pushforward identifies this transported functor by the expected geometric universal property.

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

Affine quasi-coherent pullback, constructed by transporting extension of scalars through the affine equivalences.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesPullbackPushforwardAdjunction {R S : CommRingCat} (f : R ⟶ S) : affineQuasicoherentSheavesPullback f ⊣ affineQuasicoherentSheavesPushforward f

Transported extension of scalars is left adjoint to geometric affine quasi-coherent pushforward.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesPullbackGammaIso {R S : CommRingCat} (f : R ⟶ S) : (affineQuasicoherentSheavesPullback f).comp (affineQuasicoherentSheavesEquiv S).inverse ≅ (affineQuasicoherentSheavesEquiv R).inverse.comp (ModuleCat.extendScalars (CommRingCat.Hom.hom f))

Affine global sections identify quasi-coherent pullback with extension of scalars.

Equations

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

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

Affine quasi-coherent pullback is additive.

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

Affine quasi-coherent pullback preserves finite colimits.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesPullback_preservesFiniteLimits {R S : CommRingCat} (f : R ⟶ S) (hf : (CommRingCat.Hom.hom f).Flat) : CategoryTheory.Limits.PreservesFiniteLimits (affineQuasicoherentSheavesPullback f)

Affine quasi-coherent pullback preserves finite limits when the ring map is flat.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedPullback {R S : CommRingCat} (f : R ⟶ S) (hf : (CommRingCat.Hom.hom f).Flat) : CategoryTheory.Functor (AffineQuasicoherentDerivedCategory R) (AffineQuasicoherentDerivedCategory S)

Exact affine quasi-coherent derived pullback along a flat ring map.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedPullback f hf = (AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesPullback f).mapDerivedCategory

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineExtendScalarsDerived {R S : CommRingCat} (f : R ⟶ S) (hf : (CommRingCat.Hom.hom f).Flat) : CategoryTheory.Functor (DerivedCategory (ModuleCat ↑R)) (DerivedCategory (ModuleCat ↑S))

Derived extension of scalars along a flat map, with exactness packaged in the construction.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineExtendScalarsDerived f hf = (ModuleCat.extendScalars (CommRingCat.Hom.hom f)).mapDerivedCategory

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineSchemeModuleExactDerivedPullbackComparison {R S : CommRingCat} (f : R ⟶ S) [CategoryTheory.Limits.PreservesFiniteLimits (ModuleCat.extendScalars (CommRingCat.Hom.hom f))] [CategoryTheory.Limits.PreservesFiniteLimits (Scheme.Modules.pullback (Spec.map f))] : (tilde.functor R).mapDerivedCategory.comp (Scheme.Modules.pullback (Spec.map f)).mapDerivedCategory ≅ (ModuleCat.extendScalars (CommRingCat.Hom.hom f)).mapDerivedCategory.comp (tilde.functor S).mapDerivedCategory

For exact affine pullback, derived sheafification commutes with extension of scalars on the derived categories of all module sheaves. Both exactness hypotheses are explicit; no quasi-coherent or bounded-coherent restriction is asserted here.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedPullbackGammaIso {R S : CommRingCat} (f : R ⟶ S) (hf : (CommRingCat.Hom.hom f).Flat) : (affineQuasicoherentDerivedPullback f hf).comp (affineGammaDerivedFunctor S) ≅ (affineGammaDerivedFunctor R).comp (affineExtendScalarsDerived f hf)

On derived categories, affine global sections identify exact pullback with derived extension of scalars.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedPullbackComparison {R S : CommRingCat} (f : R ⟶ S) (hf : (CommRingCat.Hom.hom f).Flat) : affineQuasicoherentDerivedPullback f hf ≅ CategoryTheory.Pseudofunctor.equivalenceTransportFunctor (affineQuasicoherentDerivedEquivalence R) (affineQuasicoherentDerivedEquivalence S) (affineExtendScalarsDerived f hf)

Exact affine derived pullback is extension of scalars transported through the affine derived equivalences.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedPullbackPushforwardAdjunction {R S : CommRingCat} (f : R ⟶ S) (hf : (CommRingCat.Hom.hom f).Flat) : affineQuasicoherentDerivedPullback f hf ⊣ affineQuasicoherentDerivedPushforward f

Exact affine derived pullback is left adjoint to exact affine derived pushforward.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedPullbackToDqc {R S : CommRingCat} (f : R ⟶ S) (hf : (CommRingCat.Hom.hom f).Flat) : CategoryTheory.Functor (AffineQuasicoherentDerivedCategory R) (SchemeQuasicoherentDerivedCategory (Spec S))

Exact affine pullback followed by the concrete realization into the target scheme's intrinsic Dqc category.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedPullbackToDqcCompInclusion {R S : CommRingCat} (f : R ⟶ S) (hf : (CommRingCat.Hom.hom f).Flat) : (affineQuasicoherentDerivedPullbackToDqc f hf).comp (SchemeQuasicoherentDerivedCategory.ι (Spec S)) ≅ (affineQuasicoherentDerivedPullback f hf).comp (affineQuasicoherentDerivedInclusion S)

Forgetting the target Dqc witness identifies realized affine pullback with pullback followed by the exact inclusion into all module sheaves.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedPullback_bounded {R S : CommRingCat} (f : R ⟶ S) (hf : (CommRingCat.Hom.hom f).Flat) (E : AffineQuasicoherentDerivedCategory R) (hE : DerivedCategory.TStructure.t.bounded E) : DerivedCategory.TStructure.t.bounded ((affineQuasicoherentDerivedPullback f hf).obj E)

Flat affine quasi-coherent derived pullback preserves cohomologically bounded objects.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedPullback {R S : CommRingCat} (f : R ⟶ S) (hf : (CommRingCat.Hom.hom f).Flat) : CategoryTheory.Functor (AffineQuasicoherentBoundedDerivedCategory R) (AffineQuasicoherentBoundedDerivedCategory S)

Flat affine quasi-coherent derived pullback restricted to bounded objects.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedPullbackCompInclusion {R S : CommRingCat} (f : R ⟶ S) (hf : (CommRingCat.Hom.hom f).Flat) : (affineQuasicoherentBoundedDerivedPullback f hf).comp DerivedCategory.Bounded.ι ≅ DerivedCategory.Bounded.ι.comp (affineQuasicoherentDerivedPullback f hf)

Forgetting boundedness recovers flat affine quasi-coherent derived pullback.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedPullbackPushforwardAdjunction {R S : CommRingCat} (f : R ⟶ S) (hf : (CommRingCat.Hom.hom f).Flat) : affineQuasicoherentBoundedDerivedPullback f hf ⊣ affineQuasicoherentBoundedDerivedPushforward f

The exact affine derived pullback--pushforward adjunction restricts to cohomologically bounded objects.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedPullbackToDqc {R S : CommRingCat} (f : R ⟶ S) (hf : (CommRingCat.Hom.hom f).Flat) : CategoryTheory.Functor (AffineQuasicoherentBoundedDerivedCategory R) (SchemeBoundedQuasicoherentDerivedCategory (Spec S))

Bounded exact affine pullback followed by the concrete realization into the target scheme's intrinsic bounded Dqc category.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedPullbackToDqcCompInclusion {R S : CommRingCat} (f : R ⟶ S) (hf : (CommRingCat.Hom.hom f).Flat) : (affineQuasicoherentBoundedDerivedPullbackToDqc f hf).comp (SchemeBoundedQuasicoherentDerivedCategory.ι (Spec S)) ≅ DerivedCategory.Bounded.ι.comp (affineQuasicoherentDerivedPullbackToDqc f hf)

Forgetting intrinsic boundedness recovers realized unbounded affine pullback on the bounded source.

Equations

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