Triangulated closure of owner deformed phase cuts #
The owner deformed cuts are extension closed by construction. Their shift symmetry upgrades this to the rotated closure properties needed for the prospective deformed t-structure.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred_shift_one_same
(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 ((shiftFunctor C 1).obj X)
The cut Q(>t) is closed under forward shift without changing t.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred_shift_neg_one_same
(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 ((shiftFunctor C (-1)).obj X)
The cut Q(≤t) is closed under backward shift without changing t.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred_shift_neg_one_same
(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 ((shiftFunctor C (-1)).obj X)
The cut Q(<t) is closed under backward shift without changing t.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedGtPred_of_triangle_obj₃
(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 S Y : C}
{f : X ⟶ S}
{g : S ⟶ Y}
{h : Y ⟶ (shiftFunctor C 1).obj X}
(hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles)
(hX : deformedGtPred C σ W hr0 hr1 hW ε t X)
(hS : deformedGtPred C σ W hr0 hr1 hW ε t S)
:
deformedGtPred C σ W hr0 hr1 hW ε t Y
Q(>t) contains the third vertex when it contains the first two.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLePred_of_triangle_obj₁
(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 S Y : C}
{f : X ⟶ S}
{g : S ⟶ Y}
{h : Y ⟶ (shiftFunctor C 1).obj X}
(hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles)
(hS : deformedLePred C σ W hr0 hr1 hW ε t S)
(hY : deformedLePred C σ W hr0 hr1 hW ε t Y)
:
deformedLePred C σ W hr0 hr1 hW ε t X
Q(≤t) contains the first vertex when it contains the last two.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.deformedLtPred_of_triangle_obj₁
(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 S Y : C}
{f : X ⟶ S}
{g : S ⟶ Y}
{h : Y ⟶ (shiftFunctor C 1).obj X}
(hT : Pretriangulated.Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles)
(hS : deformedLtPred C σ W hr0 hr1 hW ε t S)
(hY : deformedLtPred C σ W hr0 hr1 hW ε t Y)
:
deformedLtPred C σ W hr0 hr1 hW ε t X
Q(<t) contains the first vertex when it contains the last two.