Nilpotency from a shifted finite filtration

The abstract engine of a filtration argument, in a preadditive category with a zero object. Given a finite chain of subobjects F : ℕ → Subobject X with F 0 = ⊤ and F N = ⊥, an endomorphism f that moves each stage into the next — in the sense that (F k).arrow ≫ f factors through F (k + 1) for every k < N — satisfies f ^ N = 0 (RS.comp_eq_zero_of_chain); if f is moreover idempotent it vanishes outright (RS.eq_zero_of_idem_of_chain). Convenience forms taking the chain as a Fin (N + 1)-indexed family are also provided (RS.comp_eq_zero_of_finChain, RS.eq_zero_of_idem_of_finChain).

No monotonicity of the chain is assumed: only the endpoints and the shift hypothesis enter the argument.

Composition-order convention

Multiplication in End X is reversed composition: g * h = h ≫ g (CategoryTheory.End.mul_def). Read as a morphism via CategoryTheory.End.asHom, the power f ^ (n + 1) is therefore End.asHom (f ^ n) ≫ End.asHom f; the lemma RS.pow_end_eq records exactly this unfolding. (For powers of a single endomorphism all bracketings agree, but consumers matching syntactically against f ^ N should unfold via pow_end_eq.) The shift hypothesis is phrased with End.asHom f, so consumers supply factorisations of the morphism (F k).arrow ≫ End.asHom f.

theorem RS.pow_end_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (f : CategoryTheory.End X) (n : ℕ) : (f ^ (n + 1)).asHom = CategoryTheory.CategoryStruct.comp (f ^ n).asHom f.asHom

Powers in End X unfold through the reversed multiplication of End: read as a morphism, f ^ (n + 1) is f ^ n ≫ f.

theorem RS.comp_eq_zero_of_chain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {N : ℕ} (F : ℕ → CategoryTheory.Subobject X) (htop : F 0 = ⊤) (hbot : F N = ⊥) (f : CategoryTheory.End X) (hshift : ∀ k < N, (F (k + 1)).Factors (CategoryTheory.CategoryStruct.comp (F k).arrow f.asHom)) : f ^ N = 0

Shifting a finite chain forces nilpotency. If the chain F runs from F 0 = ⊤ to F N = ⊥ and the endomorphism f moves each stage into the next — (F k).arrow ≫ f factors through F (k + 1) for every k < N — then f ^ N = 0.

The proof shows by induction that (⊤ : Subobject X).arrow composed with f ^ k factors through F k; at k = N the factorisation runs through ⊥, whose arrow is zero, and the top arrow is an isomorphism, hence an epimorphism.

theorem RS.eq_zero_of_idem_of_chain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {N : ℕ} (F : ℕ → CategoryTheory.Subobject X) (htop : F 0 = ⊤) (hbot : F N = ⊥) (f : CategoryTheory.End X) (hshift : ∀ k < N, (F (k + 1)).Factors (CategoryTheory.CategoryStruct.comp (F k).arrow f.asHom)) (hidem : f * f = f) : f = 0

A shifted idempotent is zero. Under the hypotheses of comp_eq_zero_of_chain, an idempotent f (with respect to the End multiplication f * f = f) vanishes outright: f ^ N = 0 and f = f ^ N for N ≥ 1, while N = 0 makes X a zero object.

theorem RS.comp_eq_zero_of_finChain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {N : ℕ} (F : Fin (N + 1) → CategoryTheory.Subobject X) (htop : F 0 = ⊤) (hbot : F (Fin.last N) = ⊥) (f : CategoryTheory.End X) (hshift : ∀ (k : Fin N), (F k.succ).Factors (CategoryTheory.CategoryStruct.comp (F k.castSucc).arrow f.asHom)) : f ^ N = 0

Convenience form of comp_eq_zero_of_chain with the chain indexed by Fin (N + 1): it runs from F 0 = ⊤ to F (Fin.last N) = ⊥, and the shift hypothesis is stated over k : Fin N via Fin.castSucc and Fin.succ.

theorem RS.eq_zero_of_idem_of_finChain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {N : ℕ} (F : Fin (N + 1) → CategoryTheory.Subobject X) (htop : F 0 = ⊤) (hbot : F (Fin.last N) = ⊥) (f : CategoryTheory.End X) (hshift : ∀ (k : Fin N), (F k.succ).Factors (CategoryTheory.CategoryStruct.comp (F k.castSucc).arrow f.asHom)) (hidem : f * f = f) : f = 0

Convenience form of eq_zero_of_idem_of_chain with the chain indexed by Fin (N + 1).