The bounded affine quasi-coherent identification

This file proves the affine comparison between the derived category of quasi-coherent sheaves and the intrinsic bounded Dqc locus. The first ingredient is an arbitrary-rank free-generator package for AffineQuasicoherentSheaves R.

The unbounded equivalence remains a separate problem: the bounded cone argument used below requires finite cohomological amplitude.

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.affineQuasicoherentFree (R : CommRingCat) (I : Type u) : AffineQuasicoherentSheaves R

The arbitrary-rank free object in affine quasi-coherent sheaves, transported from the usual free module through the tilde equivalence.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentFree R I = (AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentSheavesEquiv R).functor.obj ((ModuleCat.free ↑R).obj I)

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentFree_projective (R : CommRingCat) (I : Type u) : CategoryTheory.Projective (affineQuasicoherentFree R I)

Arbitrary-rank affine quasi-coherent free sheaves are projective.

def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentFreeObjects (R : CommRingCat) : CategoryTheory.ObjectProperty (AffineQuasicoherentSheaves R)

The class of arbitrary-rank free affine quasi-coherent sheaves.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentFreeObjects R P = ∃ (I : Type ?u.1), P = AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentFree R I

theorem AlgebraicGeometry.DerivedCategory.Dqc.exists_affineQuasicoherentFree_epi (R : CommRingCat) (X : AffineQuasicoherentSheaves R) : ∃ (P : AffineQuasicoherentSheaves R) (p : P ⟶ X), affineQuasicoherentFreeObjects R P ∧ CategoryTheory.Epi p

Every affine quasi-coherent sheaf is an epimorphic image of an arbitrary-rank free one.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentFreeInclusionIso (R : CommRingCat) (I : Type u) : (affineQuasicoherentSheavesInclusion R).obj (affineQuasicoherentFree R I) ≅ SheafOfModules.free I

Forgetting an affine quasi-coherent free object identifies it with the usual free sheaf of modules.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentFreeInclusionIso R I = AlgebraicGeometry.tildeFinsupp I

theorem AlgebraicGeometry.DerivedCategory.Dqc.subsingleton_ext_affineQuasicoherentFree_inclusion (R : CommRingCat) (I : Type u) (Y : AffineQuasicoherentSheaves R) (n : ℕ) : Subsingleton (CategoryTheory.Abelian.Ext ((affineQuasicoherentSheavesInclusion R).obj (affineQuasicoherentFree R I)) ((affineQuasicoherentSheavesInclusion R).obj Y) (n + 1))

Higher Ext from an arbitrary-rank affine quasi-coherent free sheaf vanishes after forgetting to all module sheaves. The free sheaf is a coproduct of copies of the structure sheaf, whose Ext computes affine quasi-coherent cohomology.

theorem AlgebraicGeometry.DerivedCategory.Dqc.subsingleton_ext_affineQuasicoherentFree (R : CommRingCat) (I : Type u) (Y : AffineQuasicoherentSheaves R) (n : ℕ) : Subsingleton (CategoryTheory.Abelian.Ext (affineQuasicoherentFree R I) Y (n + 1))

Higher Ext from an arbitrary-rank free object vanishes inside affine quasi-coherent sheaves because that object is projective.

def AlgebraicGeometry.DerivedCategory.Dqc.AffineQuasicoherentExtComparison (R : CommRingCat) : Prop

The exact affine quasi-coherent inclusion induces bijections on all Ext groups.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentExtComparison (R : CommRingCat) : AffineQuasicoherentExtComparison R

Affine quasi-coherent Ext comparison. The arbitrary-rank free objects form projective generators on the source and remain acyclic against quasi-coherent targets after inclusion into all module sheaves.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedInclusion_map_bijective (R : CommRingCat) (E E' : AffineQuasicoherentBoundedDerivedCategory R) : Function.Bijective (DerivedCategory.Bounded.ι.comp (affineQuasicoherentDerivedInclusion R)).map

The bounded affine derived inclusion is bijective on each hom-set.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedToDqc_full (R : CommRingCat) : (DerivedCategory.Bounded.ι.comp (affineQuasicoherentDerivedToDqc R)).Full

The bounded affine realization into Dqc is full before restricting the target to bounded objects.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedToDqc_faithful (R : CommRingCat) : (DerivedCategory.Bounded.ι.comp (affineQuasicoherentDerivedToDqc R)).Faithful

The bounded affine realization into Dqc is faithful before restricting the target to bounded objects.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedToDqc_full (R : CommRingCat) : (affineQuasicoherentBoundedDerivedToDqc R).Full

The concrete bounded affine realization is full.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedToDqc_faithful (R : CommRingCat) : (affineQuasicoherentBoundedDerivedToDqc R).Faithful

The concrete bounded affine realization is faithful.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedToDqc_essSurj (R : CommRingCat) : (affineQuasicoherentBoundedDerivedToDqc R).EssSurj

Every intrinsically bounded object of Dqc(Spec R) is represented by a bounded complex of affine quasi-coherent sheaves.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDqcEquivalence (R : CommRingCat) : AffineQuasicoherentBoundedDerivedCategory R ≌ SchemeBoundedQuasicoherentDerivedCategory (Spec R)

Bounded affine Dqc identification. The concrete realization functor is an equivalence between the bounded derived category of affine quasi-coherent sheaves and the intrinsic bounded quasi-coherent-cohomology locus.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDqcEquivalence R = (AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDerivedToDqc R).asEquivalence

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentBoundedDqcEquivalence_functor (R : CommRingCat) : (affineQuasicoherentBoundedDqcEquivalence R).functor = affineQuasicoherentBoundedDerivedToDqc R

structure AlgebraicGeometry.DerivedCategory.Dqc.AffineQuasicoherentDqcIdentification (R : CommRingCat) : Type (u + 1)

The explicit unbounded affine Dqc identification interface. Its comparison field ensures that an abstract equivalence is the concrete derived realization constructed in AffineRealization.lean. This file does not construct an inhabitant.

• equivalence : AffineQuasicoherentDerivedCategory R ≌ SchemeQuasicoherentDerivedCategory (Spec R)

  The abstract equivalence with the quasi-coherent locus on Spec R.

• comparison : self.equivalence.functor ≅ affineQuasicoherentDerivedToDqc R

  The equivalence is the concrete derived realization, not merely some equivalence of the two categories.

def AlgebraicGeometry.DerivedCategory.Dqc.HasAffineQuasicoherentDqcIdentification (R : CommRingCat) : Prop

The proposition that the explicit unbounded affine Dqc identification is available.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.HasAffineQuasicoherentDqcIdentification R = Nonempty (AlgebraicGeometry.DerivedCategory.Dqc.AffineQuasicoherentDqcIdentification R)

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedToDqc_full_of_identification {R : CommRingCat} (I : AffineQuasicoherentDqcIdentification R) : (affineQuasicoherentDerivedToDqc R).Full

An unbounded affine identification makes the concrete realization full.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedToDqc_faithful_of_identification {R : CommRingCat} (I : AffineQuasicoherentDqcIdentification R) : (affineQuasicoherentDerivedToDqc R).Faithful

An unbounded affine identification makes the concrete realization faithful.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedToDqc_essSurj_of_identification {R : CommRingCat} (I : AffineQuasicoherentDqcIdentification R) : (affineQuasicoherentDerivedToDqc R).EssSurj

An unbounded affine identification makes the concrete realization essentially surjective.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDqcEquivalenceOfIdentification {R : CommRingCat} (I : AffineQuasicoherentDqcIdentification R) : AffineQuasicoherentDerivedCategory R ≌ SchemeQuasicoherentDerivedCategory (Spec R)

Repackage an unbounded identification as an equivalence whose forward functor is definitionally the concrete affine realization.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDqcEquivalenceOfIdentification I = (AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDerivedToDqc R).asEquivalence

@[simp]

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineQuasicoherentDqcEquivalenceOfIdentification_functor {R : CommRingCat} (I : AffineQuasicoherentDqcIdentification R) : (affineQuasicoherentDqcEquivalenceOfIdentification I).functor = affineQuasicoherentDerivedToDqc R