Boundary transport for owner skewed semistability #
Boundary truncations detect when a skewed-semistable object already belongs to a one-sided smaller target interval. The owner semistability predicate tests distinguished triangles directly, so no quasi-abelian strictness layer is needed for these reductions.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedPhase_mem_enveloped_branch
(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)
{a b ε ψ : ℝ}
(hab : a < b)
(hε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hthin : b - a + 2 * ε < 1)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
(haψ : a + ε ≤ ψ)
(hψb : ψ ≤ b - ε)
{E : C}
(hI : Slicing.intervalProp C σ.slicing a b E)
(hE : ¬Limits.IsZero E)
:
A thin interval object has phase in the unit branch centred at any enveloped skewed-semistable phase.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedPhase_gt_of_geProp_of_phase_range
(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)
{a b ε ψ : ℝ}
(hab : a < b)
(hε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hthin : b - a + 2 * ε < 1)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
{E : C}
(hI : Slicing.intervalProp C σ.slicing a b E)
(hE : ¬Limits.IsZero E)
(hrange :
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).phase
E ∈ Set.Ioo (ψ - 1) (ψ + 1))
(hbranch : b + ε < ψ + 1)
(hge : Slicing.geProp C σ.slicing (ψ + ε) E)
:
ψ < (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).phase
E
A nonzero interval object supported at or above ψ + ε has skewed
phase above ψ whenever its selected phase lies on the same branch as
ψ. This range-based form is what the highest-phase split recursion uses
before an enveloping interval has been established.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedPhase_gt_of_geProp
(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)
{a b ε ψ : ℝ}
(hab : a < b)
(hε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hthin : b - a + 2 * ε < 1)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
(haψ : a + ε ≤ ψ)
(hψb : ψ ≤ b - ε)
{E : C}
(hI : Slicing.intervalProp C σ.slicing a b E)
(hE : ¬Limits.IsZero E)
(hge : Slicing.geProp C σ.slicing (ψ + ε) E)
:
ψ < (WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).phase
E
A nonzero thin interval object supported at or above ψ + ε has
skewed phase strictly above ψ.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedPhase_lt_of_leProp
(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)
{a b ε ψ : ℝ}
(hab : a < b)
(hε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hthin : b - a + 2 * ε < 1)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
(haψ : a + ε ≤ ψ)
(hψb : ψ ≤ b - ε)
{E : C}
(hI : Slicing.intervalProp C σ.slicing a b E)
(hE : ¬Limits.IsZero E)
(hle : Slicing.leProp C σ.slicing (ψ - ε) E)
:
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab).phase
E < ψ
A nonzero thin interval object supported at or below ψ - ε has
skewed phase strictly below ψ.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.intervalProp_of_skewedSemistable_upper_target
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated 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)
{a b₁ b₂ ε ψ : ℝ}
(hab₁ : a < b₁)
(hab₂ : a < b₂)
(hb : b₁ ≤ b₂)
(hε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hthin : b₂ - a + 2 * ε < 1)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
(haψ : a + ε ≤ ψ)
(hψb : ψ ≤ b₁ - ε)
{E : C}
(hSS :
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab₂).IsSemistable
E ψ)
:
Slicing.intervalProp C σ.slicing a b₁ E
Skewed semistability excludes an upper-boundary piece above the recorded phase, so the object belongs to the smaller upper target interval.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.intervalProp_of_skewedSemistable_lower_target
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated 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)
{a₁ a₂ b ε ψ : ℝ}
(ha₁ : a₁ < b)
(ha₂ : a₂ < b)
(ha : a₁ ≤ a₂)
(hε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hthin : b - a₁ + 2 * ε < 1)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
(haψ : a₂ + ε ≤ ψ)
(hψb : ψ ≤ b - ε)
{E : C}
(hSS :
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
ha₁).IsSemistable
E ψ)
:
Slicing.intervalProp C σ.slicing a₂ b E
Skewed semistability excludes a lower-boundary quotient below the recorded phase, so the object belongs to the smaller lower target interval.