The affine quasi-coherent derived category

On an affine scheme, Mathlib proves that quasi-coherent module sheaves are equivalent to modules over the coordinate ring. This file uses that theorem to put the genuine full category of quasi-coherent sheaves on Spec R in the abelian setting and then forms its derived category.

This is a concrete prerequisite for the general Dqc realization. It does not identify this derived category with the quasi-coherent-cohomology locus in the derived category of all sheaves: that unbounded derived essential surjectivity theorem is not currently available in Mathlib.

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Dqc.AffineQuasicoherentSheaves (R : CommRingCat) : Type (u + 1)

The actual category of quasi-coherent module sheaves on Spec R.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.AffineQuasicoherentSheaves R = (SheafOfModules.isQuasicoherent (AlgebraicGeometry.Spec R).ringCatSheaf).FullSubcategory

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesHasFiniteProducts (R : CommRingCat) : CategoryTheory.Limits.HasFiniteProducts (AffineQuasicoherentSheaves R)

Finite products on affine quasi-coherent sheaves are transported across the tilde equivalence, rather than postulated on the full subcategory.

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesAbelian (R : CommRingCat) : CategoryTheory.Abelian (AffineQuasicoherentSheaves R)

On an affine scheme, quasi-coherent sheaves form an abelian category by the proved tilde equivalence with modules over the coordinate ring.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesAbelian R = CategoryTheory.abelianOfEquivalence AlgebraicGeometry.tildeEquiv.inverse

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesHasExactCoproducts (R : CommRingCat) (ι : Type u) : CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete ι) (AffineQuasicoherentSheaves R)

Affine quasi-coherent sheaves satisfy AB4 at each indexing type: ι-indexed coproducts are exact.

The coproducts themselves are not transported — they are the ambient ones, created by the inclusion into (Spec R).Modules (quasicoherentSheavesInclusion_createsCoproductsOfShape, arbitrary scheme, no hypotheses). Exactness is what the tilde equivalence supplies, from AB4 (ModuleCat R), and it is affine-only: on a general scheme the quasi-coherent subcategory is not abelian, so there is no AB4 statement there to prove or to assume.

This is the missing abelian-side input to coproducts in the affine quasi-coherent derived category: DerivedCategory.hasCoproductsOfShape asks for HasExactColimitsOfShape (Discrete ι), not merely for the coproducts.

@[reducible, inline]

abbrev AlgebraicGeometry.DerivedCategory.Dqc.AffineQuasicoherentDerivedCategory (R : CommRingCat) : Type (u + 1)

The derived category of the genuine abelian category of quasi-coherent sheaves on an affine scheme.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.AffineQuasicoherentDerivedCategory R = DerivedCategory (AlgebraicGeometry.DerivedCategory.Dqc.AffineQuasicoherentSheaves R)

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedCategory_isTriangulated (R : CommRingCat) : CategoryTheory.IsTriangulated (AffineQuasicoherentDerivedCategory R)

The affine quasi-coherent derived category is genuinely triangulated.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesEquiv (R : CommRingCat) : ModuleCat ↑R ≌ AffineQuasicoherentSheaves R

The tilde equivalence is the concrete affine realization of quasi-coherent sheaves; no all-sheaf category occurs in this equivalence.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesEquiv R = AlgebraicGeometry.tildeEquiv

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesEquiv_functor_additive (R : CommRingCat) : (affineQuasicoherentSheavesEquiv R).functor.Additive

instance AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesEquiv_inverse_additive (R : CommRingCat) : (affineQuasicoherentSheavesEquiv R).inverse.Additive

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineTildeDerivedFunctor (R : CommRingCat) : CategoryTheory.Functor (DerivedCategory (ModuleCat ↑R)) (AffineQuasicoherentDerivedCategory R)

The derived tilde functor from complexes of coordinate-ring modules to the derived category of genuine quasi-coherent sheaves.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineTildeDerivedFunctor R = (AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesEquiv R).functor.mapDerivedCategory

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineGammaDerivedFunctor (R : CommRingCat) : CategoryTheory.Functor (AffineQuasicoherentDerivedCategory R) (DerivedCategory (ModuleCat ↑R))

The derived global-sections functor in the opposite direction. The quasi-inverse theorem is proved in Dqc.AffineDerivedEquivalence.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineGammaDerivedFunctor R = (AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesEquiv R).inverse.mapDerivedCategory

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineTildeDerivedHomologyIso (R : CommRingCat) (E : DerivedCategory (ModuleCat ↑R)) (n : ℤ) : (DerivedCategory.homologyFunctor (AffineQuasicoherentSheaves R) n).obj ((affineTildeDerivedFunctor R).obj E) ≅ (affineQuasicoherentSheavesEquiv R).functor.obj ((DerivedCategory.homologyFunctor (ModuleCat ↑R) n).obj E)

Derived tilde commutes with every canonical cohomology functor.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineGammaDerivedHomologyIso (R : CommRingCat) (E : AffineQuasicoherentDerivedCategory R) (n : ℤ) : (DerivedCategory.homologyFunctor (ModuleCat ↑R) n).obj ((affineGammaDerivedFunctor R).obj E) ≅ (affineQuasicoherentSheavesEquiv R).inverse.obj ((DerivedCategory.homologyFunctor (AffineQuasicoherentSheaves R) n).obj E)

Derived global sections commutes with every canonical cohomology functor.

Equations

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