Equivariance of preimage transfer #
Preimage transfer commutes with compatible autoequivalences. Compatibility is
the natural isomorphism one obtains by passing an equivariant geometric
functor through the inverse representatives used by Slicing.mapEquiv.
Slicing.PreimageData.mapEquiv shows that the lifting witness itself
transports along compatible autoequivalences, so the twisted preimage slicing
exists whenever the untwisted one does. Together with
Slicing.preimage_mapEquiv this is Lemma 3.5(1) and Lemma 3.9(1) of
arXiv:2607.28411v1 in full, and Lemma 3.2 of arXiv:2601.22994:
f^β―(π« β L) = f^β―π« β f^*L and the left-hand side is a slicing.
preimage along F is f^β― when F is a direct image and f_β― when F
is a pullback (PreStabilityCondition.WithClassMap.pullback and
pushforward); both readings of every statement below are intended.
Main definitions #
AutPair.preimage: the compatible class-lattice datum of a target pair, transported to the class mapv β Kβ(F)of the transferred condition.
Main results #
Slicing.preimage_mapEquiv: transfer commutes with compatible autoequivalences of slicings, given a lifting witness for the twisted slicing.Slicing.PreimageData.mapEquivandSlicing.PreimageData.preimage_mapEquiv: that witness is not an extra input; it transports along the twist.AutPair.preimage_act: the charge-carrying form,AutPair.actcommutes withStabilityCondition.WithClassMap.preimage.
References #
- arXiv:2607.28411v1, Lemmas 3.5(1) and 3.9(1).
- arXiv:2601.22994, Lemma 3.2.
Preimage transfer commutes with compatible triangulated
autoequivalences. The compatibility is stated for inverse functors because
Slicing.mapEquiv defines membership by applying the inverse representative.
The lifting witness transports along compatible autoequivalences: the
twisted preimage collection is a slicing whenever the untwisted one is. This
is the existence half of Lemma 3.5(1) and Lemma 3.9(1) of arXiv:2607.28411v1,
which Slicing.preimage_mapEquiv had to assume.
Hom-vanishing is pulled back through the faithful inverse PhiC.inverse, and
an HN filtration for the twisted collection is obtained by filtering
PhiC.inverse.obj E for the untwisted one, pushing through PhiC.functor,
and landing on E by the counit, exactly as in Slicing.mapEquiv itself.
Slicing.preimage_mapEquiv with the transported witness: the twisted
preimage slicing is the twist of the preimage slicing, and it exists. This is
the complete statement of Lemma 3.5(1) and Lemma 3.9(1) of arXiv:2607.28411v1
and of Lemma 3.2 of arXiv:2601.22994 at the level of slicings.
Representative-level AutPairQuot compatibility for preimage transfer.
This theorem is intentionally about representatives aC and aD: quotient
descent additionally requires the geometric transfer data to be independent
of representatives, which is a property of the eventual family functors.
The compatible lattice datum of a target pair transports to the
transferred class map v β Kβ(F): the same lam works, because the
intertwining isomorphism identifies Kβ(F) β Kβ(PhiCβ»ΒΉ) with
Kβ(PhiDβ»ΒΉ) β Kβ(F). This is what lets an autoequivalence of the source
act on transferred stability conditions with charges, not only on their
slicings.
Unrelated to AutPair.preimage_representatives, which is the slicing-level
equality stated for two independent representatives and does not use this
construction.
Instances For
The transported pair acts on the source through the chosen twist.
Definitional; recorded for simp.
The transported pair keeps the lattice automorphism of the original.
Definitional; recorded for simp.
Transfer commutes with the autoequivalence action on stability
conditions. Acting by aD and then transferring along F is the same as
transferring and then acting by the transported pair. The slicing half is
Slicing.PreimageData.preimage_mapEquiv; the charge half is definitional,
since both sides carry Z β lam. This is Lemma 3.2 of arXiv:2601.22994 with
its central charges, in the orientation of the Lean statement:
f_β―(Ο β f^*L) = (f_β―Ο) β L.