The geometric affine bounded-projective pseudofunctor

The bounded-above projective derived locus was initially constructed in the derived category of modules over the coordinate ring. This file realizes that locus as a genuine full subcategory of the derived category of quasi-coherent sheaves on the affine spectrum. The module-side pullback pseudofunctor is then transported across the resulting objectwise equivalences.

Finally, the geometric locus is mapped into the honest Dqc(Spec R) category by the exact affine realization functor.

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

Realize the module-side bounded-above projective derived locus in the derived category of quasi-coherent sheaves on the affine spectrum.

Equations

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

instance AlgebraicGeometry.DerivedCategory.Dqc.affineBoundedAboveProjectiveQuasicoherentRealization_full (R : CommRingCat) : (affineBoundedAboveProjectiveQuasicoherentRealization R).Full

instance AlgebraicGeometry.DerivedCategory.Dqc.affineBoundedAboveProjectiveQuasicoherentRealization_faithful (R : CommRingCat) : (affineBoundedAboveProjectiveQuasicoherentRealization R).Faithful

@[reducible, inline]

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

The full geometric affine derived locus represented by bounded-above complexes of projective coordinate-ring modules.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineBoundedAboveProjectiveQuasicoherentEquivalence (R : CommRingCat) : CategoryTheory.BoundedAboveProjectiveDerivedCategory (ModuleCat ↑R) ≌ AffineBoundedAboveProjectiveQuasicoherentDerivedCategory R

The module-side bounded-above projective locus is equivalent to its geometric realization in affine quasi-coherent complexes.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineGeometricBoundedAboveProjectiveDerivedPullback {R A : CommRingCat} (f : R ⟶ A) : CategoryTheory.Functor (AffineBoundedAboveProjectiveQuasicoherentDerivedCategory R) (AffineBoundedAboveProjectiveQuasicoherentDerivedCategory A)

Arbitrary affine pullback on the geometric bounded-above projective derived loci.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineGeometricBoundedAboveProjectiveDerivedPullbackCompIso {R A B : CommRingCat} (f : R ⟶ A) (g : A ⟶ B) : (affineGeometricBoundedAboveProjectiveDerivedPullback f).comp (affineGeometricBoundedAboveProjectiveDerivedPullback g) ≅ affineGeometricBoundedAboveProjectiveDerivedPullback (CategoryTheory.CategoryStruct.comp f g)

The compositor for geometric affine bounded-above projective pullback.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineGeometricBoundedAboveProjectiveDerivedPullbackIdIso (R : CommRingCat) : affineGeometricBoundedAboveProjectiveDerivedPullback (CategoryTheory.CategoryStruct.id R) ≅ CategoryTheory.Functor.id (AffineBoundedAboveProjectiveQuasicoherentDerivedCategory R)

The unit comparison for geometric affine bounded-above projective pullback.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineGeometricBoundedAboveProjectiveDerivedPullback_associativity {R A B C : CommRingCat} (f : R ⟶ A) (g : A ⟶ B) (h : B ⟶ C) : CategoryTheory.CategoryStruct.comp (affineGeometricBoundedAboveProjectiveDerivedPullbackCompIso (CategoryTheory.CategoryStruct.comp f g) h).symm.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (affineGeometricBoundedAboveProjectiveDerivedPullbackCompIso f g).symm.hom (affineGeometricBoundedAboveProjectiveDerivedPullback h)) (CategoryTheory.CategoryStruct.comp ((affineGeometricBoundedAboveProjectiveDerivedPullback f).associator (affineGeometricBoundedAboveProjectiveDerivedPullback g) (affineGeometricBoundedAboveProjectiveDerivedPullback h)).hom (CategoryTheory.CategoryStruct.comp ((affineGeometricBoundedAboveProjectiveDerivedPullback f).whiskerLeft (affineGeometricBoundedAboveProjectiveDerivedPullbackCompIso g h).hom) (affineGeometricBoundedAboveProjectiveDerivedPullbackCompIso f (CategoryTheory.CategoryStruct.comp g h)).hom))) = CategoryTheory.CategoryStruct.id (affineGeometricBoundedAboveProjectiveDerivedPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h))

The geometric affine compositors satisfy the pentagon equation.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineGeometricBoundedAboveProjectiveDerivedPullback_leftUnitality {R A : CommRingCat} (f : R ⟶ A) : CategoryTheory.CategoryStruct.comp (affineGeometricBoundedAboveProjectiveDerivedPullbackCompIso (CategoryTheory.CategoryStruct.id R) f).symm.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (affineGeometricBoundedAboveProjectiveDerivedPullbackIdIso R).hom (affineGeometricBoundedAboveProjectiveDerivedPullback f)) (affineGeometricBoundedAboveProjectiveDerivedPullback f).leftUnitor.hom) = CategoryTheory.CategoryStruct.id (affineGeometricBoundedAboveProjectiveDerivedPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id R) f))

The unit compatibility required to package the transported pullbacks as a pseudofunctor, obtained from the module-side left triangle.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineGeometricBoundedAboveProjectiveDerivedPullback_rightUnitality {R A : CommRingCat} (f : R ⟶ A) : CategoryTheory.CategoryStruct.comp (affineGeometricBoundedAboveProjectiveDerivedPullbackCompIso f (CategoryTheory.CategoryStruct.id A)).symm.hom (CategoryTheory.CategoryStruct.comp ((affineGeometricBoundedAboveProjectiveDerivedPullback f).whiskerLeft (affineGeometricBoundedAboveProjectiveDerivedPullbackIdIso A).hom) (affineGeometricBoundedAboveProjectiveDerivedPullback f).rightUnitor.hom) = CategoryTheory.CategoryStruct.id (affineGeometricBoundedAboveProjectiveDerivedPullback (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id A)))

The second unit compatibility required to package the transported pullbacks as a pseudofunctor, obtained from the module-side right triangle.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineGeometricBoundedAboveProjectiveDerivedPseudofunctor : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete CommRingCat) CategoryTheory.Cat

The genuine geometric affine bounded-above projective loci and their arbitrary pullbacks, packaged as a pseudofunctor.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineGeometricBoundedAboveProjectiveDerivedToDqc (R : CommRingCat) : CategoryTheory.Functor (AffineBoundedAboveProjectiveQuasicoherentDerivedCategory R) (SchemeQuasicoherentDerivedCategory (Spec R))

Realization of the geometric bounded-above projective affine locus in the honest quasi-coherent-cohomology category Dqc(Spec R).

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineBoundedAboveProjectiveQuasicoherentEquivalenceCompToDqc (R : CommRingCat) : (affineBoundedAboveProjectiveQuasicoherentEquivalence R).functor.comp (affineGeometricBoundedAboveProjectiveDerivedToDqc R) ≅ (affineBoundedAboveProjectiveQuasicoherentRealization R).comp (affineQuasicoherentDerivedToDqc R)

The geometric realization agrees with the module-side realization after passing through the objectwise equivalence.

Equations

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