Finite-length Harder--Narasimhan recursion in owner thin intervals

Strict maximal destabilizing quotients have kernels whose proper strict quotients have larger phase. Strict-Artinian induction on those kernels then constructs finite Harder--Narasimhan filtrations without importing the frozen external implementation.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.kernelSubobject_isLimitKernelFork (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} (q : X ⟶ Y) : Limits.IsLimit (Limits.KernelFork.ofι (Limits.kernelSubobject q).arrow ⋯)

The interval kernel subobject represents the categorical kernel.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.strictShortExact_kernelSubobject (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} (q : X ⟶ Y) (hq : IsStrictEpi q) : StrictShortExact { X₁ := Subobject.underlying.obj (Limits.kernelSubobject q), X₂ := X, X₃ := Y, f := (Limits.kernelSubobject q).arrow, g := q, zero := ⋯ }

A strict epimorphism and its interval kernel subobject form a strict short exact sequence.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.kernelSubobject_ne_top_of_strictEpi_nonzero (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} {q : X ⟶ Y} (hq : IsStrictEpi q) (hY : ¬Limits.IsZero Y.obj) : Limits.kernelSubobject q ≠ ⊤

The kernel subobject of a strict epimorphism to a nonzero target is proper.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Subobject.map_eq_mk_comp {D : Type u_1} [Category.{u_2, u_1} D] {X Y : D} (e : X ≅ Y) (A : Subobject X) : (Subobject.map e.hom).obj A = Subobject.mk (CategoryStruct.comp A.arrow e.hom)

Owner spelling of the standard description of a mapped subobject.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Subobject.mapUnderlyingIso {D : Type u_1} [Category.{u_2, u_1} D] {X Y : D} (e : X ≅ Y) (A : Subobject X) : Subobject.underlying.obj ((Subobject.map e.hom).obj A) ≅ Subobject.underlying.obj A

Mapping a subobject along an isomorphism identifies the mapped representative canonically with the original subobject.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.phase_cokernel_kernelSubobject (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 : IsStrictEpi q) : F.phase (Limits.cokernel (Limits.kernelSubobject q).arrow).obj = F.phase B.obj

The canonical cokernel of the interval kernel subobject of a strict epimorphism has the same skewed phase as its target.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.IsStrictMDQ.phase_lt_of_strictQuotient_of_kernel (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) {A : Subobject (Subobject.underlying.obj (Limits.kernelSubobject q))} (hAtop : A ≠ ⊤) (hAstrict : IsStrictMono A.arrow) : F.phase B.obj < F.phase (Limits.cokernel A.arrow).obj

Every proper strict quotient of the kernel of a strict MDQ has phase strictly larger than the MDQ factor.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.hn_exists_of_quotientLowerBound (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) (t : ℝ) (X : Slicing.IntervalCat C σ.slicing a b) (hX : ¬Limits.IsZero X) (hquot : ∀ (A : Subobject X), A ≠ ⊤ → IsStrictMono A.arrow → t < F.phase (Limits.cokernel A.arrow).obj) : have Psem := fun (ψ : ℝ) (E : C) => F.IsSemistable E ψ; ∃ (G : HNFiltration C Psem X.obj), ∀ (j : Fin G.n), t < G.φ j ∧ G.φ j < U

Strict-Artinian recursion on kernel subobjects constructs an owner HN filtration. The explicit lower quotient bound is the induction invariant propagated from a strict MDQ to its kernel.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.hn_exists (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) : have Psem := fun (ψ : ℝ) (E : C) => F.IsSemistable E ψ; ∃ (G : HNFiltration C Psem X.obj), ∀ (j : Fin G.n), L < G.φ j ∧ G.φ j < U

Every nonzero object in an owner strict finite-length thin interval has an HN filtration whose phases remain in the common phase window.