Deformation of Stability Conditions — IntervalSelection #
Thin-interval selection, subobject lifting, finite length
Thin-interval Phase 3 selection infrastructure #
@[simp]
theorem
CategoryTheory.Triangulated.intervalSubobject_isZero_iff_eq_bot
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{s : Slicing C}
{a b : ℝ}
{X : Slicing.IntervalCat C s a b}
(B : Subobject X)
:
theorem
CategoryTheory.Triangulated.intervalSubobject_not_isZero_of_ne_bot
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{s : Slicing C}
{a b : ℝ}
{X : Slicing.IntervalCat C s a b}
{B : Subobject X}
(h : B ≠ ⊥)
:
theorem
CategoryTheory.Triangulated.intervalSubobject_top_ne_bot_of_not_isZero
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{s : Slicing C}
{a b : ℝ}
{X : Slicing.IntervalCat C s a b}
(hX : ¬Limits.IsZero X)
:
theorem
CategoryTheory.Triangulated.intervalSubobject_arrow_strictMono_of_strictMono
(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)]
{X Y : Slicing.IntervalCat C s a b}
(f : Y ⟶ X)
(hf : IsStrictMono f)
:
theorem
CategoryTheory.Triangulated.interval_strictShortExact_cokernel_of_strictMono
(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)]
{X Y : Slicing.IntervalCat C s a b}
(f : Y ⟶ X)
(hf : IsStrictMono f)
:
StrictShortExact { X₁ := Y, X₂ := X, X₃ := Limits.cokernel f, f := f, g := Limits.cokernel.π f, zero := ⋯ }
theorem
CategoryTheory.Triangulated.intervalInclusion_map_strictMono
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s₁ s₂ : Slicing C}
{a₁ b₁ a₂ b₂ : ℝ}
[Fact (a₁ < b₁)]
[Fact (b₁ - a₁ ≤ 1)]
[Fact (a₂ < b₂)]
[Fact (b₂ - a₂ ≤ 1)]
(h : Slicing.intervalProp C s₁ a₁ b₁ ≤ Slicing.intervalProp C s₂ a₂ b₂)
{X Y : Slicing.IntervalCat C s₁ a₁ b₁}
(f : X ⟶ Y)
(hf : IsStrictMono f)
:
IsStrictMono ((ObjectProperty.ιOfLE h).map f)
theorem
CategoryTheory.Triangulated.interval_strictArtinianObject_of_inclusion
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s₁ s₂ : Slicing C}
{a₁ b₁ a₂ b₂ : ℝ}
[Fact (a₁ < b₁)]
[Fact (b₁ - a₁ ≤ 1)]
[Fact (a₂ < b₂)]
[Fact (b₂ - a₂ ≤ 1)]
(h : Slicing.intervalProp C s₁ a₁ b₁ ≤ Slicing.intervalProp C s₂ a₂ b₂)
{X : Slicing.IntervalCat C s₁ a₁ b₁}
[IsArtinianObject ((ObjectProperty.ιOfLE h).obj X)]
:
theorem
CategoryTheory.Triangulated.interval_strictNoetherianObject_of_inclusion
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s₁ s₂ : Slicing C}
{a₁ b₁ a₂ b₂ : ℝ}
[Fact (a₁ < b₁)]
[Fact (b₁ - a₁ ≤ 1)]
[Fact (a₂ < b₂)]
[Fact (b₂ - a₂ ≤ 1)]
(h : Slicing.intervalProp C s₁ a₁ b₁ ≤ Slicing.intervalProp C s₂ a₂ b₂)
{X : Slicing.IntervalCat C s₁ a₁ b₁}
[IsNoetherianObject ((ObjectProperty.ιOfLE h).obj X)]
:
theorem
CategoryTheory.Triangulated.interval_strictFiniteLength_of_inclusion
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s₁ s₂ : Slicing C}
{a₁ b₁ a₂ b₂ : ℝ}
[Fact (a₁ < b₁)]
[Fact (b₁ - a₁ ≤ 1)]
[Fact (a₂ < b₂)]
[Fact (b₂ - a₂ ≤ 1)]
(h : Slicing.intervalProp C s₁ a₁ b₁ ≤ Slicing.intervalProp C s₂ a₂ b₂)
{X : Slicing.IntervalCat C s₁ a₁ b₁}
[IsArtinianObject ((ObjectProperty.ιOfLE h).obj X)]
[IsNoetherianObject ((ObjectProperty.ιOfLE h).obj X)]
:
theorem
CategoryTheory.Triangulated.interval_thinFiniteLength_of_inclusion
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s₁ s₂ : Slicing C}
{a₁ b₁ a₂ b₂ : ℝ}
[Fact (a₁ < b₁)]
[Fact (b₁ - a₁ ≤ 1)]
[Fact (a₂ < b₂)]
[Fact (b₂ - a₂ ≤ 1)]
(h : Slicing.intervalProp C s₁ a₁ b₁ ≤ Slicing.intervalProp C s₂ a₂ b₂)
(hFinite : ∀ (Y : Slicing.IntervalCat C s₂ a₂ b₂), IsArtinianObject Y ∧ IsNoetherianObject Y)
(X : Slicing.IntervalCat C s₁ a₁ b₁)
:
theorem
CategoryTheory.Triangulated.interval_strictArtinianObject_of_inclusion_strict
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s₁ s₂ : Slicing C}
{a₁ b₁ a₂ b₂ : ℝ}
[Fact (a₁ < b₁)]
[Fact (b₁ - a₁ ≤ 1)]
[Fact (a₂ < b₂)]
[Fact (b₂ - a₂ ≤ 1)]
(h : Slicing.intervalProp C s₁ a₁ b₁ ≤ Slicing.intervalProp C s₂ a₂ b₂)
{X : Slicing.IntervalCat C s₁ a₁ b₁}
[IsStrictArtinianObject ((ObjectProperty.ιOfLE h).obj X)]
:
theorem
CategoryTheory.Triangulated.interval_strictNoetherianObject_of_inclusion_strict
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s₁ s₂ : Slicing C}
{a₁ b₁ a₂ b₂ : ℝ}
[Fact (a₁ < b₁)]
[Fact (b₁ - a₁ ≤ 1)]
[Fact (a₂ < b₂)]
[Fact (b₂ - a₂ ≤ 1)]
(h : Slicing.intervalProp C s₁ a₁ b₁ ≤ Slicing.intervalProp C s₂ a₂ b₂)
{X : Slicing.IntervalCat C s₁ a₁ b₁}
[IsStrictNoetherianObject ((ObjectProperty.ιOfLE h).obj X)]
:
theorem
CategoryTheory.Triangulated.interval_strictFiniteLength_of_inclusion_strict
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s₁ s₂ : Slicing C}
{a₁ b₁ a₂ b₂ : ℝ}
[Fact (a₁ < b₁)]
[Fact (b₁ - a₁ ≤ 1)]
[Fact (a₂ < b₂)]
[Fact (b₂ - a₂ ≤ 1)]
(h : Slicing.intervalProp C s₁ a₁ b₁ ≤ Slicing.intervalProp C s₂ a₂ b₂)
{X : Slicing.IntervalCat C s₁ a₁ b₁}
[IsStrictArtinianObject ((ObjectProperty.ιOfLE h).obj X)]
[IsStrictNoetherianObject ((ObjectProperty.ιOfLE h).obj X)]
:
theorem
CategoryTheory.Triangulated.interval_thinFiniteLength_of_inclusion_strict
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s₁ s₂ : Slicing C}
{a₁ b₁ a₂ b₂ : ℝ}
[Fact (a₁ < b₁)]
[Fact (b₁ - a₁ ≤ 1)]
[Fact (a₂ < b₂)]
[Fact (b₂ - a₂ ≤ 1)]
(h : Slicing.intervalProp C s₁ a₁ b₁ ≤ Slicing.intervalProp C s₂ a₂ b₂)
(hFinite : ∀ (Y : Slicing.IntervalCat C s₂ a₂ b₂), IsStrictArtinianObject Y ∧ IsStrictNoetherianObject Y)
(X : Slicing.IntervalCat C s₁ a₁ b₁)
:
theorem
CategoryTheory.Triangulated.SectorFiniteLength.of_wide
(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 Λ]
{v : K₀ C →+ Λ}
(σ : StabilityCondition.WithClassMap C v)
{ε₀ : ℝ}
(hε₀ : 0 < ε₀)
(hε₀2 : ε₀ < 1 / 4)
(hε₀8 : ε₀ < 1 / 8)
(hWide : WideSectorFiniteLength C σ ε₀ hε₀ hε₀8)
:
SectorFiniteLength C σ ε₀ hε₀ hε₀2
theorem
CategoryTheory.Triangulated.interval_K0_of_strictMono
(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 Λ]
{v : K₀ C →+ Λ}
{s : Slicing C}
{a b : ℝ}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X Y : Slicing.IntervalCat C s a b}
(f : Y ⟶ X)
(hf : IsStrictMono f)
:
theorem
CategoryTheory.Triangulated.interval_card_subobject_lt_of_ne_top
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{s : Slicing C}
{a b : ℝ}
{X : Slicing.IntervalCat C s a b}
{M : Subobject X}
(hM : M ≠ ⊤)
[Finite (Subobject X)]
:
noncomputable def
CategoryTheory.Triangulated.intervalLiftSub
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{s : Slicing C}
{a b : ℝ}
{X : Slicing.IntervalCat C s a b}
(M : Subobject X)
(A : Subobject (Subobject.underlying.obj M))
:
Lift a subobject of an interval subobject M back to a subobject of the ambient
interval object X by composing the two defining arrows.
Equations
Instances For
theorem
CategoryTheory.Triangulated.intervalLiftSub_le
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{s : Slicing C}
{a b : ℝ}
{X : Slicing.IntervalCat C s a b}
(M : Subobject X)
(A : Subobject (Subobject.underlying.obj M))
:
theorem
CategoryTheory.Triangulated.intervalLiftSub_bot
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{s : Slicing C}
{a b : ℝ}
{X : Slicing.IntervalCat C s a b}
(M : Subobject X)
:
theorem
CategoryTheory.Triangulated.intervalLiftSub_ne_bot
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{s : Slicing C}
{a b : ℝ}
{X : Slicing.IntervalCat C s a b}
(M : Subobject X)
{A : Subobject (Subobject.underlying.obj M)}
(hA : A ≠ ⊥)
:
theorem
CategoryTheory.Triangulated.intervalLiftSub_mono
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{s : Slicing C}
{a b : ℝ}
{X : Slicing.IntervalCat C s a b}
(M : Subobject X)
{A B : Subobject (Subobject.underlying.obj M)}
(h : A ≤ B)
:
theorem
CategoryTheory.Triangulated.intervalLiftSub_lt
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{s : Slicing C}
{a b : ℝ}
{X : Slicing.IntervalCat C s a b}
(M : Subobject X)
{A : Subobject (Subobject.underlying.obj M)}
(hA : A ≠ ⊤)
:
theorem
CategoryTheory.Triangulated.intervalSubobject_bot_arrow_strictMono
(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)]
{X : Slicing.IntervalCat C s a b}
:
theorem
CategoryTheory.Triangulated.intervalLiftSub_arrow_strictMono_of_strictMono
(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)]
{X : Slicing.IntervalCat C s a b}
{M : Subobject X}
(hM : IsStrictMono M.arrow)
{A : Subobject (Subobject.underlying.obj M)}
(hA : IsStrictMono A.arrow)
:
IsStrictMono (intervalLiftSub C M A).arrow
theorem
CategoryTheory.Triangulated.intervalLiftSub_wPhase_eq
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{v : K₀ C →+ Λ}
{s : Slicing C}
{a b : ℝ}
{ssf : SkewedStabilityFunction C v s a b}
{X : Slicing.IntervalCat C s a b}
(M : Subobject X)
(A : Subobject (Subobject.underlying.obj M))
:
ssf.wPhase (Subobject.underlying.obj (intervalLiftSub C M A)).obj = ssf.wPhase (Subobject.underlying.obj A).obj
theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_phase_gt_strictSubobject_of_not_semistable
(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 Λ]
{v : K₀ C →+ Λ}
(σ : StabilityCondition.WithClassMap C v)
{a b : ℝ}
{ssf : SkewedStabilityFunction C v σ.slicing a b}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X : Slicing.IntervalCat C σ.slicing a b}
(hX : ¬Limits.IsZero X)
(hW_interval : ∀ {F : C}, Slicing.intervalProp C σ.slicing a b F → ¬Limits.IsZero F → ssf.wNe F)
(hns : ¬Semistable C ssf X.obj (ssf.wPhase X.obj))
:
A non-semistable thin-interval object contains a proper strict subobject of strictly larger
W-phase. This is the paper-faithful first step in Bridgeland's descent argument: the witness
is extracted directly from the failure of the semistability triangle test, not by finite
enumeration of subobjects.
noncomputable def
CategoryTheory.Triangulated.intervalLiftSubCokernelIso
(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)]
{X : Slicing.IntervalCat C s a b}
(M : Subobject X)
{A B : Subobject (Subobject.underlying.obj M)}
(h : A ≤ B)
:
Limits.cokernel ((intervalLiftSub C M A).ofLE (intervalLiftSub C M B) ⋯) ≅ Limits.cokernel (A.ofLE B h)
The quotient induced by a lifted subobject morphism is canonically identified with the quotient of the original subobject morphism inside the smaller interval object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_minPhase_maximal_strictKernel
(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 Λ]
{v : K₀ C →+ Λ}
(σ : StabilityCondition.WithClassMap C v)
{a b : ℝ}
{ssf : SkewedStabilityFunction C v σ.slicing a b}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X : Slicing.IntervalCat C σ.slicing a b}
(hX : ¬Limits.IsZero X)
(hW_interval : ∀ {F : C}, Slicing.intervalProp C σ.slicing a b F → ¬Limits.IsZero F → ssf.wNe F)
(hns : ¬Semistable C ssf X.obj (ssf.wPhase X.obj))
[Finite (Subobject X)]
:
∃ (M : Subobject X),
M ≠ ⊤ ∧ IsStrictMono M.arrow ∧ (∀ (B : Subobject X),
B ≠ ⊤ →
IsStrictMono B.arrow →
ssf.wPhase (Limits.cokernel M.arrow).obj ≤ ssf.wPhase (Limits.cokernel B.arrow).obj) ∧ ∀ (B : Subobject X),
B ≠ ⊤ →
IsStrictMono B.arrow →
M < B → ssf.wPhase (Limits.cokernel M.arrow).obj < ssf.wPhase (Limits.cokernel B.arrow).obj
Among the proper strict kernels of a non-semistable interval object, there is one whose
strict quotient has minimal W-phase, and among those minimal-phase kernels we may choose one
that is maximal for inclusion. This is the quotient-recursion selection step for Phase 3.
theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_minPhase_minimal_strictKernel
(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 Λ]
{v : K₀ C →+ Λ}
(σ : StabilityCondition.WithClassMap C v)
{a b : ℝ}
{ssf : SkewedStabilityFunction C v σ.slicing a b}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X : Slicing.IntervalCat C σ.slicing a b}
(hX : ¬Limits.IsZero X)
(hW_interval : ∀ {F : C}, Slicing.intervalProp C σ.slicing a b F → ¬Limits.IsZero F → ssf.wNe F)
(hns : ¬Semistable C ssf X.obj (ssf.wPhase X.obj))
[Finite (Subobject X)]
:
∃ (M : Subobject X),
M ≠ ⊤ ∧ IsStrictMono M.arrow ∧ (∀ (B : Subobject X),
B ≠ ⊤ →
IsStrictMono B.arrow →
ssf.wPhase (Limits.cokernel M.arrow).obj ≤ ssf.wPhase (Limits.cokernel B.arrow).obj) ∧ ∀ (B : Subobject X),
B ≠ ⊤ →
IsStrictMono B.arrow →
B < M → ssf.wPhase (Limits.cokernel M.arrow).obj < ssf.wPhase (Limits.cokernel B.arrow).obj
Among the proper strict kernels of a non-semistable interval object, there is one whose
strict quotient has minimal W-phase, and among the kernels achieving that minimal quotient
phase we may choose one that is minimal for inclusion. This is the mdq-oriented selection
step needed to force strict phase drop in the kernel recursion.
theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_maxPhase_maximal_strictSubobject_of_finite
(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 Λ]
{v : K₀ C →+ Λ}
(σ : StabilityCondition.WithClassMap C v)
{a b : ℝ}
{ssf : SkewedStabilityFunction C v σ.slicing a b}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X : Slicing.IntervalCat C σ.slicing a b}
(hX : ¬Limits.IsZero X)
(hT_fin : {B : Subobject X | B ≠ ⊥ ∧ IsStrictMono B.arrow}.Finite)
:
∃ (M : Subobject X),
M ≠ ⊥ ∧ IsStrictMono M.arrow ∧ (∀ (B : Subobject X),
B ≠ ⊥ →
IsStrictMono B.arrow →
ssf.wPhase (Subobject.underlying.obj B).obj ≤ ssf.wPhase (Subobject.underlying.obj M).obj) ∧ ∀ (B : Subobject X),
IsStrictMono B.arrow →
M < B → ssf.wPhase (Subobject.underlying.obj B).obj < ssf.wPhase (Subobject.underlying.obj M).obj
Among the nonzero strict subobjects of a thin-interval object, there is one with maximal W-phase, and among those maximal-phase candidates we may choose one that is maximal for inclusion. This is the strict-subobject selection step needed for the thin-interval HN recursion.
theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.exists_maxPhase_maximal_strictSubobject
(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 Λ]
{v : K₀ C →+ Λ}
(σ : StabilityCondition.WithClassMap C v)
{a b : ℝ}
{ssf : SkewedStabilityFunction C v σ.slicing a b}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X : Slicing.IntervalCat C σ.slicing a b}
(hX : ¬Limits.IsZero X)
[Finite (Subobject X)]
:
∃ (M : Subobject X),
M ≠ ⊥ ∧ IsStrictMono M.arrow ∧ (∀ (B : Subobject X),
B ≠ ⊥ →
IsStrictMono B.arrow →
ssf.wPhase (Subobject.underlying.obj B).obj ≤ ssf.wPhase (Subobject.underlying.obj M).obj) ∧ ∀ (B : Subobject X),
IsStrictMono B.arrow →
M < B → ssf.wPhase (Subobject.underlying.obj B).obj < ssf.wPhase (Subobject.underlying.obj M).obj
Among the nonzero strict subobjects of a thin-interval object, there is one with maximal W-phase, and among those maximal-phase candidates we may choose one that is maximal for inclusion. This is the strict-subobject selection step needed for the thin-interval HN recursion.
theorem
CategoryTheory.Triangulated.SkewedStabilityFunction.semistable_of_maxPhase_strictSubobject
(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 Λ]
{v : K₀ C →+ Λ}
(σ : StabilityCondition.WithClassMap C v)
{a b : ℝ}
{ssf : SkewedStabilityFunction C v σ.slicing a b}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X : Slicing.IntervalCat C σ.slicing a b}
{M : Subobject X}
(hM_ne : M ≠ ⊥)
(hM_strict : IsStrictMono M.arrow)
(hM_max :
∀ (B : Subobject X),
B ≠ ⊥ →
IsStrictMono B.arrow → ssf.wPhase (Subobject.underlying.obj B).obj ≤ ssf.wPhase (Subobject.underlying.obj M).obj)
(hW_interval : ∀ {F : C}, Slicing.intervalProp C σ.slicing a b F → ¬Limits.IsZero F → ssf.wNe F)
:
Semistable C ssf (Subobject.underlying.obj M).obj (ssf.wPhase (Subobject.underlying.obj M).obj)
A nonzero strict subobject that is maximal for W-phase among all nonzero strict subobjects is W-semistable.