Coherent affine pullback on the bounded-projective derived locus

The affine bounded-projective homotopy pseudofunctor is transported through the localization equivalences onto its essential image in the derived category.

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

The supported affine derived compositor satisfies the pentagon equation.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineBoundedAboveProjectiveDerivedPullback_leftUnitality {R A : CommRingCat} (f : R ⟶ A) : CategoryTheory.CategoryStruct.comp (affineBoundedAboveProjectiveDerivedPullbackCompIso (CategoryTheory.CategoryStruct.id R) f).symm.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (affineBoundedAboveProjectiveDerivedPullbackIdIso R).hom (affineBoundedAboveProjectiveDerivedPullback f)) (affineBoundedAboveProjectiveDerivedPullback f).leftUnitor.hom) = CategoryTheory.CategoryStruct.id (affineBoundedAboveProjectiveDerivedPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id R) f))

The supported affine derived compositor and unit satisfy the left triangle equation.

theorem AlgebraicGeometry.DerivedCategory.Dqc.affineBoundedAboveProjectiveDerivedPullback_rightUnitality {R A : CommRingCat} (f : R ⟶ A) : CategoryTheory.CategoryStruct.comp (affineBoundedAboveProjectiveDerivedPullbackCompIso f (CategoryTheory.CategoryStruct.id A)).symm.hom (CategoryTheory.CategoryStruct.comp ((affineBoundedAboveProjectiveDerivedPullback f).whiskerLeft (affineBoundedAboveProjectiveDerivedPullbackIdIso A).hom) (affineBoundedAboveProjectiveDerivedPullback f).rightUnitor.hom) = CategoryTheory.CategoryStruct.id (affineBoundedAboveProjectiveDerivedPullback (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id A)))

The supported affine derived compositor and unit satisfy the right triangle equation.

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

Arbitrary affine pullback on the bounded-above projective derived loci, packaged with its transported unit, compositor, pentagon, and triangle equations.

Equations

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