Derived pullback on K-flat quasi-coherent representatives

For a complex with quasi-coherent terms whose right tensor functor inverts quasi-isomorphisms, the canonical arbitrary left-derived pullback has quasi-coherent cohomology. K-flatness supplies that inversion premise. The theorems do not supply such a representative for every object of Dqc.

Main definitions

This file introduces no new carrier, class, or instance.

Main results

• Right-tensor inversion gives conditional preservation along any morphism.
• K-flatness is an immediate specialization.

Implementation notes

The generic objectwise comparison from KFlatPullback.lean identifies canonical derived pullback with ordinary pullback on the supplied acyclic representative. Ordinary pullback preserves quasi-coherent terms.

References

The proof uses the repository's AlgebraicGeometry.Scheme.Modules.quasiIso_pullback_of_tensorRight_inverts, AlgebraicGeometry.Scheme.Modules.isQuasicoherent_pullback, and canonical K-flat resolution.

Tags

scheme base change, derived pullback, K-flat, quasi-coherence

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.quasicoherentCohomology_arbitraryLeftDerivedPullback_of_tensorRightInverts_of_termwiseQC {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) (K : CochainComplex (CategoryTheory.Over.left U).Modules ℤ) (hRight : (HomologicalComplex.quasiIso (CategoryTheory.Over.left U).Modules (ComplexShape.up ℤ)).IsInvertedBy (((Scheme.Modules.totalTensor (CategoryTheory.Over.left U)).flip.obj K).comp DerivedCategory.Q)) (hK : ∀ (n : ℤ), SheafOfModules.IsQuasicoherent (K.X n)) : Dqc.schemeQuasicoherentCohomology (CategoryTheory.Over.left T) ((arbitraryLeftDerivedPullback f).functor.obj ((SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).obj K))

Right-tensor inversion makes the pulled-back resolution comparison invertible, so ordinary pullback computes the canonical derived pullback on this representative. The theorem does not construct such a representative for an arbitrary derived object.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.quasicoherentCohomology_arbitraryLeftDerivedPullback_of_isKFlat_of_termwiseQuasicoherent {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) (K : CochainComplex (CategoryTheory.Over.left U).Modules ℤ) (hflat : CategoryTheory.CochainComplex.IsKFlat (Scheme.Modules.totalTensor (CategoryTheory.Over.left U)) K) (hK : ∀ (n : ℤ), SheafOfModules.IsQuasicoherent (K.X n)) : Dqc.schemeQuasicoherentCohomology (CategoryTheory.Over.left T) ((arbitraryLeftDerivedPullback f).functor.obj ((SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).obj K))

K-flatness supplies the right-tensor inversion used to compare the canonical derived pullback with ordinary pullback on the given complex. This does not supply a quasi-coherent K-flat representative for every Dqc object.