The groupoid-valued affine geometric pullback pseudofunctor

This file takes the maximal subgroupoid of the geometric affine bounded-above projective derived locus. Objects remain genuine quasi-coherent complexes on affine schemes, while morphisms are restricted to isomorphisms as required by a moduli problem.

The transition functors, unit, and compositor are induced from the geometric affine pseudofunctor. Their coherence is proved from the corresponding derived-category pentagon and triangle identities.

@[reducible, inline]

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

The groupoid of geometric affine bounded-above projective derived objects over Spec R.

Equations

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

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

Arbitrary affine pullback on the maximal subgroupoids of the geometric bounded-above projective loci.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineGeometricBoundedAboveProjectiveCorePullback f = (AlgebraicGeometry.DerivedCategory.Dqc.affineGeometricBoundedAboveProjectiveDerivedPullback f).core

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineGeometricBoundedAboveProjectiveCorePullbackIdIso (R : CommRingCat) : affineGeometricBoundedAboveProjectiveCorePullback (CategoryTheory.CategoryStruct.id R) ≅ CategoryTheory.Functor.id (AffineBoundedAboveProjectiveModuliFiber R)

The unit comparison after passing geometric affine pullback to maximal subgroupoids.

Equations

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

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

The compositor after passing geometric affine pullback to maximal subgroupoids, oriented as required by LocallyDiscrete.mkPseudofunctor.

Equations

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

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

The genuine geometric affine bounded-above projective moduli groupoids and their arbitrary pullbacks, packaged as a Cat-valued pseudofunctor.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineBoundedAboveProjectiveModuliForget (R : CommRingCat) : CategoryTheory.Functor (AffineBoundedAboveProjectiveModuliFiber R) (SchemeQuasicoherentDerivedCategory (Spec R))

Forgetting the affine moduli groupoid to the honest geometric derived locus.

Equations

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