Strict maximal destabilizing quotients in owner thin intervals #
This module introduces the strict finite-length hypothesis and the witness structure used by the owner Harder--Narasimhan recursion. It remains on the Mathlib-only side of the ownership boundary.
def
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.ThinStrictFiniteLength
(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 : ℝ)
[Fact (a < b)]
[Fact (b - a ≤ 1)]
:
Every object of an owner thin interval is strict Artinian and strict Noetherian. This is the chain-condition hypothesis used by strict MDQ selection and the finite-length HN recursion.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.ThinStrictFiniteLength.of_finiteLength
(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 : ℝ}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
(h : ∀ (Y : Slicing.IntervalCat C σ.slicing a b), IsArtinianObject Y ∧ IsNoetherianObject Y)
:
ThinStrictFiniteLength C σ a b
Ordinary finite length of every thin-interval object implies owner strict finite length.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.exists_semistable_strictQuotient_le_phase
(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)]
(hFiniteLength : ThinStrictFiniteLength C σ a b)
(hCharge : ∀ {E : C}, Slicing.intervalProp C σ.slicing a b E → ¬Limits.IsZero E → F.ChargeNe E)
{L U : ℝ}
(hWindow : ∀ (Y : Slicing.IntervalCat C σ.slicing a b), ¬Limits.IsZero Y.obj → L < F.phase Y.obj ∧ F.phase Y.obj < U)
(hWidth : U - L < 1)
{X : Slicing.IntervalCat C σ.slicing a b}
(hX : ¬Limits.IsZero X)
:
∃ (M : Subobject X),
M ≠ ⊤ ∧ IsStrictMono M.arrow ∧ F.IsSemistable (Limits.cokernel M.arrow).obj (F.phase (Limits.cokernel M.arrow).obj) ∧ F.phase (Limits.cokernel M.arrow).obj ≤ F.phase X.obj
Strict-Noetherian induction selects a semistable strict quotient whose phase is no greater than that of the original nonzero object.
structure
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.IsStrictMDQ
(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 B : Slicing.IntervalCat C σ.slicing a b}
(q : X ⟶ B)
:
A strict maximal destabilizing quotient in an owner thin interval. Its phase is minimal among nonzero semistable strict quotients, and equality forces the competing quotient to factor through it.
- strictEpi : IsStrictEpi q
The quotient map is a strict epimorphism.
- nonzero : ¬Limits.IsZero B.obj
The quotient is nonzero as an ambient object.
- semistable : F.IsSemistable B.obj (F.phase B.obj)
The quotient is semistable at its skewed phase.
- minimal {B' : Slicing.IntervalCat C σ.slicing a b} (q' : X ⟶ B') : IsStrictEpi q' → ¬Limits.IsZero B'.obj → F.IsSemistable B'.obj (F.phase B'.obj) → F.phase B.obj ≤ F.phase B'.obj ∧ (F.phase B'.obj = F.phase B.obj → ∃ (t : B ⟶ B'), q' = CategoryStruct.comp q t)
The quotient has minimal phase, with the expected rigidity at equal phase.
Instances For
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.IsStrictMDQ.id_of_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}
{L U : ℝ}
(hWindow : ∀ (Y : Slicing.IntervalCat C σ.slicing a b), ¬Limits.IsZero Y.obj → L < F.phase Y.obj ∧ F.phase Y.obj < U)
(hWidth : U - L < 1)
(hss : F.IsSemistable X.obj (F.phase X.obj))
:
IsStrictMDQ C σ F (CategoryStruct.id X)
A semistable interval object is its own strict MDQ when every nonzero interval object has phase in a common window of width less than one.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.IsStrictMDQ.epi
(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 B : Slicing.IntervalCat C σ.slicing a b}
{q : X ⟶ B}
(hq : IsStrictMDQ C σ F q)
:
Epi q
A strict MDQ is epic.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.IsStrictMDQ.strict
(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 B : Slicing.IntervalCat C σ.slicing a b}
{q : X ⟶ B}
(hq : IsStrictMDQ C σ F q)
:
IsStrict q
A strict MDQ is strict.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.IsStrictMDQ.phase_le
(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 B : Slicing.IntervalCat C σ.slicing a b}
{q : X ⟶ B}
(hq : IsStrictMDQ C σ F q)
{B' : Slicing.IntervalCat C σ.slicing a b}
(q' : X ⟶ B')
(hq' : IsStrictEpi q')
(hB' : ¬Limits.IsZero B'.obj)
(hss : F.IsSemistable B'.obj (F.phase B'.obj))
:
The minimal-phase part of the strict MDQ universal property.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.IsStrictMDQ.factor_of_phase_eq
(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 B : Slicing.IntervalCat C σ.slicing a b}
{q : X ⟶ B}
(hq : IsStrictMDQ C σ F q)
{B' : Slicing.IntervalCat C σ.slicing a b}
(q' : X ⟶ B')
(hq' : IsStrictEpi q')
(hB' : ¬Limits.IsZero B'.obj)
(hss : F.IsSemistable B'.obj (F.phase B'.obj))
(hphase : F.phase B'.obj = F.phase B.obj)
:
∃ (t : B ⟶ B'), q' = CategoryStruct.comp q t
Equal phase forces a semistable strict quotient to factor through a strict MDQ.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.IsStrictMDQ.precomposeIso
(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 B : Slicing.IntervalCat C σ.slicing a b}
{q : X ⟶ B}
(hq : IsStrictMDQ C σ F q)
{X' : Slicing.IntervalCat C σ.slicing a b}
(e : X' ≅ X)
:
IsStrictMDQ C σ F (CategoryStruct.comp e.hom q)
Precomposing a strict MDQ by an isomorphism of source interval objects preserves its universal property.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.IsStrictMDQ.of_strictEpi_factor
(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 B : Slicing.IntervalCat C σ.slicing a b}
{q : X ⟶ B}
(hq : IsStrictMDQ C σ F q)
{Q : Slicing.IntervalCat C σ.slicing a b}
{p : X ⟶ Q}
(hp : IsStrictEpi p)
{π : Q ⟶ B}
(hfac : CategoryStruct.comp p π = q)
:
IsStrictMDQ C σ F π
If a strict MDQ factors through a strict epimorphism, then the induced quotient of the intermediate object is again a strict MDQ.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.IsStrictMDQ.phase_le_of_strictQuotient
(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 B : Slicing.IntervalCat C σ.slicing a b}
{q : X ⟶ B}
(hq : IsStrictMDQ C σ F q)
(hFiniteLength : ThinStrictFiniteLength C σ a b)
(hCharge : ∀ {E : C}, Slicing.intervalProp C σ.slicing a b E → ¬Limits.IsZero E → F.ChargeNe E)
{L U : ℝ}
(hWindow : ∀ (Y : Slicing.IntervalCat C σ.slicing a b), ¬Limits.IsZero Y.obj → L < F.phase Y.obj ∧ F.phase Y.obj < U)
(hWidth : U - L < 1)
{Q : Slicing.IntervalCat C σ.slicing a b}
(p : X ⟶ Q)
(hp : IsStrictEpi p)
(hQ : ¬Limits.IsZero Q.obj)
:
The phase of a strict MDQ is bounded above by the phase of every nonzero strict quotient, whether or not that quotient is already semistable.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.IsStrictMDQ.isSemistable_of_strictQuotient_phase_eq
(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 B : Slicing.IntervalCat C σ.slicing a b}
{q : X ⟶ B}
(hq : IsStrictMDQ C σ F q)
(hFiniteLength : ThinStrictFiniteLength C σ a b)
(hCharge : ∀ {E : C}, Slicing.intervalProp C σ.slicing a b E → ¬Limits.IsZero E → F.ChargeNe E)
{L U : ℝ}
(hWindow : ∀ (Y : Slicing.IntervalCat C σ.slicing a b), ¬Limits.IsZero Y.obj → L < F.phase Y.obj ∧ F.phase Y.obj < U)
(hWidth : U - L < 1)
{Q : Slicing.IntervalCat C σ.slicing a b}
(p : X ⟶ Q)
(hp : IsStrictEpi p)
(hQ : ¬Limits.IsZero Q.obj)
(hphase : F.phase Q.obj = F.phase B.obj)
:
F.IsSemistable Q.obj (F.phase Q.obj)
A nonzero strict quotient having the same phase as a strict MDQ is semistable.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.IsStrictMDQ.factor_of_strictQuotient_phase_eq
(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 B : Slicing.IntervalCat C σ.slicing a b}
{q : X ⟶ B}
(hq : IsStrictMDQ C σ F q)
(hFiniteLength : ThinStrictFiniteLength C σ a b)
(hCharge : ∀ {E : C}, Slicing.intervalProp C σ.slicing a b E → ¬Limits.IsZero E → F.ChargeNe E)
{L U : ℝ}
(hWindow : ∀ (Y : Slicing.IntervalCat C σ.slicing a b), ¬Limits.IsZero Y.obj → L < F.phase Y.obj ∧ F.phase Y.obj < U)
(hWidth : U - L < 1)
{Q : Slicing.IntervalCat C σ.slicing a b}
(p : X ⟶ Q)
(hp : IsStrictEpi p)
(hQ : ¬Limits.IsZero Q.obj)
(hphase : F.phase Q.obj = F.phase B.obj)
:
∃ (t : B ⟶ Q), p = CategoryStruct.comp q t
Equal phase forces every nonzero strict quotient to factor through the strict MDQ; semistability follows from the preceding theorem.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.IsStrictMDQ.comp_of_destabilizing_semistable_subobject
(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}
{A : Subobject X}
(hFiniteLength : ThinStrictFiniteLength C σ a b)
(hCharge : ∀ {E : C}, Slicing.intervalProp C σ.slicing a b E → ¬Limits.IsZero E → F.ChargeNe E)
{L U : ℝ}
(hWindow : ∀ (Y : Slicing.IntervalCat C σ.slicing a b), ¬Limits.IsZero Y.obj → L < F.phase Y.obj ∧ F.phase Y.obj < U)
(hWidth : U - L < 1)
{V : ℝ}
(hHom :
∀ {E G : Slicing.IntervalCat C σ.slicing a b},
F.IsSemistable E.obj (F.phase E.obj) →
F.IsSemistable G.obj (F.phase G.obj) → F.phase G.obj < F.phase E.obj → F.phase E.obj < V → ∀ (f : E ⟶ G), f = 0)
(hAss : F.IsSemistable (Subobject.underlying.obj A).obj (F.phase (Subobject.underlying.obj A).obj))
(hAstrict : IsStrictMono A.arrow)
(hAphase : F.phase X.obj < F.phase (Subobject.underlying.obj A).obj)
(hAtop : A ≠ ⊤)
(hAupper : F.phase (Subobject.underlying.obj A).obj < V)
{Q : Slicing.IntervalCat C σ.slicing a b}
{r : Limits.cokernel A.arrow ⟶ Q}
(hr : IsStrictMDQ C σ F r)
:
IsStrictMDQ C σ F (CategoryStruct.comp (Limits.cokernel.π A.arrow) r)
An MDQ of the quotient by a destabilizing semistable strict subobject composes to an MDQ of the original object.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.exists_strictMDQ
(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)]
(hFiniteLength : ThinStrictFiniteLength C σ a b)
(hCharge : ∀ {E : C}, Slicing.intervalProp C σ.slicing a b E → ¬Limits.IsZero E → F.ChargeNe E)
{L U : ℝ}
(hWindow : ∀ (Y : Slicing.IntervalCat C σ.slicing a b), ¬Limits.IsZero Y.obj → L < F.phase Y.obj ∧ F.phase Y.obj < U)
(hWidth : U - L < 1)
{V : ℝ}
(hHom :
∀ {E G : Slicing.IntervalCat C σ.slicing a b},
F.IsSemistable E.obj (F.phase E.obj) →
F.IsSemistable G.obj (F.phase G.obj) → F.phase G.obj < F.phase E.obj → F.phase E.obj < V → ∀ (f : E ⟶ G), f = 0)
(hDestabBound :
∀ {Y : Slicing.IntervalCat C σ.slicing a b},
¬Limits.IsZero Y →
∀ {A : Subobject Y},
F.IsSemistable (Subobject.underlying.obj A).obj (F.phase (Subobject.underlying.obj A).obj) →
IsStrictMono A.arrow →
F.phase Y.obj < F.phase (Subobject.underlying.obj A).obj → F.phase (Subobject.underlying.obj A).obj < V)
{X : Slicing.IntervalCat C σ.slicing a b}
(hX : ¬Limits.IsZero X)
:
∃ (B : Slicing.IntervalCat C σ.slicing a b) (q : X ⟶ B), IsStrictMDQ C σ F q
Every nonzero owner thin-interval object admits a strict maximal destabilizing quotient under strict finite length, a common phase window, and the semistable Hom-vanishing used in the recursive transport step.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.IsStrictMDQ.kernelSubobject_ne_bot_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 B : Slicing.IntervalCat C σ.slicing a b}
{q : X ⟶ B}
(hq : IsStrictMDQ C σ F q)
(hns : ¬F.IsSemistable X.obj (F.phase X.obj))
:
A strict MDQ of a non-semistable source has a genuinely nonzero kernel subobject.