Strict morphisms, and finiteness conditions built from them

A morphism is strict when its canonical coimage-to-image comparison is an isomorphism. The universal-property criteria below avoid importing the corresponding vendor module.

Four layers, in order:

• strict morphisms — IsStrict, IsStrictMono, IsStrictEpi, their kernel and cokernel criteria, and their relation to NormalMono/RegularEpi/ StrongEpi;
• StrictShortExact, and what it becomes in an abelian category, where every morphism is strict (isStrict_of_abelian);
• strict subobjects, and the strict Artinian, Noetherian and finite-length object properties they generate, each paired with its non-strict counterpart;
• transfer of all of it along a fully faithful functor preserving monos.

Placement

Generic category theory: this file imports only Mathlib's abelian, short-complex, pullback, and subobject material, mentions no stability condition, and uses nothing triangulated. It lives under CategoryTheory/Abelian/, beside Mathlib's Abelian/NonPreadditive.lean precedent for a category with exactness conditions weaker than abelian. It sat under StabilityCondition/Foundation/ until #488 because its first consumer was Bridgeland's thin-interval argument (Foundation/Slicing/IntervalStrictness.lean is still the caller), then under Triangulated/ until 2026-09-02, when the review of the Mathlib-mesh restructure applied the rule that a file belongs under Triangulated/ only if it uses something triangulated. The namespace stays CategoryTheory.Triangulated: declaration names are unchanged across moves so that the immutable review payloads the exe/RestateHistoricalNames.lean bridge protects keep resolving.

What this file asserts, and where

The QuasiAbelian class below states the two stability axioms — strict epimorphisms stable under pullback, strict monomorphisms stable under pushout. It is inhabited: Slicing.intervalCat_quasiAbelian (Foundation/Slicing/IntervalStrictness.lean) shows a thin owner slicing interval is quasi-abelian, and it is the only instance at the time of writing.

Most of the file is prior to that class: strictness of individual morphisms and the finiteness conditions built on it, none of which needs the axioms.

Two earlier versions of this section were wrong, in opposite directions. The first said QuasiAbelian "appears in no declaration in this file", which the class below contradicts. Its replacement said no category is shown to be quasi-abelian, which intervalCat_quasiAbelian contradicts — the search behind that claim matched one line at a time, and the instance carries its type on the next line. Neither claim should have been made without a search that could see a multi-line signature.

def CategoryTheory.Triangulated.IsStrict {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] : Prop

A morphism is strict when the canonical coimage-to-image comparison is an isomorphism.

Equations

• CategoryTheory.Triangulated.IsStrict f = CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)

structure CategoryTheory.Triangulated.IsStrictMono {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] : Prop

A strict monomorphism.

• mono : Mono f
• strict : IsStrict f

structure CategoryTheory.Triangulated.IsStrictEpi {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] : Prop

A strict epimorphism.

• epi : Epi f
• strict : IsStrict f

theorem CategoryTheory.Triangulated.isStrictEpi_of_isColimitCokernelCofork {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Limits.HasZeroObject C] [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] (hf : Limits.IsColimit (Limits.CokernelCofork.ofπ f ⋯)) : IsStrictEpi f

A morphism which is the cokernel of its kernel is a strict epimorphism.

theorem CategoryTheory.Triangulated.isStrictMono_of_isLimitKernelFork {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Limits.HasZeroObject C] [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] (hf : Limits.IsLimit (Limits.KernelFork.ofι f ⋯)) : IsStrictMono f

A morphism which is the kernel of its cokernel is a strict monomorphism.

noncomputable def CategoryTheory.Triangulated.IsStrictEpi.isColimitCokernelCofork {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Limits.HasZeroObject C] [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] (hf : IsStrictEpi f) : Limits.IsColimit (Limits.CokernelCofork.ofπ f ⋯)

A strict epimorphism is the cokernel of its kernel.

Equations

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

noncomputable def CategoryTheory.Triangulated.IsStrictMono.isLimitKernelFork {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Limits.HasZeroObject C] [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] (hf : IsStrictMono f) : Limits.IsLimit (Limits.KernelFork.ofι f ⋯)

A strict monomorphism is the kernel of its cokernel.

Equations

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

@[reducible]

noncomputable def CategoryTheory.Triangulated.IsStrictEpi.normalEpi {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Limits.HasZeroObject C] [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] (hf : IsStrictEpi f) : NormalEpi f

A strict epimorphism supplies a normal epimorphism witness.

Equations

• hf.normalEpi = { W := CategoryTheory.Limits.kernel f, g := CategoryTheory.Limits.kernel.ι f, w := ⋯, isColimit := hf.isColimitCokernelCofork }

@[reducible]

noncomputable def CategoryTheory.Triangulated.IsStrictMono.normalMono {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Limits.HasZeroObject C] [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] (hf : IsStrictMono f) : NormalMono f

A strict monomorphism supplies a normal monomorphism witness.

Equations

• hf.normalMono = { Z := CategoryTheory.Limits.cokernel f, g := CategoryTheory.Limits.cokernel.π f, w := ⋯, isLimit := hf.isLimitKernelFork }

theorem CategoryTheory.Triangulated.isStrictMono_of_isIso {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Limits.HasZeroObject C] [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] [IsIso f] : IsStrictMono f

Every isomorphism is a strict monomorphism.

theorem CategoryTheory.Triangulated.isStrictEpi_of_isIso {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Limits.HasZeroObject C] [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] [IsIso f] : IsStrictEpi f

Every isomorphism is a strict epimorphism.

theorem CategoryTheory.Triangulated.IsStrictEpi.isIso {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Limits.HasZeroObject C] [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] (hf : IsStrictEpi f) [Mono f] : IsIso f

A strict epimorphism which is also monic is an isomorphism.

theorem CategoryTheory.Triangulated.IsStrictMono.isIso {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Limits.HasZeroObject C] [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] (hf : IsStrictMono f) [Epi f] : IsIso f

A strict monomorphism which is also epic is an isomorphism.

theorem CategoryTheory.Triangulated.isStrictEpi_of_normalEpi {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Limits.HasZeroObject C] [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] [hf : NormalEpi f] : IsStrictEpi f

Every normal epimorphism is strict.

theorem CategoryTheory.Triangulated.isStrictMono_of_normalMono {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Limits.HasZeroObject C] [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] [hf : NormalMono f] : IsStrictMono f

Every normal monomorphism is strict.

noncomputable def CategoryTheory.Triangulated.IsStrictEpi.regularEpi {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Limits.HasZeroObject C] [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] (hf : IsStrictEpi f) : RegularEpi f

A strict epimorphism supplies a regular epimorphism witness.

Equations

• hf.regularEpi = CategoryTheory.NormalEpi.regularEpi f

theorem CategoryTheory.Triangulated.IsStrictEpi.strongEpi {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Limits.HasZeroObject C] [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] (hf : IsStrictEpi f) : StrongEpi f

Every strict epimorphism is strong.

noncomputable def CategoryTheory.Triangulated.IsStrictMono.regularMono {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Limits.HasZeroObject C] [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] (hf : IsStrictMono f) : RegularMono f

A strict monomorphism supplies a regular monomorphism witness.

Equations

• hf.regularMono = CategoryTheory.NormalMono.regularMono f

theorem CategoryTheory.Triangulated.IsStrictMono.strongMono {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Limits.HasZeroObject C] [Limits.HasKernel f] [Limits.HasCokernel f] [Limits.HasKernel (Limits.cokernel.π f)] [Limits.HasCokernel (Limits.kernel.ι f)] (hf : IsStrictMono f) : StrongMono f

Every strict monomorphism is strong.

theorem CategoryTheory.Triangulated.isStrictMono_kernel {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {X Y : C} (g : X ⟶ Y) : IsStrictMono (Limits.kernel.ι g)

A kernel inclusion is a strict monomorphism.

theorem CategoryTheory.Triangulated.isStrictEpi_cokernel {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {X Y : C} (g : X ⟶ Y) : IsStrictEpi (Limits.cokernel.π g)

A cokernel projection is a strict epimorphism.

class CategoryTheory.Triangulated.QuasiAbelian (C : Type u) [Category.{v, u} C] [Preadditive C] [Limits.HasKernels C] [Limits.HasCokernels C] [Limits.HasPullbacks C] [Limits.HasPushouts C] : Prop

An owner quasi-abelian category is preabelian and has pullbacks and pushouts, with strict epimorphisms stable under pullback and strict monomorphisms stable under pushout.

• pullback_strictEpi {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : IsStrictEpi g → IsStrictEpi (Limits.pullback.fst f g)
• pushout_strictMono {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y) : IsStrictMono f → IsStrictMono (Limits.pushout.inr f g)

structure CategoryTheory.Triangulated.StrictShortExact {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] (S : ShortComplex C) : Prop

A strict short exact sequence is a short exact complex whose two maps are strict.

• shortExact : S.ShortExact
• strict_f : IsStrict S.f
• strict_g : IsStrict S.g

theorem CategoryTheory.Triangulated.IsStrictEpi.strictShortExact_kernel {D : Type u} [Category.{v, u} D] [Preadditive D] [Limits.HasKernels D] [Limits.HasCokernels D] {X Y : D} (q : X ⟶ Y) [Limits.HasZeroObject D] (hq : IsStrictEpi q) : StrictShortExact { X₁ := Limits.kernel q, X₂ := X, X₃ := Y, f := Limits.kernel.ι q, g := q, zero := ⋯ }

The canonical kernel sequence of a strict epimorphism is strict short exact.

theorem CategoryTheory.Triangulated.isStrict_of_abelian {D : Type u} [Category.{v, u} D] [Abelian D] {X Y : D} (f : X ⟶ Y) : IsStrict f

Every morphism in an abelian category is strict.

theorem CategoryTheory.Triangulated.isStrictMono_of_mono {D : Type u} [Category.{v, u} D] [Abelian D] {X Y : D} (f : X ⟶ Y) [Mono f] : IsStrictMono f

Every monomorphism in an abelian category is strict.

theorem CategoryTheory.Triangulated.isStrictEpi_of_epi {D : Type u} [Category.{v, u} D] [Abelian D] {X Y : D} (f : X ⟶ Y) [Epi f] : IsStrictEpi f

Every epimorphism in an abelian category is strict.

theorem CategoryTheory.Triangulated.strictShortExact_of_shortExact {D : Type u} [Category.{v, u} D] [Abelian D] {S : ShortComplex D} (h : S.ShortExact) : StrictShortExact S

Every short exact sequence in an abelian category is strictly short exact.

def CategoryTheory.Triangulated.IsStrictSubobject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {X : C} (P : Subobject X) : Prop

A strict subobject is one whose canonical inclusion is an owner strict monomorphism.

Equations

• CategoryTheory.Triangulated.IsStrictSubobject P = CategoryTheory.Triangulated.IsStrictMono P.arrow

@[simp]

theorem CategoryTheory.Triangulated.isStrictSubobject_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {X : C} (P : Subobject X) : IsStrictSubobject P ↔ IsStrictMono P.arrow

@[reducible, inline]

abbrev CategoryTheory.Triangulated.StrictSubobject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] (X : C) : Type (max 0 u v)

The ordered type of strict subobjects of an object.

Equations

• CategoryTheory.Triangulated.StrictSubobject X = { P : CategoryTheory.Subobject X // CategoryTheory.Triangulated.IsStrictSubobject P }

def CategoryTheory.Triangulated.isStrictArtinianObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] : ObjectProperty C

Objects satisfying the descending chain condition on strict subobjects.

Equations

• CategoryTheory.Triangulated.isStrictArtinianObject X = WellFoundedLT (CategoryTheory.Triangulated.StrictSubobject X)

@[reducible, inline]

abbrev CategoryTheory.Triangulated.IsStrictArtinianObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] (X : C) : Prop

Proposition-level strict-Artinian predicate.

Equations

• CategoryTheory.Triangulated.IsStrictArtinianObject X = CategoryTheory.Triangulated.isStrictArtinianObject.Is X

instance CategoryTheory.Triangulated.instWellFoundedLTStrictSubobjectOfIsStrictArtinianObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {X : C} [IsStrictArtinianObject X] : WellFoundedLT (StrictSubobject X)

def CategoryTheory.Triangulated.isStrictNoetherianObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] : ObjectProperty C

Objects satisfying the ascending chain condition on strict subobjects.

Equations

• CategoryTheory.Triangulated.isStrictNoetherianObject X = WellFoundedGT (CategoryTheory.Triangulated.StrictSubobject X)

@[reducible, inline]

abbrev CategoryTheory.Triangulated.IsStrictNoetherianObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] (X : C) : Prop

Proposition-level strict-Noetherian predicate.

Equations

• CategoryTheory.Triangulated.IsStrictNoetherianObject X = CategoryTheory.Triangulated.isStrictNoetherianObject.Is X

instance CategoryTheory.Triangulated.instWellFoundedGTStrictSubobjectOfIsStrictNoetherianObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {X : C} [IsStrictNoetherianObject X] : WellFoundedGT (StrictSubobject X)

theorem CategoryTheory.Triangulated.isStrictArtinianObject_of_isArtinianObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {X : C} [IsArtinianObject X] : IsStrictArtinianObject X

An Artinian object is strict-Artinian.

theorem CategoryTheory.Triangulated.isStrictNoetherianObject_of_isNoetherianObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {X : C} [IsNoetherianObject X] : IsStrictNoetherianObject X

A Noetherian object is strict-Noetherian.

theorem CategoryTheory.Triangulated.isArtinianObject_of_isStrictArtinianObject {D : Type u} [Category.{v, u} D] [Abelian D] {X : D} [IsStrictArtinianObject X] : IsArtinianObject X

A strict-Artinian object in an abelian category is Artinian.

theorem CategoryTheory.Triangulated.isNoetherianObject_of_isStrictNoetherianObject {D : Type u} [Category.{v, u} D] [Abelian D] {X : D} [IsStrictNoetherianObject X] : IsNoetherianObject X

A strict-Noetherian object in an abelian category is Noetherian.

noncomputable def CategoryTheory.Triangulated.subobjectImageOfFullFaithful {A : Type u} [Category.{v, u} A] {D : Type u'} [Category.{v', u'} D] (F : Functor A D) [F.Full] [F.Faithful] [F.PreservesMonomorphisms] {E : A} : Subobject E → Subobject (F.obj E)

The map on subobjects induced by a full faithful functor preserving monomorphisms.

Equations

• CategoryTheory.Triangulated.subobjectImageOfFullFaithful F = CategoryTheory.Subobject.lift (fun {S : A} (f : S ⟶ E) [CategoryTheory.Mono f] => CategoryTheory.Subobject.mk (F.map f)) ⋯

theorem CategoryTheory.Triangulated.subobjectImageOfFullFaithful_injective {A : Type u} [Category.{v, u} A] {D : Type u'} [Category.{v', u'} D] (F : Functor A D) [F.Full] [F.Faithful] [F.PreservesMonomorphisms] {E : A} : Function.Injective (subobjectImageOfFullFaithful F)

The induced map on subobjects is injective.

theorem CategoryTheory.Triangulated.subobjectImageOfFullFaithful_monotone {A : Type u} [Category.{v, u} A] {D : Type u'} [Category.{v', u'} D] (F : Functor A D) [F.Full] [F.Faithful] [F.PreservesMonomorphisms] {E : A} : Monotone (subobjectImageOfFullFaithful F)

The induced map on subobjects is monotone.

theorem CategoryTheory.Triangulated.Finite.subobject_of_fullFaithful_preservesMono {A : Type u} [Category.{v, u} A] {D : Type u'} [Category.{v', u'} D] (F : Functor A D) [F.Full] [F.Faithful] [F.PreservesMonomorphisms] {E : A} (h : Finite (Subobject (F.obj E))) : Finite (Subobject E)

A full faithful functor preserving monomorphisms reflects finiteness of subobject lattices.

theorem CategoryTheory.Triangulated.isArtinianObject_of_fullFaithful_preservesMono {A : Type u} [Category.{v, u} A] {D : Type u'} [Category.{v', u'} D] (F : Functor A D) [F.Full] [F.Faithful] [F.PreservesMonomorphisms] {E : A} [IsArtinianObject (F.obj E)] : IsArtinianObject E

Artinian objects transfer across full faithful functors preserving monomorphisms.

theorem CategoryTheory.Triangulated.isNoetherianObject_of_fullFaithful_preservesMono {A : Type u} [Category.{v, u} A] {D : Type u'} [Category.{v', u'} D] (F : Functor A D) [F.Full] [F.Faithful] [F.PreservesMonomorphisms] {E : A} [IsNoetherianObject (F.obj E)] : IsNoetherianObject E

Noetherian objects transfer across full faithful functors preserving monomorphisms.

noncomputable def CategoryTheory.Triangulated.strictSubobjectImageOfFullFaithful {A : Type u} [Category.{v, u} A] [Limits.HasZeroMorphisms A] [Limits.HasKernels A] [Limits.HasCokernels A] {D : Type u} [Category.{v, u} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor A D) [F.Full] [F.Faithful] (hF : ∀ {X Y : A} (f : X ⟶ Y), IsStrictMono f → IsStrictMono (F.map f)) {E : A} : StrictSubobject E → Subobject (F.obj E)

A full faithful functor that maps strict monomorphisms induces a map from owner strict subobjects to ambient subobjects.

Equations

• CategoryTheory.Triangulated.strictSubobjectImageOfFullFaithful F hF B = CategoryTheory.Subobject.mk (F.map (↑B).arrow)

theorem CategoryTheory.Triangulated.strictSubobjectImageOfFullFaithful_monotone {A : Type u} [Category.{v, u} A] [Limits.HasZeroMorphisms A] [Limits.HasKernels A] [Limits.HasCokernels A] {D : Type u} [Category.{v, u} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor A D) [F.Full] [F.Faithful] (hF : ∀ {X Y : A} (f : X ⟶ Y), IsStrictMono f → IsStrictMono (F.map f)) {E : A} : Monotone (strictSubobjectImageOfFullFaithful F ⋯)

The ambient-subobject image of owner strict subobjects is monotone.

theorem CategoryTheory.Triangulated.strictSubobjectImageOfFullFaithful_injective {A : Type u} [Category.{v, u} A] [Limits.HasZeroMorphisms A] [Limits.HasKernels A] [Limits.HasCokernels A] {D : Type u} [Category.{v, u} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor A D) [F.Full] [F.Faithful] (hF : ∀ {X Y : A} (f : X ⟶ Y), IsStrictMono f → IsStrictMono (F.map f)) {E : A} : Function.Injective (strictSubobjectImageOfFullFaithful F ⋯)

The ambient-subobject image of owner strict subobjects is injective.

theorem CategoryTheory.Triangulated.isStrictArtinianObject_of_fullFaithful_map_strictMono {A : Type u} [Category.{v, u} A] [Limits.HasZeroMorphisms A] [Limits.HasKernels A] [Limits.HasCokernels A] {D : Type u} [Category.{v, u} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor A D) [F.Full] [F.Faithful] (hF : ∀ {X Y : A} (f : X ⟶ Y), IsStrictMono f → IsStrictMono (F.map f)) {E : A} [IsArtinianObject (F.obj E)] : IsStrictArtinianObject E

Strict-Artinian objects transfer across full faithful functors that map strict monomorphisms to strict monomorphisms.

theorem CategoryTheory.Triangulated.isStrictNoetherianObject_of_fullFaithful_map_strictMono {A : Type u} [Category.{v, u} A] [Limits.HasZeroMorphisms A] [Limits.HasKernels A] [Limits.HasCokernels A] {D : Type u} [Category.{v, u} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor A D) [F.Full] [F.Faithful] (hF : ∀ {X Y : A} (f : X ⟶ Y), IsStrictMono f → IsStrictMono (F.map f)) {E : A} [IsNoetherianObject (F.obj E)] : IsStrictNoetherianObject E

Strict-Noetherian objects transfer across full faithful functors that map strict monomorphisms to strict monomorphisms.

def CategoryTheory.Triangulated.IsStrictFiniteLengthObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] (X : C) : Prop

Both chain conditions on StrictSubobject X at once.

The conditions are stated on strict subobjects rather than on all of Subobject X because that is the order a quasi-abelian category actually controls: a strict monomorphism is exactly one that is the kernel of its own cokernel (IsStrictMono.isLimitKernelFork), so a strict subobject has a well-behaved quotient and a non-strict one need not. This is the hypothesis Harder–Narasimhan recursion needs — it terminates on chains of strict subobjects — and it is strictly weaker than IsFiniteLengthObject in general, because StrictSubobject X is a subtype of Subobject X and a chain condition on a subtype is the easier statement. The two coincide exactly when every mono is strict, which isStrictFiniteLengthObject_iff_isFiniteLengthObject records for abelian categories.

Equations

• CategoryTheory.Triangulated.IsStrictFiniteLengthObject X = (CategoryTheory.Triangulated.IsStrictArtinianObject X ∧ CategoryTheory.Triangulated.IsStrictNoetherianObject X)

def CategoryTheory.Triangulated.IsFiniteLengthObject {C : Type u} [Category.{v, u} C] (X : C) : Prop

Both chain conditions on Subobject X at once.

Mathlib has IsArtinianObject and IsNoetherianObject but no bundled object-level finite-length predicate, so this is defined here rather than imported; it is a plausible upstreaming candidate. It exists in this file only to state the comparison results below — the owner API is built on IsStrictFiniteLengthObject.

Equations

• CategoryTheory.Triangulated.IsFiniteLengthObject X = (CategoryTheory.IsArtinianObject X ∧ CategoryTheory.IsNoetherianObject X)

theorem CategoryTheory.Triangulated.isStrictFiniteLengthObject_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {X : C} : IsStrictFiniteLengthObject X ↔ IsStrictArtinianObject X ∧ IsStrictNoetherianObject X

Destructure strict finite length into its two chain conditions.

Definitionally Iff.rfl. It exists so that a deformation hypothesis carrying an IsStrictFiniteLengthObject can produce the two instances without callers unfolding the definition, which keeps later proofs stable if the conjunction is ever replaced by a structure.

theorem CategoryTheory.Triangulated.IsStrictFiniteLengthObject.isStrictArtinianObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {X : C} (h : IsStrictFiniteLengthObject X) : IsStrictArtinianObject X

The descending chain condition carried by strict finite length.

A deformation hypothesis arrives as a bare IsStrictFiniteLengthObject X, but every consumer downstream wants the chain conditions as instances, so the recurring idiom is letI := h.isStrictArtinianObject. Going through the named projection rather than h.1 keeps those call sites readable and unbroken if the conjunction ever becomes a structure.

theorem CategoryTheory.Triangulated.IsStrictFiniteLengthObject.isStrictNoetherianObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {X : C} (h : IsStrictFiniteLengthObject X) : IsStrictNoetherianObject X

The ascending chain condition carried by strict finite length.

See IsStrictFiniteLengthObject.isStrictArtinianObject for why this is a named projection rather than h.2.

theorem CategoryTheory.Triangulated.IsStrictFiniteLengthObject.mk' {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {X : C} [IsStrictArtinianObject X] [IsStrictNoetherianObject X] : IsStrictFiniteLengthObject X

Assemble strict finite length from the two chain conditions as instances.

The mirror image of the projections: consumers hand back instances, and this is what turns them into the packaged hypothesis without an anonymous constructor at every call site.

theorem CategoryTheory.Triangulated.IsFiniteLengthObject.isArtinianObject {C : Type u} [Category.{v, u} C] {X : C} (h : IsFiniteLengthObject X) : IsArtinianObject X

The descending chain condition carried by ordinary finite length.

theorem CategoryTheory.Triangulated.IsFiniteLengthObject.isNoetherianObject {C : Type u} [Category.{v, u} C] {X : C} (h : IsFiniteLengthObject X) : IsNoetherianObject X

The ascending chain condition carried by ordinary finite length.

theorem CategoryTheory.Triangulated.IsFiniteLengthObject.mk' {C : Type u} [Category.{v, u} C] {X : C} [IsArtinianObject X] [IsNoetherianObject X] : IsFiniteLengthObject X

Assemble ordinary finite length from the two chain conditions as instances.

theorem CategoryTheory.Triangulated.isStrictFiniteLengthObject_of_finite_subobjects {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {X : C} (h : Finite (Subobject X)) : IsStrictFiniteLengthObject X

Finitely many subobjects force strict finite length.

Both halves come from the single Finite (Subobject X) hypothesis: it makes the subtype StrictSubobject X finite, and a finite order is well-founded in both directions at once, so neither chain condition needs a separate argument. This is the constructor to reach for on an object of a heart with finitely many subobjects, where checking the chain conditions directly would mean an induction.

theorem CategoryTheory.Triangulated.isStrictFiniteLengthObject_of_isFiniteLengthObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {X : C} (h : IsFiniteLengthObject X) : IsStrictFiniteLengthObject X

Finite length implies strict finite length, in any quasi-abelian category.

The implication runs this way and not the other because well-foundedness restricts along the inclusion StrictSubobject X ↪ Subobject X: a chain of strict subobjects is in particular a chain of subobjects, so both conditions transport by InvImage.wf. Recovering the converse needs every mono to be strict, and so is available only under Abelian — see isStrictFiniteLengthObject_iff_isFiniteLengthObject.

theorem CategoryTheory.Triangulated.isStrictFiniteLengthObject_iff_isFiniteLengthObject {D : Type u} [Category.{v, u} D] [Abelian D] {X : D} : IsStrictFiniteLengthObject X ↔ IsFiniteLengthObject X

Over an abelian category the strict and ordinary notions agree.

Abelian is what collapses the distinction: every monomorphism is strict, so StrictSubobject X is the whole of Subobject X and the two chain conditions are the same statement. Only the forward direction consumes the hypothesis; the reverse is the general implication above. The practical use is to import finite-length facts about a heart, which is abelian, into the quasi-abelian interval categories where the owner theory lives — the transfer is sound in that direction precisely because this equivalence is unavailable in the quasi-abelian setting itself.