Derived pullback from K-projective replacements, with no hypothesis on the morphism

PullbackAcyclicResolution and KFlatPullbackAcyclic both carry two fields that are assertions about the morphism being derived: that pullback along f inverts the quasi-isomorphisms produced by the replacement, and that it inverts the comparison of an already replaced complex. Until now those two fields were supplied by the caller for every nonexact f, so the arbitrary derived pullback was inhabited only by assuming the preservation it was supposed to construct.

This file removes both assertions for replacements whose values are K-projective. A quasi-isomorphism between K-projective cochain complexes is already an isomorphism in the homotopy category, and degreewise pullback is additive, so it preserves the homotopies witnessing that isomorphism. The two acyclicity fields are therefore theorems, proved for an arbitrary morphism of scheme base changes: no exactness, no flatness, no limit preservation, and no caller-supplied assertion about f.

What remains supplied is the replacement itself. Nothing here constructs a functorial K-projective -- or K-flat -- replacement on X.Modules, and this file makes no claim that one exists. That is a separate open deliverable of SF8.5, and on a general scheme the category of all 𝒪_X-modules does not have enough projectives, so the honest general-scheme route is a K-flat replacement whose transport along f is still open. The statements below are about what a replacement buys once it is in hand, and they are phrased so that the K-projectivity hypothesis stays visible at every call site.

Main statements

• SchemeBaseChange.quasiIso_complexPullback_map_of_isKProjective: degreewise pullback along an arbitrary morphism preserves quasi-isomorphisms between K-projective complexes.
• SchemeBaseChange.PullbackAcyclicResolution.ofKProjective: a functorial K-projective replacement is a pullback-acyclic resolution along every morphism.
• SchemeBaseChange.kFlatPullbackAcyclic_of_isKProjective: the K-flat pullback-acyclicity hypothesis of kFlatLeftDerivedPullback is discharged, rather than assumed, for a K-projective-valued K-flat replacement.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.quasiIso_complexPullback_map_of_isKProjective {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) {K L : CochainComplex (CategoryTheory.Over.left U).Modules ℤ} [K.IsKProjective] [L.IsKProjective] {g : K ⟶ L} (hg : HomologicalComplex.quasiIso (CategoryTheory.Over.left U).Modules (ComplexShape.up ℤ) g) : HomologicalComplex.quasiIso (CategoryTheory.Over.left T).Modules (ComplexShape.up ℤ) ((complexPullback f).map g)

Degreewise pullback along an arbitrary morphism of scheme base changes carries a quasi-isomorphism between K-projective complexes to a quasi-isomorphism.

The morphism carries no exactness, flatness, or limit-preservation hypothesis. Only additivity of module-sheaf pullback is used, and that holds for every scheme morphism.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.isIso_complexPullback_map_of_isKProjective {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) {K L : CochainComplex (CategoryTheory.Over.left U).Modules ℤ} [K.IsKProjective] [L.IsKProjective] {g : K ⟶ L} (hg : HomologicalComplex.quasiIso (CategoryTheory.Over.left U).Modules (ComplexShape.up ℤ) g) : CategoryTheory.IsIso (((complexPullback f).comp (SchemeDerivedCategory.Q (CategoryTheory.Over.left T))).map g)

The localized form of quasiIso_complexPullback_map_of_isKProjective: pullback of a quasi-isomorphism between K-projective complexes becomes an isomorphism in the derived category of the source scheme.

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution.ofKProjective {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) (resolution : CategoryTheory.Functor (CochainComplex (CategoryTheory.Over.left U).Modules ℤ) (CochainComplex (CategoryTheory.Over.left U).Modules ℤ)) (comparison : resolution ⟶ CategoryTheory.Functor.id (CochainComplex (CategoryTheory.Over.left U).Modules ℤ)) (hcomparison : ∀ (K : CochainComplex (CategoryTheory.Over.left U).Modules ℤ), HomologicalComplex.quasiIso (CategoryTheory.Over.left U).Modules (ComplexShape.up ℤ) (comparison.app K)) (hKProjective : ∀ (K : CochainComplex (CategoryTheory.Over.left U).Modules ℤ), (resolution.obj K).IsKProjective) : PullbackAcyclicResolution f

A functorial replacement whose values are K-projective is a pullback-acyclic resolution along every morphism of scheme base changes.

Both acyclicity fields of PullbackAcyclicResolution are proved here. The hypotheses hcomparison and hKProjective speak only about the replacement on U; neither mentions f, so one replacement serves every morphism out of U simultaneously.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kProjectiveLeftDerivedPullback {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) (resolution : CategoryTheory.Functor (CochainComplex (CategoryTheory.Over.left U).Modules ℤ) (CochainComplex (CategoryTheory.Over.left U).Modules ℤ)) (comparison : resolution ⟶ CategoryTheory.Functor.id (CochainComplex (CategoryTheory.Over.left U).Modules ℤ)) (hcomparison : ∀ (K : CochainComplex (CategoryTheory.Over.left U).Modules ℤ), HomologicalComplex.quasiIso (CategoryTheory.Over.left U).Modules (ComplexShape.up ℤ) (comparison.app K)) (hKProjective : ∀ (K : CochainComplex (CategoryTheory.Over.left U).Modules ℤ), (resolution.obj K).IsKProjective) : LeftDerivedPullback f

Arbitrary left-derived pullback, inhabited from a functorial K-projective replacement alone.

There is no hypothesis on f and no supplied preservation assertion: the universal property comes from PullbackAcyclicResolution.isLeftDerived, and its two acyclicity inputs are proved in ofKProjective.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kProjectiveExactComparison {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsExactPullback f] (resolution : CategoryTheory.Functor (CochainComplex (CategoryTheory.Over.left U).Modules ℤ) (CochainComplex (CategoryTheory.Over.left U).Modules ℤ)) (comparison : resolution ⟶ CategoryTheory.Functor.id (CochainComplex (CategoryTheory.Over.left U).Modules ℤ)) (hcomparison : ∀ (K : CochainComplex (CategoryTheory.Over.left U).Modules ℤ), HomologicalComplex.quasiIso (CategoryTheory.Over.left U).Modules (ComplexShape.up ℤ) (comparison.app K)) (hKProjective : ∀ (K : CochainComplex (CategoryTheory.Over.left U).Modules ℤ), (resolution.obj K).IsKProjective) : (kProjectiveLeftDerivedPullback f resolution comparison hcomparison hKProjective).functor ≅ derivedPullback f

When ordinary pullback happens to be exact, the K-projective construction normalizes to the existing exact derived pullback.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatPullbackAcyclic_of_isKProjective {S : Scheme} {T U : SchemeBaseChange S} (R : SchemeKFlatResolution (CategoryTheory.Over.left U)) (f : T ⟶ U) (hKProjective : ∀ (K : CochainComplex (CategoryTheory.Over.left U).Modules ℤ), (R.resolution.obj K).IsKProjective) : KFlatPullbackAcyclic R f

Pullback-acyclicity of a K-flat replacement is a theorem, not a caller-supplied hypothesis, as soon as the replacement is K-projective valued.

This discharges the KFlatPullbackAcyclic argument of kFlatLeftDerivedPullback for an arbitrary morphism, where previously it was provable only for exact and flat morphisms and otherwise assumed.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatLeftDerivedPullbackOfKProjective {S : Scheme} {T U : SchemeBaseChange S} (R : SchemeKFlatResolution (CategoryTheory.Over.left U)) (f : T ⟶ U) (hKProjective : ∀ (K : CochainComplex (CategoryTheory.Over.left U).Modules ℤ), (R.resolution.obj K).IsKProjective) : LeftDerivedPullback f

The K-flat derived pullback along an arbitrary morphism, with its acyclicity hypothesis proved rather than supplied.

Equations

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