Coherent pullback preserves perfect complexes #

Every coherent pullback contract sends the finite locally free generators of the perfect objects to finite locally free generators, hence, by coherentDerivedPullback_preservesPerfect, every perfect complex to a perfect complex. The contract identifies its sheaf-level functor with module-sheaf pullback through comparison; module-sheaf pullback preserves fixed-rank locally free atlases along every morphism (FiniteLocallyFreeData.pullback); and the contract's derived pullback commutes with the degree-zero embedding through its factorization derivedFactors (Functor.singleFunctorIsoOfFactors). So perfect complexes are preserved by every instance of HasCoherentPullback, with no further hypothesis, and the perfect lift perfectDerivedPullback follows. Its identity and composition laws are in Families/CoherentPullbackCoherence.lean. No flatness enters.

Main definitions #

SchemeBaseChange.derivedPullbackSingleFunctor: the contract's derived pullback commutes with DerivedCategory.singleFunctor;
SchemeBaseChange.perfectDerivedPullback: pullback on perfect derived fibers;
SchemeBaseChange.perfectDerivedPullbackCompInclusion: the perfect lift forgets to coherent derived pullback.

Main results #

SchemeBaseChange.schemeFiniteLocallyFreeGenerator_le_inverseImage_coherentDerivedPullback: generators go to generators;
SchemeBaseChange.coherentDerivedPullback_preservesPerfect: every coherent pullback contract preserves perfect complexes.

References #

arXiv:2607.28411v1, Definition 3.6 and Proposition 3.8, whose pullback of stability conditions along a flat morphism is stated on Dᵇ(Coh) and restricts to perfect complexes; arXiv:2601.22994, Definition 3.1.

source

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.derivedPullbackSingleFunctor {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [HasCoherentPullback f] (n : ℤ) :

(DerivedCategory.singleFunctor (Coh (CategoryTheory.Over.left U)) n).comp (coherentDerivedPullback f) ≅ (HasCoherentPullback.sheafPullback f).comp (DerivedCategory.singleFunctor (Coh (CategoryTheory.Over.left T)) n)

The contract's derived pullback commutes with the degree-n embedding, through its factorization derivedFactors.

Equations

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

Instances For

source

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.schemeFiniteLocallyFreeGenerator_le_inverseImage_coherentDerivedPullback {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [HasCoherentPullback f] :

schemeFiniteLocallyFreeGenerator (CategoryTheory.Over.left U) ≤ (schemeFiniteLocallyFreeGenerator (CategoryTheory.Over.left T)).inverseImage (coherentDerivedPullback f)

Coherent pullback sends finite locally free generators to finite locally free generators: the atlas of F pulls back along f.left and is transported through comparison, and the derived pullback of the degree-zero object F is the degree-zero object of the pulled-back sheaf.

source

theorem AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.coherentDerivedPullback_preservesPerfect {S : Scheme} {T U : SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [HasCoherentPullback f] :

schemePerfect (CategoryTheory.Over.left U) ≤ (schemePerfect (CategoryTheory.Over.left T)).inverseImage (coherentDerivedPullback f)

Every coherent pullback contract preserves perfect complexes. Generators go to generators, which lie in the envelope, and a triangulated functor that sends the generators into a thick triangulated subcategory sends the whole envelope into it.

source