Documentation

DerivedAlgGeo.AlgebraicGeometry.DerivedCategory.Dqc.AffineDerivedEquivalence

The affine quasi-coherent derived equivalence #

The affine tilde equivalence is exact, so its functor and inverse preserve quasi-isomorphisms of cochain complexes. The resulting functors on derived categories are quasi-inverse. This identifies the genuine derived category of quasi-coherent sheaves on Spec R with the derived category of R-modules.

source
noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedEquivalence (R : CommRingCat) :
DerivedCategory (ModuleCat ↑R) ≌ AffineQuasicoherentDerivedCategory R

The derived tilde functor is an equivalence between the derived category of coordinate-ring modules and the genuine derived category of quasi-coherent sheaves on the affine spectrum.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedEquivalence_functor (R : CommRingCat) :
    (affineQuasicoherentDerivedEquivalence R).functor = affineTildeDerivedFunctor R
    source
    @[simp]
    theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedEquivalence_inverse (R : CommRingCat) :
    (affineQuasicoherentDerivedEquivalence R).inverse = affineGammaDerivedFunctor R
    source
    @[reducible, inline]
    abbrev AlgebraicGeometry.DerivedCategory.Dqc.AffineQuasicoherentBoundedDerivedCategory (R : CommRingCat) :
    Type (u + 1)

    The cohomologically bounded derived category of genuine quasi-coherent sheaves on an affine spectrum.

    Equations
    Instances For
      source
      theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedEquivalence_bounded_inverseImage (R : CommRingCat) :
      DerivedCategory.TStructure.t.bounded.inverseImage (affineQuasicoherentDerivedEquivalence R).functor = DerivedCategory.TStructure.t.bounded

      The affine derived tilde equivalence detects cohomological boundedness. Both directions follow from exactness of the abelian tilde equivalence.

      source
      noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedEquivalence (R : CommRingCat) :
      DerivedCategory.Bounded (ModuleCat ↑R) ≌ AffineQuasicoherentBoundedDerivedCategory R

      The affine quasi-coherent derived equivalence restricted to cohomologically bounded objects.

      Equations
      Instances For