Pullback of stability conditions along bounded coherent direct image #
Definition 3.1(3) of arXiv:2607.28411v1 on the geometric object it is about.
For a morphism f : T ⟶ U of scheme base changes with an exact coherent
pushforward, a stability condition σ on Dᵇ(Coh U) whose slicing lifts
along f_* : Dᵇ(Coh T) ⥤ Dᵇ(Coh U) pulls back to f^♯σ on Dᵇ(Coh T),
with class map v ∘ f_* and unchanged charge. This is also the pullback
half of Definition 3.1 of arXiv:2601.22994, where f is a finite morphism
of smooth projective varieties; finite morphisms inhabit
HasCoherentPushforward through hasCoherentPushforwardOfIsFinite.
Main definitions #
SchemeBaseChange.BoundedCoherentPushforwardPreimageData: the explicit witness thatf_*detects a slicing, the conclusion of Proposition 3.3.SchemeBaseChange.BoundedCoherentPushforwardInducingData: the phase-indexed A.17 output forf_*, the form in which Proposition 3.3 delivers it.PreStabilityCondition.WithClassMap.boundedCoherentPullbackandStabilityCondition.WithClassMap.boundedCoherentPullback:f^♯σfrom an explicit witness.PreStabilityCondition.WithClassMap.boundedCoherentPullbackOfInducingand its stability-level twin:f^♯σfrom the A.17 output.
Main results #
SchemeBaseChange.BoundedCoherentPushforwardPreimageData.identity,comp,preimage_identity, andpreimage_comp: the witnesses along an identity and along a composite, and the slicings they produce.boundedCoherentPullback_slicing,boundedCoherentPullback_Z, andboundedCoherentPullback_charge, in both namespaces: the slicing off^♯σis the geometric preimage slicing, the charge onΛis unchanged, and the charge of an object is the charge of its direct image.
Implementation notes #
Every declaration here is the categorical preimage of
Phase/Transfer/PreStability.lean and Phase/Transfer/LocallyFinite.lean at
the functor boundedCoherentDerivedPushforward f; nothing geometric is
proved. Lemma 3.5(2) and (3) of arXiv:2607.28411v1, the extreme phases and
the slicing distance under f^♯, are therefore available through
PreStabilityCondition.WithClassMap.preimage_phiPlus and
slicingDist_preimage_le at this functor with no further work.
The witness structures carry the same identity and composition laws as
BoundedCoherentPullbackPreimageData, and on both sides the bounded
isomorphisms are theorems about every instance of the contract
(Families/CoherentPullbackCoherence.lean there,
Families/CoherentPushforwardCoherence.lean here). The composition law reads the two-step
transfer inside out: pull back along g first, then along f, and the
result is the transfer along f ≫ g.
The declarations stay in
CategoryTheory.Triangulated.{Pre,}StabilityCondition.WithClassMap so that
σ.boundedCoherentPullback f h is dot notation on the categorical carrier;
this is the geometric-realization row of Tier 2 in
docs/architecture/placement.md.
Proposition 3.3 itself, which produces the witness from condition (3.1) on
f_* 𝒪_X ⊗ −, is not proved here: its inputs are the Ind-extensions of the
standard slicings inside Dqc and the adjunction f^* ⊣ f_* on Dqc, the
same open geometric inputs as Proposition 3.8.
References #
- arXiv:2607.28411v1, Definition 3.1, Remark 3.2, Proposition 3.3, Lemma 3.5.
- arXiv:2601.22994, Definition 3.1.
Explicit preimage-slicing data for bounded coherent direct image along one
morphism of locally Noetherian scheme base changes: the two non-formal slicing
axioms for f_*. This is the conclusion of Proposition 3.3 of
arXiv:2607.28411v1, which this file consumes and does not prove. Kept as a
structure rather than an abbreviation so that the composition law can be added
beside BoundedCoherentPullbackPreimageData.comp without changing
consumers.
- preimageData : s.PreimageData (boundedCoherentDerivedPushforward f)
The two non-formal slicing axioms for the actual bounded coherent direct image.
Instances For
The pullback slicing f^♯𝒫 on the source fiber constructed from the
explicit witness: an object has phase φ exactly when its direct image
does.
Equations
Instances For
The identity direct image carries the identity witness, transported across
boundedCoherentDerivedPushforwardId.
The slicing pulled back along the identity is the original slicing.
Witnesses compose: a witness for g on s and a witness for f on the
slicing pulled back along g give a witness for f ≫ g on s, transported
across boundedCoherentDerivedPushforwardComp. The order of the two witnesses
is the order in which the transfers are applied, g first.
One-step and two-step pullbacks of a slicing agree.
The phase-indexed A.17 output for f_*, given its own name so that
Proposition 3.3 of arXiv:2607.28411v1 has a typed conclusion to deliver into;
toPreimageData is its only consumer.
- inducedTStructures : s.InducedTStructures (boundedCoherentDerivedPushforward f)
The induced source t-structures with the (A.8) recognition formulas.
Instances For
The identity direct image carries the inhabited identity A.17 model,
transported across boundedCoherentDerivedPushforwardId.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Apply the owned finite phase-truncation theorem to the actual A.17 output.
Definition 3.1(3) of arXiv:2607.28411v1 on Dᵇ(Coh): the pullback
f^♯σ of a pre-stability condition along the bounded coherent direct image
f_*, given the witness that f_* detects a slicing.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The slicing of f^♯σ is the geometric preimage slicing, so the
slicing-level API of Phase.Transfer.Basic applies to it verbatim.
Pullback leaves the central charge on Λ untouched; only the class map
changes. Definitional; recorded for simp.
The charge of an object for f^♯σ is the charge of its direct image for
σ, the geometric form of (f^♯Z)(E) = Z(f_* E).
f^♯σ from the phase-indexed A.17 output for the bounded coherent direct
image, the form in which Proposition 3.3 of arXiv:2607.28411v1 delivers the
slicing witness.
Equations
Instances For
Definition 3.1(3) of arXiv:2607.28411v1 on Dᵇ(Coh) for stability
conditions: f^♯σ is again a stability condition, by the categorical
local-finiteness transfer Slicing.PreimageData.isLocallyFinite. This is
the content of Remark 3.2: once f^♯𝒫 is a slicing, f^♯σ is a stability
condition with respect to (Λ, f^♯v).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The slicing of f^♯σ is the geometric preimage slicing, restated at the
stability-condition level so callers need not pass through the underlying
pre-stability condition.
Pullback leaves the central charge on Λ untouched. Definitional;
recorded for simp.
The charge of an object for f^♯σ is the charge of its direct image for
σ. Not a simp lemma: simp derives it from
StabilityCondition.WithClassMap.preimage_toWithClassMap and the
pre-stability preimage_charge, so it is recorded as the direct restatement
a caller can rw with.
f^♯σ for stability conditions from the phase-indexed A.17 output, the
form in which Proposition 3.3 of arXiv:2607.28411v1 delivers the slicing
witness; local finiteness travels by StabilityCondition.WithClassMap.preimage.