Truncating a weak HN filtration, and the cut at a slope

This is Truncation.lean for the slope-indexed weak filtration, together with Splitting.lean's crossing index and the sub half of the splitting.

What ports and what does not, stated precisely

Truncation.lean has two truncations and they behave differently under weakening.

• restrict — read the chain below an index as a filtration of the term at that index. It travels along Subobject.map of a monomorphism, uses only Subobject.map_obj_injective and the successive-quotient congruences, and mentions no charge. It ports verbatim, and is restrict below.

• Uniqueness/Tail.lean's tailAt — push the chain above an index down to the quotient. It did not port when this file was written: its two supporting lemmas, pullback_imageSubobject_eq and cokernelPullbackIso, were proved from semiClosedUpperHalfPlane_ne_zero — a nonzero object has nonzero charge — which is precisely the implication weak stability drops, and which fails on the skyscraper.

  That obstruction is gone. Both statements are true in any abelian category, being the subobject correspondence for a quotient, and CategoryTheory/SubobjectCorrespondence.lean proves them with no charge anywhere. WeakTail.lean ports tailAt on top of them.

exists_subobject_hnTors below gives the torsion subobject of the splitting. It is kept because it is the weaker statement and needs no truncation of the quotient, but it is superseded by WeakStabilityFunctionOn.exists_subobject_hnTors_cokernel_hnFree (WeakSplitting.lean), which supplies both halves — and hence by the weak TorsionPair in Weak/Tilting/TorsionPair/WeakStabilityFunction.lean.

noncomputable def CategoryTheory.Triangulated.AbelianWeakHNFiltration.restrictChain {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) (k : ℕ) (hkn : k ≤ F.n) (j : ℕ) (hjk : j ≤ k) : Subobject (Subobject.underlying.obj (F.chain ⟨k, ⋯⟩))

The j-th term of a weak HN filtration read as a subobject of the k-th term, for j ≤ k.

Equations

• F.restrictChain k hkn j hjk = CategoryTheory.Subobject.mk ((F.chain ⟨j, ⋯⟩).ofLE (F.chain ⟨k, ⋯⟩) ⋯)

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.map_restrictChain {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) (k : ℕ) (hkn : k ≤ F.n) (j : ℕ) (hjk : j ≤ k) : (Subobject.map (F.chain ⟨k, ⋯⟩).arrow).obj (F.restrictChain k hkn j hjk) = F.chain ⟨j, ⋯⟩

Mapping a restricted term back along the arrow of the k-th term recovers the original term.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.restrictChain_le {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) (k : ℕ) (hkn : k ≤ F.n) {j₁ j₂ : ℕ} (hj : j₁ ≤ j₂) (hjk : j₂ ≤ k) : F.restrictChain k hkn j₁ ⋯ ≤ F.restrictChain k hkn j₂ hjk

The restricted chain is monotone, by composing the inclusions.

noncomputable def CategoryTheory.Triangulated.AbelianWeakHNFiltration.restrict {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) (k : ℕ) (hk : 0 < k) (hkn : k ≤ F.n) : AbelianWeakHNFiltration W (Subobject.underlying.obj (F.chain ⟨k, ⋯⟩))

The chain below an index is a weak HN filtration of the term at that index. The factors are the original factors 0, …, k-1, so the slopes are the original slopes up to k.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.restrict_n {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) (k : ℕ) (hk : 0 < k) (hkn : k ≤ F.n) : (F.restrict k hk hkn).n = k

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.restrict_μPlus {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) (k : ℕ) (hk : 0 < k) (hkn : k ≤ F.n) : (F.restrict k hk hkn).μPlus = F.μPlus

A restriction starts where the filtration it was cut from starts.

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.restrict_μMinus {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) (k : ℕ) (hk : 0 < k) (hkn : k ≤ F.n) : (F.restrict k hk hkn).μMinus = F.μ ⟨k - 1, ⋯⟩

The lowest slope of a restriction is the last slope below the cut.

def CategoryTheory.Triangulated.AbelianWeakHNFiltration.ofIso {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) {E' : A} (e : E ≅ E') : AbelianWeakHNFiltration W E'

Transport along an isomorphism. The chain is carried by Subobject.map of the isomorphism, which leaves every successive quotient isomorphic to the original, so the slopes are literally the same function.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.ofIso_μPlus {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) {E' : A} (e : E ≅ E') : (F.ofIso e).μPlus = F.μPlus

@[simp]

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.ofIso_μMinus {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) {E' : A} (e : E ≅ E') : (F.ofIso e).μMinus = F.μMinus

theorem CategoryTheory.Triangulated.AbelianWeakHNFiltration.exists_crossIndex {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {E : A} (F : AbelianWeakHNFiltration W E) (μ₀ : WithTop ℝ) : ∃ k ≤ F.n, (∀ (j : Fin F.n), ↑j < k → μ₀ < F.μ j) ∧ ∀ (j : Fin F.n), k ≤ ↑j → F.μ j ≤ μ₀

The crossing index. The HN slopes strictly decrease, so the indices whose slope exceeds μ₀ are an initial segment; this names its length. The argument is Nat.find on the order alone, so WithTop ℝ serves as well as ℝ.

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.hnTors_of_iso {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {μ₀ : WithTop ℝ} {E E' : A} (e : E ≅ E') (h : E ∈ W.hnTors μ₀) : E' ∈ W.hnTors μ₀

The torsion class is closed under isomorphism.

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.hnFree_of_iso {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {μ₀ : WithTop ℝ} {E E' : A} (e : E ≅ E') (h : E ∈ W.hnFree μ₀) : E' ∈ W.hnFree μ₀

The torsion-free class is closed under isomorphism.

theorem CategoryTheory.Triangulated.WeakStabilityFunctionOn.exists_subobject_hnTors {A : Type u} [Category.{v, u} A] [Abelian A] {W : WeakStabilityFunctionOn (abelianDatum A)} {μ₀ : WithTop ℝ} (hHN : W.HasHNProperty) (E : A) : ∃ (T : Subobject E), Subobject.underlying.obj T ∈ W.hnTors μ₀

The torsion subobject of the splitting. Cutting an HN filtration at its crossing index gives a subobject in T μ₀.

This is one half of exists_subobject_hnTors_cokernel_hnFree, and is superseded by it: WeakSplitting.lean now supplies the torsion-free quotient too. Kept because it is the weaker statement and does not truncate the quotient.