Identity and composition for the bounded coherent direct image

The direct image f_* : Dᵇ(Coh X) ⥤ Dᵇ(Coh Y) of Families/CoherentPushforward.lean is pseudofunctorial: along an identity it is the identity, and along a composite it is the composite, up to natural isomorphism. This file proves both for every instance of HasCoherentPushforward, at the three levels the direct image is built in.

Main definitions

• SchemeBaseChange.HasCoherentPushforward.sheafPushforwardId and SchemeBaseChange.HasCoherentPushforward.sheafPushforwardComp: on coherent sheaves, from the contract's comparison isomorphism and Mathlib's Modules.pushforwardId and pushforwardComp, lifted through the fully faithful Coh.ι.
• SchemeBaseChange.coherentDerivedPushforwardId and coherentDerivedPushforwardComp: on D(Coh), through the pseudofunctoriality of Functor.mapDerivedCategory.
• SchemeBaseChange.boundedCoherentDerivedPushforwardId and boundedCoherentDerivedPushforwardComp: on Dᵇ(Coh), lifted through the fully faithful DerivedCategory.Bounded.ι.

Implementation notes

As on the pullback side (Families/CoherentPullbackCoherence.lean), nothing here is assumed: the contract's comparison isomorphism determines the coherent pushforward up to isomorphism, so the laws are theorems about every instance. The consumer is Stability/BoundedCoherentPullback.lean, where they give the identity and composition laws of the f^♯ witnesses.

Each lift through a fully faithful functor is Functor.fullyFaithfulCancelRight, applied to an isomorphism assembled from the comparison isomorphisms and associators; nothing is computed on sections or on complexes.

The triangle and pentagon coherence equations between these isomorphisms are not stated, as they are not for pullback.

References

• arXiv:2607.28411v1, Definition 3.1; the laws are what make (f ≫ g)^♯ = f^♯ ∘ g^♯ and 𝟙^♯ = 𝟙 meaningful for the pullback of stability conditions.

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

Coherent pushforward along an identity is the identity, for every instance of the contract: the comparison isomorphism reads it as module-sheaf pushforward along 𝟙, which is Modules.pushforwardId, 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.HasCoherentPushforward.sheafPushforwardComp {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)] [HasCoherentPushforward f] [HasCoherentPushforward g] [HasCoherentPushforward (CategoryTheory.CategoryStruct.comp f g)] : (sheafPushforward f).comp (sheafPushforward g) ≅ sheafPushforward (CategoryTheory.CategoryStruct.comp f g)

The composite of two coherent pushforwards is the coherent pushforward along the composite, for every instance of the contract: three comparison isomorphisms and Modules.pushforwardComp identify both sides after Coh.ι, which cancels. The direction is that of Modules.pushforwardComp.

Equations

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

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

The derived direct image along an identity is the identity: transport sheafPushforwardId through mapDerivedCategory and use Functor.mapDerivedCategoryIdIso.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.coherentDerivedPushforwardComp {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)] [HasCoherentPushforward f] [HasCoherentPushforward g] [HasCoherentPushforward (CategoryTheory.CategoryStruct.comp f g)] : (coherentDerivedPushforward f).comp (coherentDerivedPushforward g) ≅ coherentDerivedPushforward (CategoryTheory.CategoryStruct.comp f g)

The composite of two derived direct images is the derived direct image along the composite: Functor.mapDerivedCategoryCompIso at the factorization sheafPushforwardComp, which is exactly the shape of derivedPullbackComp on the pullback side.

Equations

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

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

The bounded direct image along an identity is the identity, lifted through the fully faithful DerivedCategory.Bounded.ι from coherentDerivedPushforwardId.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.boundedCoherentDerivedPushforwardComp {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)] [HasCoherentPushforward f] [HasCoherentPushforward g] [HasCoherentPushforward (CategoryTheory.CategoryStruct.comp f g)] : (boundedCoherentDerivedPushforward f).comp (boundedCoherentDerivedPushforward g) ≅ boundedCoherentDerivedPushforward (CategoryTheory.CategoryStruct.comp f g)

The composite of two bounded direct images is the bounded direct image along the composite, lifted through the fully faithful DerivedCategory.Bounded.ι from coherentDerivedPushforwardComp and the three inclusion comparisons.

Equations

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