Identity and composition for coherent derived pullback

The contract HasCoherentPullback determines its functors up to isomorphism: the comparison isomorphism reads the sheaf-level pullback as module-sheaf pullback, and derivedFactors reads the derived pullback as degreewise sheaf-level pullback on complexes. So the identity and composition laws of the coherent, bounded coherent, and perfect derived pullbacks are theorems about every instance of the contract, the mirror image of Families/CoherentPushforwardCoherence.lean.

Main definitions

• SchemeBaseChange.HasCoherentPullback.sheafPullbackId and sheafPullbackComp: on Coh, from the comparison isomorphisms and modulePullbackId/modulePullbackComp, lifted through the fully faithful Coh.ι.
• SchemeBaseChange.coherentDerivedPullbackId and coherentDerivedPullbackComp: on D(Coh), by the universal property of the localization at the contract's factorization.
• SchemeBaseChange.boundedCoherentDerivedPullbackId and boundedCoherentDerivedPullbackComp: on Dᵇ(Coh), lifted through the fully faithful DerivedCategory.Bounded.ι.
• SchemeBaseChange.perfectDerivedPullbackId and perfectDerivedPullbackComp: on Perf, lifted through the fully faithful (schemePerfect _).ι.

Implementation notes

The derived pullback of the contract is data, not Functor.mapDerivedCategory of the sheaf pullback, so the derived laws cannot come from NatIso.mapDerivedCategory as on the pushforward side. They come from Localization.liftNatIso with the Lifting instances that the factorization supplies, packaged as DerivedCategory.isoOfFactors, DerivedCategory.idFactors, and DerivedCategory.compFactors in Algebra/Homology/DerivedCategory/ExactFunctor.lean. Each lift through a fully faithful functor is Functor.fullyFaithfulCancelRight, applied to an isomorphism assembled from the inclusion comparisons and associators; nothing is computed on sections or on complexes. The direction convention is that of modulePullbackComp: pullback g ⋙ pullback f ≅ pullback (f ≫ g).

The consumer is Stability/BoundedCoherentBaseChange.lean, where these give the identity and composition laws of the f^♯ witnesses. The triangle and pentagon coherence equations between the isomorphisms are not stated, as on the pushforward side.

References

• arXiv:2607.28411v1, Proposition 3.8 and the pseudofunctoriality it uses implicitly; arXiv:2601.22994, Definition 3.1.

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.HasCoherentPullback.sheafPullbackId {S : Scheme} (T : SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [HasCoherentPullback (CategoryTheory.CategoryStruct.id T)] : sheafPullback (CategoryTheory.CategoryStruct.id T) ≅ CategoryTheory.Functor.id (Coh (CategoryTheory.Over.left T))

Coherent pullback along an identity is the identity, for every instance of the contract: the comparison isomorphism reads it as module-sheaf pullback along 𝟙, which is modulePullbackId, and the fully faithful Coh.ι cancels.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.HasCoherentPullback.sheafPullbackComp {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [IsLocallyNoetherian (CategoryTheory.Over.left V)] [HasCoherentPullback f] [HasCoherentPullback g] [HasCoherentPullback (CategoryTheory.CategoryStruct.comp f g)] : (sheafPullback g).comp (sheafPullback f) ≅ sheafPullback (CategoryTheory.CategoryStruct.comp f g)

The composite of two coherent pullbacks is the coherent pullback along the composite, for every instance of the contract: three comparison isomorphisms and modulePullbackComp identify both sides after Coh.ι, which cancels.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.coherentDerivedPullbackId {S : Scheme} (T : SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [HasCoherentPullback (CategoryTheory.CategoryStruct.id T)] : coherentDerivedPullback (CategoryTheory.CategoryStruct.id T) ≅ CategoryTheory.Functor.id (SchemeCoherentDerivedCategory (CategoryTheory.Over.left T))

The coherent derived pullback along an identity is the identity: derivedFactors writes it as degreewise sheafPullback (𝟙 T), DerivedCategory.idFactors writes 𝟭 as degreewise 𝟭 (Coh T.left), and sheafPullbackId identifies the two sheaf-level functors, so DerivedCategory.isoOfFactors applies.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.coherentDerivedPullbackComp {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [IsLocallyNoetherian (CategoryTheory.Over.left V)] [HasCoherentPullback f] [HasCoherentPullback g] [HasCoherentPullback (CategoryTheory.CategoryStruct.comp f g)] : (coherentDerivedPullback g).comp (coherentDerivedPullback f) ≅ coherentDerivedPullback (CategoryTheory.CategoryStruct.comp f g)

The composite of two coherent derived pullbacks is the coherent derived pullback along the composite: the composite factors degreewise through the composite of the sheaf-level pullbacks, and sheafPullbackComp identifies that with the sheaf-level pullback along f ≫ g.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.boundedCoherentDerivedPullbackId {S : Scheme} (T : SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [HasCoherentPullback (CategoryTheory.CategoryStruct.id T)] : boundedCoherentDerivedPullback (CategoryTheory.CategoryStruct.id T) ≅ CategoryTheory.Functor.id T.BoundedCoherentDerivedFiber

The bounded coherent pullback along an identity is the identity, lifted through the fully faithful DerivedCategory.Bounded.ι from coherentDerivedPullbackId.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.boundedCoherentDerivedPullbackComp {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [IsLocallyNoetherian (CategoryTheory.Over.left V)] [HasCoherentPullback f] [HasCoherentPullback g] [HasCoherentPullback (CategoryTheory.CategoryStruct.comp f g)] : (boundedCoherentDerivedPullback g).comp (boundedCoherentDerivedPullback f) ≅ boundedCoherentDerivedPullback (CategoryTheory.CategoryStruct.comp f g)

The composite of two bounded coherent pullbacks is the bounded coherent pullback along the composite, lifted through the fully faithful DerivedCategory.Bounded.ι from coherentDerivedPullbackComp and the three inclusion comparisons.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.perfectDerivedPullbackId {S : Scheme} (T : SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [HasCoherentPullback (CategoryTheory.CategoryStruct.id T)] : perfectDerivedPullback (CategoryTheory.CategoryStruct.id T) ≅ CategoryTheory.Functor.id T.PerfectDerivedFiber

The perfect pullback along an identity is the identity, lifted through the fully faithful (schemePerfect _).ι from coherentDerivedPullbackId.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.perfectDerivedPullbackComp {S : Scheme} {T U V : SchemeBaseChange S} (f : T ⟶ U) (g : U ⟶ V) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [IsLocallyNoetherian (CategoryTheory.Over.left V)] [HasCoherentPullback f] [HasCoherentPullback g] [HasCoherentPullback (CategoryTheory.CategoryStruct.comp f g)] : (perfectDerivedPullback g).comp (perfectDerivedPullback f) ≅ perfectDerivedPullback (CategoryTheory.CategoryStruct.comp f g)

The composite of two perfect pullbacks is the perfect pullback along the composite, lifted through the fully faithful (schemePerfect _).ι from coherentDerivedPullbackComp and the three inclusion comparisons.

Equations

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