Shift equivariance of owner deformed phase cuts

Shifting an object by one translates its owner deformed phase by one. The same operation preserves the provisional extension-closed cuts after translating their cutoff.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_shift_one (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε ψ : ℝ} {X : C} (h : deformedPred C σ W hr0 hr1 hW ε ψ X) : deformedPred C σ W hr0 hr1 hW ε (ψ + 1) ((shiftFunctor C 1).obj X)

Forward shift for the owner deformed predicate.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_of_shift_one (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε ψ : ℝ} {X : C} (h : deformedPred C σ W hr0 hr1 hW ε (ψ + 1) ((shiftFunctor C 1).obj X)) : deformedPred C σ W hr0 hr1 hW ε ψ X

Converse to forward shift for the owner deformed predicate.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedPred_shift_neg_one (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε ψ : ℝ} {X : C} (h : deformedPred C σ W hr0 hr1 hW ε ψ X) : deformedPred C σ W hr0 hr1 hW ε (ψ - 1) ((shiftFunctor C (-1)).obj X)

Backward shift for the owner deformed predicate.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred_shift_one (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε t : ℝ} {X : C} (hX : deformedGtPred C σ W hr0 hr1 hW ε t X) : deformedGtPred C σ W hr0 hr1 hW ε (t + 1) ((shiftFunctor C 1).obj X)

Forward shift preserves the provisional cut Q(>t).

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred_shift_neg_one (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε t : ℝ} {X : C} (hX : deformedGtPred C σ W hr0 hr1 hW ε t X) : deformedGtPred C σ W hr0 hr1 hW ε (t - 1) ((shiftFunctor C (-1)).obj X)

Backward shift preserves the provisional cut Q(>t).

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred_shift_one (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε t : ℝ} {X : C} (hX : deformedLePred C σ W hr0 hr1 hW ε t X) : deformedLePred C σ W hr0 hr1 hW ε (t + 1) ((shiftFunctor C 1).obj X)

Forward shift preserves the provisional cut Q(≤t).

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred_shift_neg_one (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε t : ℝ} {X : C} (hX : deformedLePred C σ W hr0 hr1 hW ε t X) : deformedLePred C σ W hr0 hr1 hW ε (t - 1) ((shiftFunctor C (-1)).obj X)

Backward shift preserves the provisional cut Q(≤t).

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred_shift_one (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε t : ℝ} {X : C} (hX : deformedLtPred C σ W hr0 hr1 hW ε t X) : deformedLtPred C σ W hr0 hr1 hW ε (t + 1) ((shiftFunctor C 1).obj X)

Forward shift preserves the provisional cut Q(<t).

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred_shift_neg_one (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] {κ : K₀ C →+ Λ} (σ : WithClassMap C κ) (W : Λ →+ ℂ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) (hW : WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) ≤ ENNReal.ofReal r) {ε t : ℝ} {X : C} (hX : deformedLtPred C σ W hr0 hr1 hW ε t X) : deformedLtPred C σ W hr0 hr1 hW ε (t - 1) ((shiftFunctor C (-1)).obj X)

Backward shift preserves the provisional cut Q(<t).