The abstract Bayer property

The geometric literature writes the Bayer property for tensoring by a line bundle and shifting by an integer. At the abstract slicing layer, the tensor operation is simply a chosen autoequivalence action, while the shift is a phase translation. Keeping those two inputs explicit avoids importing a scheme or pretending that AutQuot C is literally tensor by a line bundle.

Quantifier order

HasBayerProperty s q l fixes one slicing s, one quotient autoequivalence q, and one integer l, and asserts the single comparison

s ≼ (q • s).phaseShift l.

There is no existential quantifier over the twist or the integer. This is the quantifier order of arXiv:2607.28411v1, Definition 3.16; the geometric instantiation q = - ⊗ L remains outside this repository.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.HasBayerProperty {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (q : AutQuot C) (l : ℤ) : Prop

The abstract Bayer property for a slicing, a chosen autoequivalence, and an integer phase shift.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.SlicingBayerProperty {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (q : AutQuot C) (l : ℤ) : Prop

Explicit name for the slicing-level abstraction.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.hasBayerProperty_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) (q : AutQuot C) (l : ℤ) : HasBayerProperty s q l ↔ Slicing.PrecedesWeak C s (Slicing.phaseShift C (q • s) ↑l)

Unfold the abstract Bayer property to its defining slicing comparison.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.hasBayerProperty_one_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (s : Slicing C) : HasBayerProperty s 1 0

The identity autoequivalence with zero phase shift satisfies the Bayer property by reflexivity of the weak slicing order.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.hasBayerProperty_smul_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (r q : AutQuot C) (s : Slicing C) (l : ℤ) : HasBayerProperty (r • s) (r * q * r⁻¹) l ↔ HasBayerProperty s q l

Bayer's property is invariant under simultaneous autoequivalence transport, with the twist conjugated by the transporting element.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.BayerProperty {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Lambda : Type u'} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : StabilityCondition.WithClassMap C v) (q : AutPairQuot v) (l : ℤ) : Prop

The paper-facing Bayer property for a class-map stability condition and a chosen compatible autoequivalence. The lattice component of q moves the charge; its underlying autoequivalence moves the slicing.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.bayerProperty_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Lambda : Type u'} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : StabilityCondition.WithClassMap C v) (q : AutPairQuot v) (l : ℤ) : BayerProperty sigma q l ↔ HasBayerProperty sigma.slicing (AutPairQuot.toAutQuot q) l

Express the paper-facing Bayer property through the reusable slicing-level predicate and the forgetful homomorphism to AutQuot.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.bayerProperty_iff_phiPlus_le {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Lambda : Type u'} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : StabilityCondition.WithClassMap C v) (q : AutPairQuot v) (l : ℤ) : BayerProperty sigma q l ↔ ∀ {E : C} {phi : ℝ}, sigma.slicing.P phi E → ∀ (hE0 : ¬Limits.IsZero E), Slicing.phiPlus C (Slicing.phaseShift C (q • sigma).slicing ↑l) E hE0 ≤ phi

Upper-phase formulation of the paper-facing Bayer property. For an object semistable in the original slicing, its highest phase in the acted and shifted slicing is at most its original phase.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.bayerProperty_iff_le_phiMinus {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Lambda : Type u'} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : StabilityCondition.WithClassMap C v) (q : AutPairQuot v) (l : ℤ) : BayerProperty sigma q l ↔ ∀ {E : C} {phi : ℝ}, (Slicing.phaseShift C (q • sigma).slicing ↑l).P phi E → ∀ (hE0 : ¬Limits.IsZero E), phi ≤ Slicing.phiMinus C sigma.slicing E hE0

Lower-phase formulation of the paper-facing Bayer property. For an object semistable in the acted and shifted slicing, its lowest phase in the original slicing is at least its acted phase.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.bayerProperty_mk_iff_inverse_phiPlus_le {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Lambda : Type u'} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : StabilityCondition.WithClassMap C v) (a : AutPair v) (l : ℤ) : BayerProperty sigma (AutPairQuot.mk a) l ↔ ∀ {E : C} {phi : ℝ}, sigma.slicing.P phi E → ∀ (hInv0 : ¬Limits.IsZero (a.Φ.e.inverse.obj E)), Slicing.phiPlus C sigma.slicing (a.Φ.e.inverse.obj E) hInv0 ≤ phi + ↑l

Lemma 3.17(2) at the representative level. The inverse object map appears explicitly because a.Φ is a chosen autoequivalence rather than only its natural-isomorphism class. The phase shift [-l] in the paper has been moved to the right-hand side of the inequality.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.bayerProperty_mk_iff_inverse_le_phiMinus {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Lambda : Type u'} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : StabilityCondition.WithClassMap C v) (a : AutPair v) (l : ℤ) : BayerProperty sigma (AutPairQuot.mk a) l ↔ ∀ {E : C} {phi : ℝ}, sigma.slicing.P (phi + ↑l) (a.Φ.e.inverse.obj E) → ∀ (hE0 : ¬Limits.IsZero E), phi ≤ Slicing.phiMinus C sigma.slicing E hE0

Preimage form of Lemma 3.17(3). Semistability for the acted and shifted slicing is rewritten as semistability of the inverse image in the original slicing; the conclusion is the corresponding original lowest-phase bound.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.bayerProperty_mk_iff_sub_le_functor_phiMinus {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Lambda : Type u'} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : StabilityCondition.WithClassMap C v) (a : AutPair v) (l : ℤ) : BayerProperty sigma (AutPairQuot.mk a) l ↔ ∀ {F : C} {phi : ℝ}, sigma.slicing.P phi F → ∀ (hMap0 : ¬Limits.IsZero (a.Φ.e.functor.obj F)), phi - ↑l ≤ Slicing.phiMinus C sigma.slicing (a.Φ.e.functor.obj F) hMap0

Lemma 3.17(3) at the representative level. For an original semistable object, the lowest phase of its forward image is bounded below by phi - l. Equivalently, shifting that image by [l] gives the paper's inequality phiMinus (a.Φ(F)[l]) ≥ phi.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.bayerProperty_one_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] {Lambda : Type u'} [AddCommGroup Lambda] {v : K₀ C →+ Lambda} (sigma : StabilityCondition.WithClassMap C v) : BayerProperty sigma 1 0

The identity compatible autoequivalence with zero phase shift satisfies the paper-facing Bayer property.