Pullback of quasi-isomorphisms between K-flat scheme-module complexes

Arbitrary scheme pullback preserves a quasi-isomorphism between complexes whose right tensor functors invert quasi-isomorphisms. K-flatness supplies these two hypotheses. The argument uses the free-Yoneda K-flat resolution, exactness and detection of quasi-isomorphisms at module stalks, and the fixed-left ordinary tensor/stalk natural isomorphism.

Main definitions

• AlgebraicGeometry.Scheme.Modules.quasiIso_pullback_of_tensorRight_inverts uses only the right tensor-inversion halves of K-flatness.

Main results

• AlgebraicGeometry.Scheme.Modules.quasiIso_pullback_of_isKFlat specializes this to K-flat complexes.

Implementation notes

The generic functor and scalar-change transports below are private proof helpers. No derived pullback functor is asserted in this file.

References

AlgebraicGeometry.Scheme.Modules.pullback is the pinned Mathlib functor. The fixed-left tensor and stalk comparisons used here are existing repository results, combined with the canonical free-Yoneda K-flat resolution.

Tags

scheme module, pullback, K-flat complex, quasi-isomorphism

theorem AlgebraicGeometry.Scheme.Modules.quasiIso_pullback_of_tensorRight_inverts {X Y : Scheme} (f : X ⟶ Y) {K L : CochainComplex Y.Modules ℤ} (g : K ⟶ L) (hg : HomologicalComplex.quasiIso Y.Modules (ComplexShape.up ℤ) g) (hK : (HomologicalComplex.quasiIso Y.Modules (ComplexShape.up ℤ)).IsInvertedBy (((totalTensor Y).flip.obj K).comp DerivedCategory.Q)) (hL : (HomologicalComplex.quasiIso Y.Modules (ComplexShape.up ℤ)).IsInvertedBy (((totalTensor Y).flip.obj L).comp DerivedCategory.Q)) : QuasiIso (((pullback f).mapHomologicalComplex (ComplexShape.up ℤ)).map g)

Pullback along any scheme morphism preserves a quasi-isomorphism when both source complexes invert quasi-isomorphisms under tensor in the right slot. The proof tests after stalks, realizes the needed stalk module by a sheaf, and uses the ordinary fixed-left tensor/stalk comparison.

theorem AlgebraicGeometry.Scheme.Modules.quasiIso_pullback_of_isKFlat {X Y : Scheme} (f : X ⟶ Y) {K L : CochainComplex Y.Modules ℤ} (g : K ⟶ L) (hg : HomologicalComplex.quasiIso Y.Modules (ComplexShape.up ℤ) g) (hK : CategoryTheory.CochainComplex.IsKFlat (totalTensor Y) K) (hL : CategoryTheory.CochainComplex.IsKFlat (totalTensor Y) L) : QuasiIso (((pullback f).mapHomologicalComplex (ComplexShape.up ℤ)).map g)

K-flatness supplies the right tensor-inversion hypotheses at both endpoints, so the stronger pullback criterion applies using only those halves of the K-flatness assumptions.