Direct image on bounded coherent derived categories #
Definition 3.1 of arXiv:2607.28411v1 pulls a stability condition on Dᵇ(Y)
back along a proper morphism f : X → Y through the direct image
f_* : Dᵇ(X) ⥤ Dᵇ(Y). This file supplies that functor on the genuine
bounded coherent derived fibers of scheme base changes, in the shape in which
BoundedGeometry.lean supplies the inverse image f^*.
The contract HasCoherentPushforward f records what a morphism must provide:
an exact pushforward on coherent sheaves that forgets to module-sheaf
pushforward. Unlike HasCoherentPullback, it carries no derived functor as
a field. An exact functor between abelian categories induces its derived
functor degreewise, so coherentDerivedPushforward is Mathlib's
Functor.mapDerivedCategory, and boundedness, the shift, and the triangulated
structure are theorems (mapDerivedCategory_bounded and Mathlib's instances)
rather than obligations of the instance.
Finite morphisms between locally Noetherian schemes inhabit the contract
through Coh.pushforward, closed immersions among them; this is the generality
in which Proposition 3.3 of the paper and Definition 3.1 of arXiv:2601.22994
use f_*.
The contract is stated on an arbitrary morphism so that a further inhabitant,
an affine morphism whose pushforward preserves coherence, is an addition rather
than a rewrite.
Main definitions #
SchemeBaseChange.HasCoherentPushforward: the exact coherent pushforward contract.SchemeBaseChange.coherentDerivedPushforwardandSchemeBaseChange.boundedCoherentDerivedPushforward:f_*onD(Coh)and onDᵇ(Coh).SchemeBaseChange.hasCoherentPushforwardOfIsFinite: finite morphisms inhabit the contract.
Main results #
SchemeBaseChange.coherentDerivedPushforward_bounded:f_*preserves bounded complexes.SchemeBaseChange.boundedCoherentDerivedPushforwardCompInclusionwith theCommShiftandIsTriangulatedinstances: the bounded restriction is a triangulated functor.
Implementation notes #
Identity and composition laws for boundedCoherentDerivedPushforward are in
Families/CoherentPushforwardCoherence.lean, proved for every instance of
the contract from the comparison isomorphism.
(f ≫ g).left is definitionally f.left ≫ g.left but not reducibly so, hence
Mathlib's composition instance for IsFinite does not reach it;
isFinite_comp_left restates it in the form instance search meets, so that
hasCoherentPushforwardOfIsFinite fires on a composite of finite morphisms.
The contract keeps the sheaf-level functor as data, as HasCoherentPushforward's
mirror HasCoherentPullback does, although the comparison isomorphism
determines it up to isomorphism: an instance may then supply a functor
computed differently from the literal lift through Coh.ι, with only the
comparison to prove. Additivity is derived from the comparison isomorphism
and faithfulness of Coh.ι rather than taken as a field.
References #
- arXiv:2607.28411v1, Definition 3.1, Remark 3.2, and Proposition 3.3.
- arXiv:2601.22994, Definition 3.1.
The geometric data needed to restrict module-sheaf pushforward to coherent
sheaves: an exact functor on coherent sheaves that forgets to module-sheaf
pushforward. Exactness is the whole contract; it is what lets the derived
direct image be computed degreewise and preserve bounded objects. Along a
proper morphism that is not affine, f_* is only left exact on coherent
sheaves and the derived direct image is not degreewise; such a morphism does
not inhabit this class, and Definition 3.1 of arXiv:2607.28411v1 in that
generality needs a right-derived functor the repository does not own.
- sheafPushforward : CategoryTheory.Functor (Coh (CategoryTheory.Over.left T)) (Coh (CategoryTheory.Over.left U))
Pushforward on coherent sheaves.
- preservesFiniteLimits : CategoryTheory.Limits.PreservesFiniteLimits (sheafPushforward f)
Coherent pushforward preserves finite limits.
- preservesFiniteColimits : CategoryTheory.Limits.PreservesFiniteColimits (sheafPushforward f)
Coherent pushforward preserves finite colimits.
- comparison : (sheafPushforward f).comp (Coh.ι (CategoryTheory.Over.left U)) ≅ (Coh.ι (CategoryTheory.Over.left T)).comp (modulePushforward f)
After forgetting coherence, this is ordinary module-sheaf pushforward.
Instances
Coherent pushforward is additive. Reflected through the faithful additive
inclusion Coh.ι from additivity of module-sheaf pushforward, using the
comparison isomorphism; Functor.mapDerivedCategory asks for additivity
separately from exactness, and this discharges it for every instance.
The direct image f_* on unbounded coherent derived categories: the
degreewise derived functor of the exact coherent pushforward.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Mathlib's Functor.mapDerivedCategoryFactors under the geometric name, so
a caller computing f_* on a complex rewrites here instead of unfolding
coherentDerivedPushforward.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The shift on the derived direct image is Mathlib's, supplied by name: after unfolding the
def, instance search would still not see through the wrapper (see
.claude/references/instance-transparency.md), and the triangulated instance below needs this
one to be Mathlib's term, not a re-derivation, to unify at all.
Equations
- One or more equations did not get rendered due to their size.
The derived direct image preserves canonical boundedness, because an exact functor applied degreewise preserves strict complex bounds.
The direct image f_* : Dᵇ(Coh X) ⥤ Dᵇ(Coh Y) of Definition 3.1 of
arXiv:2607.28411v1, restricted from the unbounded direct image through
coherentDerivedPushforward_bounded.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The bounded lift forgets to the unbounded direct image. This is the
isomorphism isTriangulated_iff_comp_right pivots on: the triangulated
structure on Dᵇ(Coh) is inherited through it rather than re-proved.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A composite of finite morphisms of scheme base changes has finite
underlying morphism. Stated on (f ≫ g).left, the spelling instance search
meets, because that projection only unfolds to f.left ≫ g.left at default
transparency.
Finite morphisms between locally Noetherian schemes inhabit the contract:
Coh.pushforward is exact and lands in coherent sheaves, and its comparison
with module-sheaf pushforward is Coh.pushforwardCompι, an Iso.refl, so
nothing is transported. Closed immersions are finite (Mathlib's instance), so
this covers Theorem 6.2 of arXiv:2607.28411v1, which constructs stability
conditions on a projective scheme X as the pullbacks ι^♯σ along a closed
embedding ι : X ↪ Pⁿ of stability conditions σ on Pⁿ, as well as the
finite morphisms of Propositions 3.3 and 3.24, both stated for finite
morphisms between noetherian schemes, and of Definition 3.1 of
arXiv:2601.22994.
Equations
- One or more equations did not get rendered due to their size.