Preservation of the affine bounded-above projective locus

Extension of scalars preserves projective modules, so the generic bounded-above projective derived functor specializes to a composable affine pullback without a flatness hypothesis.

instance AlgebraicGeometry.DerivedCategory.Dqc.affineExtendScalars_preservesProjectiveObjects {R A : CommRingCat} (f : R ⟶ A) : (ModuleCat.extendScalars (CommRingCat.Hom.hom f)).PreservesProjectiveObjects

Extension of scalars preserves projective modules.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineBoundedAboveProjectiveHomotopyPullback {R A : CommRingCat} (f : R ⟶ A) : CategoryTheory.Functor (CategoryTheory.BoundedAboveProjectiveHomotopyCategory (ModuleCat ↑R)) (CategoryTheory.BoundedAboveProjectiveHomotopyCategory (ModuleCat ↑A))

Arbitrary affine extension of scalars acts on bounded-above projective homotopy representatives.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineBoundedAboveProjectiveHomotopyPullback f = CategoryTheory.mapBoundedAboveProjectiveHomotopy (ModuleCat.extendScalars (CommRingCat.Hom.hom f))

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

Affine extension of scalars composes on bounded-above projective homotopy representatives.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.affineBoundedAboveProjectiveDerivedPullback {R A : CommRingCat} (f : R ⟶ A) : CategoryTheory.Functor (CategoryTheory.BoundedAboveProjectiveDerivedCategory (ModuleCat ↑R)) (CategoryTheory.BoundedAboveProjectiveDerivedCategory (ModuleCat ↑A))

Arbitrary affine derived pullback preserves the full derived locus represented by bounded-above complexes of projective modules.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.affineBoundedAboveProjectiveDerivedPullback f = CategoryTheory.boundedAboveProjectiveDerivedFunctor (ModuleCat.extendScalars (CommRingCat.Hom.hom f))

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

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

Equations

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