The Bayer property under transfer

Lemma 3.25 of arXiv:2607.28411v1 ends with the observation that the Bayer property of a slicing survives pullback: if 𝒫 ⪯ 𝒫 ⊗ L[l] on the target, then f^♯𝒫 ⪯ f^♯𝒫 ⊗ f^*L[l] on the source, "by Lemma 3.5(1) and Remark 3.14(3)". The same two ingredients give the pushforward statement. This file proves that observation at the categorical level, where the twist is a pair of compatible autoequivalences and the shift is a phase translation.

Main results

• HasBayerProperty.preimage: the slicing-level Bayer property transfers along a phase-detecting functor to the transported twist.
• BayerProperty.preimage: the same for stability conditions with class maps, the twist carried by AutPair.preimage.

Implementation notes

The proof is exactly the paper's: Slicing.PreimageData.preimage_mapEquiv (Lemma 3.5(1)) identifies the twist of the transferred slicing with the transfer of the twisted slicing, Slicing.preimage_phaseShift_self moves the phase translation through the transfer, and Slicing.PrecedesWeak.preimage_of_preimageData (Remark 3.14(3)) transports the weak order. No conservativity hypothesis is taken; the lifting witness supplies it.

Both theorems take a single lifting witness and are stated for representatives of the autoequivalence quotients. There is no family-wide form to distinguish them from, so they carry the plain name preimage rather than the preimage_of_preimageData of the order lemmas.

References

• arXiv:2607.28411v1, Lemma 3.5(1), Remark 3.14(3), Definition 3.16, Lemma 3.25.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.HasBayerProperty.preimage {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {s : Slicing D} {F : Functor C D} [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : s.PreimageData F) (PhiC : TriEquiv C) (PhiD : TriEquiv D) (alpha : F.comp PhiD.e.inverse ≅ PhiC.e.inverse.comp F) (l : ℤ) (hB : HasBayerProperty s (AutQuot.mk PhiD) l) : HasBayerProperty (s.preimage F h) (AutQuot.mk PhiC) l

The Bayer property survives transfer. If s ⪯ (PhiD • s)[l] on the target and PhiC is the compatible twist on the source, then the transferred slicing satisfies s_F ⪯ (PhiC • s_F)[l].

Geometrically this is both directions of Lemma 3.25 of arXiv:2607.28411v1: the pullback f^♯ of a slicing with the Bayer property for L has it for f^*L, and dually the pushforward f_♯ of a slicing with the Bayer property for f^*L has it for L. Which reading applies is fixed by whether F is a direct image or a pullback, as in PreStabilityCondition.WithClassMap.pullback and pushforward.

Stated for the representatives PhiC, PhiD rather than for classes in AutQuot: descent needs the intertwiner alpha to be independent of the representative, which is a property of the eventual family functors and is not available here, the same restriction as AutPair.preimage_representatives.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.BayerProperty.preimage {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [IsTriangulated C] [IsTriangulated D] {Λ : Type u'} [AddCommGroup Λ] {v : K₀ D →+ Λ} (σ : StabilityCondition.WithClassMap D v) {F : Functor C D} [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (h : σ.slicing.PreimageData F) (aD : AutPair v) (PhiC : TriEquiv C) (alpha : F.comp aD.Φ.e.inverse ≅ PhiC.e.inverse.comp F) (l : ℤ) (hB : BayerProperty σ (AutPairQuot.mk aD) l) : BayerProperty (σ.preimage F h) (AutPairQuot.mk (aD.preimage F PhiC alpha)) l

The paper-facing Bayer property of a stability condition transfers, with the twist carried across the class map by AutPair.preimage. Reduces to HasBayerProperty.preimage through bayerProperty_iff; the class-lattice component plays no role in the comparison of slicings. Stated for the representative aD rather than for q : AutPairQuot v, for the reason given at HasBayerProperty.preimage.