Carrying an HN filtration along a monomorphism

Both constructions here move a chain by Subobject.map of a mono.

Uniqueness/Tail.lean owns tailAt, which pushes the chain above an index down to the quotient by that index. This file owns the other half — restrict, the chain below an index as an HN filtration of the term at that index — and ofIso, the transport along an isomorphism that the two classes at a cutoff need in order to be closed under isomorphism.

The two together cut a filtration in half at any index, and the halves keep the original factors — so their phases are read off F.phase with no new computation. That is what makes a cut at the index where the phases cross a number produce one object with all phases above it and one with all phases at or below it.

The chain is carried across by Subobject.map along the arrow of the term: map_restrictChain says the mapped-back chain is the original one, and MonoDescent.lean then supplies the successive quotients unchanged.

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

The j-th term of an 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.AbelianHNFiltration.map_restrictChain {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z 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.AbelianHNFiltration.restrictChain_le {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z 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.AbelianHNFiltration.restrict {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) (k : ℕ) (hk : 0 < k) (hkn : k ≤ F.n) : AbelianHNFiltration Z (Subobject.underlying.obj (F.chain ⟨k, ⋯⟩))

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

Equations

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

@[simp]

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

theorem CategoryTheory.Triangulated.AbelianHNFiltration.restrict_phiPlus {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) (k : ℕ) (hk : 0 < k) (hkn : k ≤ F.n) : (F.restrict k hk hkn).phiPlus = F.phiPlus

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

theorem CategoryTheory.Triangulated.AbelianHNFiltration.restrict_phiMinus {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) (k : ℕ) (hk : 0 < k) (hkn : k ≤ F.n) : (F.restrict k hk hkn).phiMinus = F.phase ⟨k - 1, ⋯⟩

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

def CategoryTheory.Triangulated.AbelianHNFiltration.ofIso {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) {E' : A} (e : E ≅ E') : AbelianHNFiltration Z 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 phases are literally the same function.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.AbelianHNFiltration.ofIso_phiPlus {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) {E' : A} (e : E ≅ E') : (F.ofIso e).phiPlus = F.phiPlus

@[simp]

theorem CategoryTheory.Triangulated.AbelianHNFiltration.ofIso_phiMinus {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) {E' : A} (e : E ≅ E') : (F.ofIso e).phiMinus = F.phiMinus