First strict short exact sequence in an owner thin interval #
Failure of skewed semistability produces a proper strict subobject of larger phase. Strict-Artinian descent then terminates at a semistable strict subobject, yielding the first strict short exact sequence used by the owner maximal-destabilizing-quotient construction.
@[simp]
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.subobject_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)
:
An interval subobject is zero exactly when it is the bottom subobject.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.subobject_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}
(hB : B ≠ ⊥)
:
A non-bottom interval subobject is nonzero.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.subobject_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 Y : Slicing.IntervalCat C s a b}
(f : Y ⟶ X)
(hf : IsStrictMono f)
:
The canonical arrow of the subobject represented by a strict mono is strict.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.strictShortExact_cokernel
(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 := ⋯ }
A strict mono and its canonical cokernel projection form a strict short exact sequence.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.isAdmissibleSubobject_of_isStrictSubobject
(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)]
{E : Slicing.IntervalCat C s a b}
(A : Subobject E)
(hA : IsStrictSubobject A)
:
Every owner strict subobject of a thin slicing interval is intrinsically
admissible. Together with
Slicing.IntervalCat.isStrictSubobject_of_isAdmissible, this identifies the
two subobject orders used by local finiteness and strict HN recursion.
def
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.admissibleStrictSubobjectOrderIso
(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)]
(E : Slicing.IntervalCat C s a b)
:
Intrinsic admissible subobjects and owner strict subobjects are the same ordered type in a thin slicing interval.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.isStrictFiniteLength_of_isFiniteLength
(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)]
{E : Slicing.IntervalCat C s a b}
(hE : Slicing.IsFiniteLength C s E)
:
Intrinsic local finite length supplies the strict finite length required by owner HN recursion.
noncomputable def
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.liftSub
(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 back to the ambient interval object by composing the two canonical arrows.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.liftSub_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.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.liftSub_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.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.liftSub_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.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.liftSub_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}
{M : Subobject X}
(hM : IsStrictMono M.arrow)
{A : Subobject (Subobject.underlying.obj M)}
(hA : IsStrictMono A.arrow)
:
IsStrictMono (liftSub C M A).arrow
Strictness is preserved when a strict subobject of a strict subobject is lifted to the ambient interval object.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.phase_liftSub
(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 : SkewedStabilityFunction C κ s a b}
{X : Slicing.IntervalCat C s a b}
(M : Subobject X)
(A : Subobject (Subobject.underlying.obj M))
:
Lifting a subobject does not change the underlying skewed phase.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.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 Λ]
{κ : K₀ C →+ Λ}
{σ : StabilityCondition.WithClassMap C κ}
{a b : ℝ}
{F : SkewedStabilityFunction C κ σ.slicing a b}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X : Slicing.IntervalCat C σ.slicing a b}
(hX : ¬Limits.IsZero X)
(hCharge : ∀ {E : C}, Slicing.intervalProp C σ.slicing a b E → ¬Limits.IsZero E → F.ChargeNe E)
(hns : ¬F.IsSemistable X.obj (F.phase X.obj))
:
Failure of skewed semistability supplies a proper strict subobject of strictly larger skewed phase.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.exists_first_strictShortExact_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 Λ]
{κ : K₀ C →+ Λ}
{σ : StabilityCondition.WithClassMap C κ}
{a b : ℝ}
{F : SkewedStabilityFunction C κ σ.slicing a b}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X : Slicing.IntervalCat C σ.slicing a b}
[IsStrictArtinianObject X]
(hX : ¬Limits.IsZero X)
(hns : ¬F.IsSemistable X.obj (F.phase X.obj))
(hCharge : ∀ {E : C}, Slicing.intervalProp C σ.slicing a b E → ¬Limits.IsZero E → F.ChargeNe E)
:
∃ (M : Subobject X),
M ≠ ⊥ ∧ M ≠ ⊤ ∧ IsStrictMono M.arrow ∧ F.IsSemistable (Subobject.underlying.obj M).obj (F.phase (Subobject.underlying.obj M).obj) ∧ F.phase X.obj < F.phase (Subobject.underlying.obj M).obj ∧ StrictShortExact
{ X₁ := Subobject.underlying.obj M, X₂ := X, X₃ := Limits.cokernel M.arrow, f := M.arrow,
g := Limits.cokernel.π M.arrow, zero := ⋯ }
Strict-Artinian descent terminates at a proper nonzero semistable strict subobject of strictly larger phase, together with its canonical strict short exact sequence.