Target-envelope transport for owner skewed semistability #
The existential interval in the owner deformed predicate is auxiliary. This file proves that a semistability witness can be read in every other thin old phase interval which contains the object and envelops the recorded phase.
noncomputable def
CategoryTheory.Triangulated.Slicing.IntervalCat.isLimitKernelForkOfDistinguished
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s : Slicing C}
{a b : ℝ}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{S : ShortComplex (IntervalCat C s a b)}
{δ : S.X₃.obj ⟶ (shiftFunctor C 1).obj S.X₁.obj}
(hT : Pretriangulated.Triangle.mk S.f.hom S.g.hom δ ∈ Pretriangulated.distinguishedTriangles)
:
The first map of a distinguished triangle inside a thin owner interval is a kernel of the second map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedSemistable_of_target_triangleTest
(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₁ a₂ b₂ ε ψ : ℝ}
(hab₁ : a₁ < b₁)
(hab₂ : a₂ < b₂)
(hε : 0 < ε)
(hthin₂ : b₂ - a₂ + 2 * ε < 1)
(ha₂ψ : a₂ + ε ≤ ψ)
(hψb₂ : ψ ≤ b₂ - ε)
{E : C}
(hI₂ : Slicing.intervalProp C σ.slicing a₂ b₂ E)
(hSS :
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab₁).IsSemistable
E ψ)
(htri :
∀ ⦃K Q : C⦄ ⦃i : K ⟶ E⦄ ⦃q : E ⟶ Q⦄ ⦃δ : Q ⟶ (shiftFunctor C 1).obj K⦄,
Pretriangulated.Triangle.mk i q δ ∈ Pretriangulated.distinguishedTriangles →
Slicing.intervalProp C σ.slicing a₂ b₂ K →
Slicing.intervalProp C σ.slicing a₂ b₂ Q →
¬Limits.IsZero K →
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1
hW hab₂).phase
K ≤ ψ)
:
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab₂).IsSemistable
E ψ
Repackage a source semistability proof once the target interval tests have been discharged.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.phase_add_lt_of_le_of_lt
(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 →+ Λ}
{s : Slicing C}
{a b : ℝ}
(F : WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction C κ s a b)
{X Y K : C}
{ψ : ℝ}
(hsum : F.charge X + F.charge Y = F.charge K)
(hXle : F.phase X ≤ ψ)
(hYlt : F.phase Y < ψ)
(hYne : F.ChargeNe Y)
(hXrange : F.phase X ∈ Set.Ioo (ψ - 1) (ψ + 1))
(hYrange : F.phase Y ∈ Set.Ioo (ψ - 1) (ψ + 1))
(hKrange : F.phase K ∈ Set.Ioo (ψ - 1) (ψ + 1))
:
If two summands have phases at most ψ, one strictly so, their sum has
phase strictly below ψ, provided all selected phases use the same branch.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.phase_seesaw_dual
(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 →+ Λ}
{s : Slicing C}
{a b : ℝ}
(F : WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction C κ s a b)
{E E₁ E₂ : C}
{ψ : ℝ}
(hsum : F.charge E₁ + F.charge E₂ = F.charge E)
(hψ : F.phase E = ψ)
(hE₁gt : ψ < F.phase E₁)
(hE₁ne : F.ChargeNe E₁)
(hE₁range : F.phase E₁ ∈ Set.Ioo (ψ - 1) (ψ + 1))
(hE₂range : F.phase E₂ ∈ Set.Ioo (ψ - 1) (ψ + 1))
:
The dual strict phase see-saw, packaged for an owner skewed stability function.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedSemistable_of_lower_inclusion
(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ε4 : ε < 1 / 4)
(haψ : a₁ + ε ≤ ψ)
(hψb : ψ ≤ b - ε)
(hthin₂ : b - a₂ + 2 * ε < 1)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
{E : C}
(hSS :
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
ha₁).IsSemistable
E ψ)
:
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
ha₂).IsSemistable
E ψ
Lowering the left endpoint of a thin interval preserves owner skewed semistability.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedSemistable_of_upper_inclusion
(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ε4 : ε < 1 / 4)
(haψ : a + ε ≤ ψ)
(hψb : ψ ≤ b₁ - ε)
(hthin₂ : b₂ - a + 2 * ε < 1)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
{E : C}
(hSS :
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab₁).IsSemistable
E ψ)
:
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab₂).IsSemistable
E ψ
Raising the right endpoint of a thin interval preserves owner skewed semistability.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedSemistable_of_interval_inclusion
(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₁ b₂ ψ ε : ℝ}
(hab₁ : a₁ < b₁)
(hab₂ : a₂ < b₂)
(ha : a₂ ≤ a₁)
(hb : b₁ ≤ b₂)
(hε : 0 < ε)
(hε4 : ε < 1 / 4)
(haψ : a₁ + ε ≤ ψ)
(hψb : ψ ≤ b₁ - ε)
(hthin₂ : b₂ - a₂ + 2 * ε < 1)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
{E : C}
(hSS :
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab₁).IsSemistable
E ψ)
:
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab₂).IsSemistable
E ψ
Enlarging both endpoints of a thin interval preserves owner skewed semistability.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedSemistable_of_target_subinterval
(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₁ a₂ b₂ b₁ ψ ε : ℝ}
(hab₁ : a₁ < b₁)
(hab₂ : a₂ < b₂)
(ha : a₁ ≤ a₂)
(hb : b₂ ≤ b₁)
{E : C}
(hI₂ : Slicing.intervalProp C σ.slicing a₂ b₂ E)
(hε : 0 < ε)
(hε4 : ε < 1 / 4)
(haψ : a₂ + ε ≤ ψ)
(hψb : ψ ≤ b₂ - ε)
(hthin₁ : b₁ - a₁ + 2 * ε < 1)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
(hSS :
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab₁).IsSemistable
E ψ)
:
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab₂).IsSemistable
E ψ
Restricting a semistability presentation to a nested target interval that still envelops its phase preserves owner skewed semistability.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.skewedSemistable_of_target_envelope
(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₁ b₂ ψ ε : ℝ}
(hab₁ : a₁ < b₁)
(hab₂ : a₂ < b₂)
{E : C}
(hI₂ : Slicing.intervalProp C σ.slicing a₂ b₂ E)
(hε : 0 < ε)
(hε4 : ε < 1 / 4)
(ha₁ψ : a₁ + ε ≤ ψ)
(hψb₁ : ψ ≤ b₁ - ε)
(ha₂ψ : a₂ + ε ≤ ψ)
(hψb₂ : ψ ≤ b₂ - ε)
(hthin₁ : b₁ - a₁ + 2 * ε < 1)
(hthin₂ : b₂ - a₂ + 2 * ε < 1)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
(hSS :
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab₁).IsSemistable
E ψ)
:
(WeakStabilityCondition.StabilityCondition.Deformation.skewedStabilityFunctionOfSeminormLtOne C σ W hr0 hr1 hW
hab₂).IsSemistable
E ψ
A semistability witness transports to every other thin old interval containing the object and enveloping the same recorded phase.
theorem
CategoryTheory.Triangulated.StabilityCondition.WithClassMap.hom_eq_zero_of_deformedPred
(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)
{ε : ℝ}
(hε : 0 < ε)
(hε2 : ε ≤ 1 / 2)
(hε8 : ε < 1 / 8)
(hsin :
WeakStabilityCondition.StabilityCondition.Deformation.stabilitySeminorm C σ (W - σ.Z) < ENNReal.ofReal (Real.sin (Real.pi * ε)))
{E F : C}
{ψ₁ ψ₂ : ℝ}
(hE : deformedPred C σ W hr0 hr1 hW ε ψ₁ E)
(hF : deformedPred C σ W hr0 hr1 hW ε ψ₂ F)
(hgap : ψ₂ < ψ₁)
(f : E ⟶ F)
:
Sharp owner Hom-vanishing for deformed slices, with target-envelope transport discharged internally.