Derived pullback from K-flat resolutions

A K-flat resolution on the source of pullback already supplies the functorial replacement, comparison, and quasi-isomorphism required by AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.PullbackAcyclicResolution. This file isolates the two remaining operational facts about pullback of those replacements and constructs the genuine left-derived pullback universal property from them.

Quasicoherence and compactness are reduced to the resolved complex-level pullback. Thus the base-change construction no longer needs independently supplied functors on derived categories: all categorical structure descends from one K-flat replacement and explicit geometric evidence.

Main definitions

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatPullbackAcyclic records the two pullback-acyclicity fields.
• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.arbitraryLeftDerivedPullback uses the canonical free-Yoneda resolution.

Main results

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatPullbackAcyclic proves both fields for any K-flat resolution and morphism.
• The right-tensor comparison identifies canonical derived pullback with ordinary pullback on a supplied tensor-acyclic complex. Its K-flat specialization supplies the inversion premise.

Implementation notes

The caller-free constructor applies the existing left-derived universal-property construction to the canonical resolution and the acyclicity theorem.

References

The resolution and derived functor constructions are in the repository's DerivedCategory/Tensor/FreeYonedaKFlat.lean and DerivedCategory/Families/PullbackAcyclicResolution.lean modules.

Tags

scheme pullback, derived category, K-flat resolution

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatResolvedPullback {S : Scheme} {T U : SchemeBaseChange S} (R : SchemeKFlatResolution (CategoryTheory.Over.left U)) (f : T ⟶ U) : CategoryTheory.Functor (CochainComplex (CategoryTheory.Over.left U).Modules ℤ) T.DerivedFiber

Resolve a complex by a K-flat replacement on U, pull it back to T, and localize.

Equations

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

structure AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatPullbackAcyclic {S : Scheme} {T U : SchemeBaseChange S} (R : SchemeKFlatResolution (CategoryTheory.Over.left U)) (f : T ⟶ U) : Prop

The exact geometric conditions under which a K-flat replacement is acyclic for pullback.

The first field lets resolved pullback descend through source localization. The second says that the comparison is invertible after pulling back an already resolved complex; this is the idempotence input used by the left-derived universal property.

• pullback_inverts : (HomologicalComplex.quasiIso (CategoryTheory.Over.left U).Modules (ComplexShape.up ℤ)).IsInvertedBy (kFlatResolvedPullback R f)
• resolved_comparison_isIso (K : CochainComplex (CategoryTheory.Over.left U).Modules ℤ) : CategoryTheory.IsIso (((complexPullback f).comp (SchemeDerivedCategory.Q (CategoryTheory.Over.left T))).map (R.comparison.app (R.resolution.obj K)))

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatPullbackAcyclic_ofExact {S : Scheme} {T U : SchemeBaseChange S} (R : SchemeKFlatResolution (CategoryTheory.Over.left U)) (f : T ⟶ U) [IsExactPullback f] : KFlatPullbackAcyclic R f

Along an exact pullback, every K-flat replacement is automatically pullback-acyclic. Exactness preserves the quasi-isomorphisms produced by the replacement, including its comparison on an already resolved complex.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatPullbackAcyclic_ofFlat {S : Scheme} {T U : SchemeBaseChange S} (R : SchemeKFlatResolution (CategoryTheory.Over.left U)) (f : T ⟶ U) [Flat (CategoryTheory.Over.Hom.left f)] : KFlatPullbackAcyclic R f

Flat scheme pullback is an unconditional geometric case of K-flat pullback acyclicity.

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatPullbackAcyclic {S : Scheme} {T U : SchemeBaseChange S} (R : SchemeKFlatResolution (CategoryTheory.Over.left U)) (f : T ⟶ U) : KFlatPullbackAcyclic R f

Every K-flat resolution is acyclic for pullback along an arbitrary scheme morphism. Both fields follow by applying pullback preservation to quasi-isomorphisms between resolved complexes; for the second field these are the once- and twice-resolved complexes.

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatPullbackAcyclicResolution {S : Scheme} {T U : SchemeBaseChange S} (R : SchemeKFlatResolution (CategoryTheory.Over.left U)) (f : T ⟶ U) (hR : KFlatPullbackAcyclic R f) : PullbackAcyclicResolution f

A K-flat resolution satisfying the pullback-acyclicity conditions constructs the existing functorial pullback-acyclic resolution interface.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatLeftDerivedPullback {S : Scheme} {T U : SchemeBaseChange S} (R : SchemeKFlatResolution (CategoryTheory.Over.left U)) (f : T ⟶ U) (hR : KFlatPullbackAcyclic R f) : LeftDerivedPullback f

The genuine left-derived pullback constructed from a pullback-acyclic K-flat replacement.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.arbitraryLeftDerivedPullback {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) : LeftDerivedPullback f

The left-derived pullback for any morphism in Over S, constructed using the canonical free-Yoneda K-flat resolution and its proved pullback acyclicity. No preservation assertion or resolution is supplied by the caller.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullbackObjIsoOfTensorRightInverts {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)) : (arbitraryLeftDerivedPullback f).functor.obj ((SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).obj K) ≅ (SchemeDerivedCategory.Q (CategoryTheory.Over.left T)).obj ((complexPullback f).obj K)

On an input whose right tensor functor inverts quasi-isomorphisms, ordinary pullback computes the canonical arbitrary left-derived pullback. The comparison uses the canonical free-Yoneda resolution but does not require its terms to be quasi-coherent.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullbackObjIsoOfKFlat {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) (K : CochainComplex (CategoryTheory.Over.left U).Modules ℤ) (hK : CategoryTheory.CochainComplex.IsKFlat (Scheme.Modules.totalTensor (CategoryTheory.Over.left U)) K) : (arbitraryLeftDerivedPullback f).functor.obj ((SchemeDerivedCategory.Q (CategoryTheory.Over.left U)).obj K) ≅ (SchemeDerivedCategory.Q (CategoryTheory.Over.left T)).obj ((complexPullback f).obj K)

Ambient K-flatness supplies the right-tensor inversion premise for the objectwise comparison with ordinary pullback.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatExactPullbackComparison {S : Scheme} {T U : SchemeBaseChange S} (R : SchemeKFlatResolution (CategoryTheory.Over.left U)) (f : T ⟶ U) [IsExactPullback f] : (kFlatLeftDerivedPullback R f ⋯).functor ≅ derivedPullback f

For exact pullback, the K-flat construction agrees canonically with the existing exact derived pullback.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatFlatPullbackComparison {S : Scheme} {T U : SchemeBaseChange S} (R : SchemeKFlatResolution (CategoryTheory.Over.left U)) (f : T ⟶ U) [Flat (CategoryTheory.Over.Hom.left f)] : (kFlatLeftDerivedPullback R f ⋯).functor ≅ derivedPullback f

The exact comparison specialized to a flat scheme morphism.

Equations

• AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatFlatPullbackComparison R f = AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatExactPullbackComparison R f

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatResolvedPullbackPreservesQuasicoherentCohomology {S : Scheme} {T U : SchemeBaseChange S} (R : SchemeKFlatResolution (CategoryTheory.Over.left U)) (f : T ⟶ U) : Prop

Quasicoherence preservation stated only on resolved complex representatives.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatLeftDerivedPullback_preservesQuasicoherentCohomology {S : Scheme} {T U : SchemeBaseChange S} (R : SchemeKFlatResolution (CategoryTheory.Over.left U)) (f : T ⟶ U) (hR : KFlatPullbackAcyclic R f) (hqc : KFlatResolvedPullbackPreservesQuasicoherentCohomology R f) (E : U.DerivedFiber) : Dqc.schemeQuasicoherentCohomology (CategoryTheory.Over.left U) E → Dqc.schemeQuasicoherentCohomology (CategoryTheory.Over.left T) ((kFlatLeftDerivedPullback R f hR).functor.obj E)

Quasicoherence preservation for K-flat derived pullback follows from the resolved complex-level claim.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatDqcLeftDerivedPullback {S : Scheme} {T U : SchemeBaseChange S} (R : SchemeKFlatResolution (CategoryTheory.Over.left U)) (f : T ⟶ U) (hR : KFlatPullbackAcyclic R f) (hqc : KFlatResolvedPullbackPreservesQuasicoherentCohomology R f) : DqcLeftDerivedPullback f

A pullback-acyclic K-flat replacement whose resolved pullback preserves quasicoherence constructs the actual Dqc left-derived pullback used by base change.

Equations

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

def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.KFlatResolvedPullbackPreservesCompactObjects {S : Scheme} {T U : SchemeBaseChange S} (R : SchemeKFlatResolution (CategoryTheory.Over.left U)) (f : T ⟶ U) (hqc : KFlatResolvedPullbackPreservesQuasicoherentCohomology R f) : Prop

Compactness preservation stated only for resolved representatives of compact Dqc(U) objects.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.kFlatDqcLeftDerivedPullback_preservesCompactObjects {S : Scheme} {T U : SchemeBaseChange S} (R : SchemeKFlatResolution (CategoryTheory.Over.left U)) (f : T ⟶ U) (hR : KFlatPullbackAcyclic R f) (hqc : KFlatResolvedPullbackPreservesQuasicoherentCohomology R f) (hcompact : KFlatResolvedPullbackPreservesCompactObjects R f hqc) : (kFlatDqcLeftDerivedPullback R f hR hqc).PreservesCompactObjects

Compactness preservation for the constructed Dqc left-derived pullback follows from its resolved representative-level form.