Realizing the affine quasi-coherent derived category inside Dqc

On an affine spectrum, ambient kernels and cokernels of quasi-coherent module sheaves are again quasi-coherent. Hence the inclusion of quasi-coherent sheaves into all module sheaves is exact. Passing to derived categories and using exactness to identify cohomology gives a concrete functor from the derived category of affine quasi-coherent sheaves into the honest quasi-coherent-cohomology locus Dqc(Spec R).

This does not claim that the resulting functor is essentially surjective on the unbounded Dqc locus. That general affine realization theorem requires additional unbounded derived-category input.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherent_kernel {R : CommRingCat} {M N : (Spec R).Modules} (g : M ⟶ N) (hM : SheafOfModules.IsQuasicoherent M) (hN : SheafOfModules.IsQuasicoherent N) : SheafOfModules.IsQuasicoherent (CategoryTheory.Limits.kernel g)

On an affine spectrum, an ambient kernel of a morphism between quasi-coherent module sheaves is quasi-coherent.

The proof moved to CoherentSheaf/Quasicoherent/Kernels.lean when #720 needed it for an arbitrary scheme; this name survives as the moduli lane's entry point.

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherent_isClosedUnderKernels (R : CommRingCat) : (AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentProperty✝ R).IsClosedUnderKernels

Quasi-coherent module sheaves on an affine spectrum are closed under ambient kernels.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherent_cokernel {R : CommRingCat} {M N : (Spec R).Modules} (g : M ⟶ N) (hM : SheafOfModules.IsQuasicoherent M) (hN : SheafOfModules.IsQuasicoherent N) : SheafOfModules.IsQuasicoherent (CategoryTheory.Limits.cokernel g)

On an affine spectrum, an ambient cokernel of a morphism between quasi-coherent module sheaves is quasi-coherent.

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherent_isClosedUnderCokernels (R : CommRingCat) : (AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentProperty✝ R).IsClosedUnderCokernels

Quasi-coherent module sheaves on an affine spectrum are closed under ambient cokernels.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesInclusion (R : CommRingCat) : CategoryTheory.Functor (AffineQuasicoherentSheaves R) (Spec R).Modules

The inclusion of affine quasi-coherent sheaves into all module sheaves.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesInclusion R = (AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentProperty✝ R).ι

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesInclusion_additive (R : CommRingCat) : (affineQuasicoherentSheavesInclusion R).Additive

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesInclusion_preservesKernel (R : CommRingCat) {M N : AffineQuasicoherentSheaves R} (g : M ⟶ N) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair g 0) (affineQuasicoherentSheavesInclusion R)

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesInclusion_preservesCokernel (R : CommRingCat) {M N : AffineQuasicoherentSheaves R} (g : M ⟶ N) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair g 0) (affineQuasicoherentSheavesInclusion R)

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesInclusion_preservesFiniteLimits (R : CommRingCat) : CategoryTheory.Limits.PreservesFiniteLimits (affineQuasicoherentSheavesInclusion R)

The affine quasi-coherent inclusion preserves all finite limits.

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesInclusion_preservesFiniteColimits (R : CommRingCat) : CategoryTheory.Limits.PreservesFiniteColimits (affineQuasicoherentSheavesInclusion R)

The affine quasi-coherent inclusion preserves all finite colimits.

instance AlgebraicGeometry.DerivedCategory.Dqc.affineTilde_preservesFiniteLimits (R : CommRingCat) : CategoryTheory.Limits.PreservesFiniteLimits (tilde.functor R)

Exactness of tilde follows from its factorization through the affine quasi-coherent equivalence and the exact inclusion.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedInclusion (R : CommRingCat) : CategoryTheory.Functor (AffineQuasicoherentDerivedCategory R) (SchemeDerivedCategory (Spec R))

The exact inclusion of affine quasi-coherent sheaves induces a functor into the ambient derived category of all module sheaves.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedInclusion R = (AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesInclusion R).mapDerivedCategory

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedInclusion_mem_dqc (R : CommRingCat) (E : AffineQuasicoherentDerivedCategory R) : schemeQuasicoherentCohomology (Spec R) ((affineQuasicoherentDerivedInclusion R).obj E)

Every object in the image of the affine derived inclusion has quasi-coherent cohomology.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedToDqc (R : CommRingCat) : CategoryTheory.Functor (AffineQuasicoherentDerivedCategory R) (SchemeQuasicoherentDerivedCategory (Spec R))

The genuine affine quasi-coherent derived category maps concretely into the honest quasi-coherent-cohomology locus Dqc(Spec R).

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedToDqcCompInclusion (R : CommRingCat) : (affineQuasicoherentDerivedToDqc R).comp (SchemeQuasicoherentDerivedCategory.ι (Spec R)) ≅ affineQuasicoherentDerivedInclusion R

Forgetting the quasi-coherent-cohomology proof recovers the exact affine derived inclusion.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedToDqc_bounded (R : CommRingCat) (E : AffineQuasicoherentBoundedDerivedCategory R) : schemeBoundedQuasicoherent (Spec R) ((affineQuasicoherentDerivedToDqc R).obj E.obj)

Affine realization carries cohomologically bounded quasi-coherent complexes to the intrinsic bounded locus in Dqc.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedToDqc (R : CommRingCat) : CategoryTheory.Functor (AffineQuasicoherentBoundedDerivedCategory R) (SchemeBoundedQuasicoherentDerivedCategory (Spec R))

The bounded affine quasi-coherent derived category maps concretely into the intrinsic bounded Dqc locus.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedToDqcCompInclusion (R : CommRingCat) : (affineQuasicoherentBoundedDerivedToDqc R).comp (SchemeBoundedQuasicoherentDerivedCategory.ι (Spec R)) ≅ DerivedCategory.Bounded.ι.comp (affineQuasicoherentDerivedToDqc R)

Forgetting boundedness recovers affine realization into Dqc.

Equations

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