6. QuasiAbelian.Basic
Module BridgelandStability.QuasiAbelian.Basic — 8 declarations (Definition, Structure)
6.1. CategoryTheory.IsStrict
Definition | BridgelandStability.QuasiAbelian.Basic | Source | Open Issue
/-- A morphism `f` is *strict* if the canonical comparison morphism from the
(abelian) coimage to the (abelian) image is an isomorphism. In an abelian category,
every morphism is strict.
This uses `Abelian.coimageImageComparison` from `Mathlib.CategoryTheory.Abelian.Images`,
which is defined without assuming the category is abelian. -/
def IsStrict : Prop :=
IsIso (Abelian.coimageImageComparison f)
6.2. CategoryTheory.IsStrictMono
Structure | BridgelandStability.QuasiAbelian.Basic | Source | Open Issue
/-- A morphism is a *strict monomorphism* if it is both a monomorphism and strict. -/
structure IsStrictMono : Prop where
mono : Mono f
strict : IsStrict f
6.3. CategoryTheory.Subobject.IsStrict
Definition | BridgelandStability.QuasiAbelian.Basic | Source | Open Issue
/-- A subobject is *strict* if its arrow is a strict monomorphism. This is the
quasi-abelian notion of admissible / exact subobject used in Bridgeland's finite-length
thin interval categories. -/
def IsStrict (P : Subobject X) : Prop :=
IsStrictMono P.arrow
6.4. CategoryTheory.StrictSubobject
Definition | BridgelandStability.QuasiAbelian.Basic | Source | Open Issue
/-- The ordered type of strict subobjects of `X`. -/
abbrev StrictSubobject (X : C) :=
{ P : Subobject X // P.IsStrict }
6.5. CategoryTheory.isStrictArtinianObject
Definition | BridgelandStability.QuasiAbelian.Basic | Source | Open Issue
/-- An object is *strict-Artinian* if its strict subobjects satisfy the descending chain
condition. This is the exact finite-length notion relevant to quasi-abelian categories. -/
def isStrictArtinianObject : ObjectProperty C :=
fun X ↦ WellFoundedLT (StrictSubobject X)
6.6. CategoryTheory.isStrictNoetherianObject
Definition | BridgelandStability.QuasiAbelian.Basic | Source | Open Issue
/-- An object is *strict-Noetherian* if its strict subobjects satisfy the ascending chain
condition. This is the exact finite-length notion relevant to quasi-abelian categories. -/
def isStrictNoetherianObject : ObjectProperty C :=
fun X ↦ WellFoundedGT (StrictSubobject X)
6.7. CategoryTheory.IsStrictArtinianObject
Definition | BridgelandStability.QuasiAbelian.Basic | Source | Open Issue
/-- An object is *strict-Artinian* if its strict subobjects satisfy the descending chain
condition. -/
abbrev IsStrictArtinianObject : Prop := isStrictArtinianObject.Is X
6.8. CategoryTheory.IsStrictNoetherianObject
Definition | BridgelandStability.QuasiAbelian.Basic | Source | Open Issue
/-- An object is *strict-Noetherian* if its strict subobjects satisfy the ascending chain
condition. -/
abbrev IsStrictNoetherianObject : Prop := isStrictNoetherianObject.Is X