Equivariance of the slicing orders

Both slicing orders are invariant under simultaneous transport by a triangulated autoequivalence. The result is first proved for a representative TriEquiv and then descends to the repository's honest quotient group AutQuot C.

Phase bounds under transport

theorem CategoryTheory.Triangulated.Slicing.mapEquiv_ltProp_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Phi : C ≌ C) [Phi.functor.Additive] [Phi.inverse.Additive] [Phi.functor.CommShift ℤ] [Phi.inverse.CommShift ℤ] [Phi.functor.IsTriangulated] [Phi.inverse.IsTriangulated] (s : Slicing C) (phi : ℝ) (E : C) : ltProp C (s.mapEquiv Phi) phi E ↔ ltProp C s phi (Phi.inverse.obj E)

Transport by an equivalence relabels objects but leaves the strict upper phase bound unchanged.

theorem CategoryTheory.Triangulated.Slicing.mapEquiv_leProp_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Phi : C ≌ C) [Phi.functor.Additive] [Phi.inverse.Additive] [Phi.functor.CommShift ℤ] [Phi.inverse.CommShift ℤ] [Phi.functor.IsTriangulated] [Phi.inverse.IsTriangulated] (s : Slicing C) (phi : ℝ) (E : C) : leProp C (s.mapEquiv Phi) phi E ↔ leProp C s phi (Phi.inverse.obj E)

Transport by an equivalence relabels objects but leaves the weak upper phase bound unchanged.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.TriEquiv.precedes_act_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Phi : TriEquiv C) (s t : Slicing C) : Slicing.Precedes C (Phi.act s) (Phi.act t) ↔ Slicing.Precedes C s t

Simultaneous transport by a triangulated autoequivalence preserves and reflects the strict slicing order.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.TriEquiv.precedesWeak_act_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (Phi : TriEquiv C) (s t : Slicing C) : Slicing.PrecedesWeak C (Phi.act s) (Phi.act t) ↔ Slicing.PrecedesWeak C s t

Simultaneous transport by a triangulated autoequivalence preserves and reflects the weak slicing order.

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

The quotient autoequivalence action preserves the strict slicing order.

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

The quotient autoequivalence action preserves the weak slicing order.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.smul_slicing {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) (q : AutPairQuot v) (sigma : StabilityCondition.WithClassMap C v) : (q • sigma).slicing = toAutQuot q • sigma.slicing

Forgetting the compatible lattice automorphism turns the AutPairQuot action's underlying slicing into the AutQuot action.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.precedes_smul_stability_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) (q : AutPairQuot v) (sigma tau : StabilityCondition.WithClassMap C v) : Slicing.Precedes C (q • sigma).slicing (q • tau).slicing ↔ Slicing.Precedes C sigma.slicing tau.slicing

The AutPairQuot action on stability conditions preserves the strict slicing order. The compatible class-lattice datum affects the charge but not this comparison of the underlying slicings.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.GroupAction.AutPairQuot.precedesWeak_smul_stability_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) (q : AutPairQuot v) (sigma tau : StabilityCondition.WithClassMap C v) : Slicing.PrecedesWeak C (q • sigma).slicing (q • tau).slicing ↔ Slicing.PrecedesWeak C sigma.slicing tau.slicing

The AutPairQuot action on stability conditions preserves the weak slicing order.