Bridgeland Stability Conditions

5. QuasiAbelian🔗

5.1. IsStrict🔗

A morphism f : X \to Y in a category with kernels and cokernels 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, so strictness is a nontrivial condition only in the pre-abelian setting.

Construction: Defined as IsIso (Abelian.coimageImageComparison f), using the comparison morphism from Mathlib that is defined without assuming the ambient category is abelian.

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

Something wrong, better idea? Suggest a change

5.2. IsStrictMono🔗

A morphism f is a strict monomorphism if it is both a monomorphism and strict: f is mono and the coimage-to-image comparison is an isomorphism.

Construction: A Prop-valued structure with two fields: mono : Mono f and strict : IsStrict f.

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

Constructor

CategoryTheory.IsStrictMono.mk.{v, u}

Fields

mono : CategoryTheory.Mono f
strict : CategoryTheory.IsStrict f

Something wrong, better idea? Suggest a change

5.3. IsStrictEpi🔗

A morphism f is a strict epimorphism if it is both an epimorphism and strict: f is epi and the coimage-to-image comparison is an isomorphism.

Construction: A Prop-valued structure with two fields: epi : Epi f and strict : IsStrict f.

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

Constructor

CategoryTheory.IsStrictEpi.mk.{v, u}

Fields

epi : CategoryTheory.Epi f
strict : CategoryTheory.IsStrict f

Something wrong, better idea? Suggest a change

5.4. isColimitCokernelCofork🔗

A strict epimorphism is the cokernel of its kernel: the cofork \operatorname{ker}(f) \xrightarrow{\iota} X \xrightarrow{f} Y is a colimit.

Construction: Constructs an IsColimit witness for the cokernel cofork of f at its kernel, using the isomorphism \operatorname{Coim}(f) \cong Y that results from strictness and the epi hypothesis.

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

Something wrong, better idea? Suggest a change

5.5. isLimitKernelFork🔗

A strict monomorphism is the kernel of its cokernel: the fork X \xrightarrow{f} Y \xrightarrow{\pi} \operatorname{coker}(f) is a limit.

Construction: Constructs an IsLimit witness for the kernel fork of f at its cokernel, using the isomorphism X \cong \operatorname{Im}(f) that results from strictness and the mono hypothesis.

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

Something wrong, better idea? Suggest a change

5.6. isStrictEpi_of_isColimitCokernelCofork🔗

If f is the cokernel of its kernel, then f is a strict epimorphism.

Proof: The colimit hypothesis makes f epi. The coimage-to-image comparison is shown to be an isomorphism by factoring it as \operatorname{inv}(\operatorname{image.\iota}) \circ e where e : \operatorname{Coim}(f) \cong Y comes from the colimit comparison.

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

Something wrong, better idea? Suggest a change

5.7. isStrictMono_of_isLimitKernelFork🔗

If f is the kernel of its cokernel, then f is a strict monomorphism.

Proof: The limit hypothesis makes f mono. An explicit inverse pair of kernel.lift morphisms establishes X \cong \operatorname{Im}(f), and the coimage-to-image comparison is expressed as a composition of isomorphisms.

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

Something wrong, better idea? Suggest a change

5.8. isStrictMono_of_isIso🔗

An isomorphism is a strict monomorphism.

Proof: Apply isStrictMono_of_isLimitKernelFork: the cokernel of an iso is zero, so f is trivially the kernel of its zero cokernel.

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

Something wrong, better idea? Suggest a change

5.9. isStrictEpi_of_isIso🔗

An isomorphism is a strict epimorphism.

Proof: Apply isStrictEpi_of_isColimitCokernelCofork: the kernel of an iso is zero, so f is trivially the cokernel of its zero kernel.

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

Something wrong, better idea? Suggest a change

5.10. IsStrictEpi.isIso🔗

A strict epimorphism that is also mono is an isomorphism.

Proof: The kernel is zero since f is mono. Descend through the cokernel colimit to construct a section, making f a split mono. A split mono that is also epi is an isomorphism.

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

Something wrong, better idea? Suggest a change

5.11. IsStrictMono.isIso🔗

A strict monomorphism that is also epi is an isomorphism.

Proof: The cokernel is zero since f is epi. Lift through the kernel limit to construct a retraction, making f a split epi. A split epi that is also mono is an isomorphism.

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

Something wrong, better idea? Suggest a change

5.12. normalEpi🔗

A strict epimorphism is a normal epimorphism: it is the cokernel of some morphism (namely, its own kernel).

Construction: Constructs a NormalEpi instance from the cokernel colimit witness.

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

Something wrong, better idea? Suggest a change

5.13. regularEpi🔗

A strict epimorphism is a regular epimorphism.

Construction: Obtained from the normal epi structure via NormalEpi.regularEpi.

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

Something wrong, better idea? Suggest a change

5.14. strongEpi🔗

A strict epimorphism is a strong epimorphism.

Proof: A regular epi is a strong epi in any category.

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

Something wrong, better idea? Suggest a change

5.15. isStrictEpi_of_normalEpi🔗

A normal epimorphism in a preadditive category with kernels and cokernels is strict.

Proof: Factor the normal epi's colimit through the kernel inclusion to obtain a colimit for the cokernel cofork, then apply isStrictEpi_of_isColimitCokernelCofork.

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

Something wrong, better idea? Suggest a change

5.16. normalMono🔗

A strict monomorphism is a normal monomorphism: it is the kernel of some morphism (namely, its own cokernel).

Construction: Constructs a NormalMono instance from the kernel limit witness.

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

Something wrong, better idea? Suggest a change

5.17. isStrictMono_of_normalMono🔗

A normal monomorphism in a preadditive category with kernels and cokernels is strict.

Proof: Factor the normal mono's limit through the cokernel projection to obtain a limit for the kernel fork, then apply isStrictMono_of_isLimitKernelFork.

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

Something wrong, better idea? Suggest a change

5.18. QuasiAbelian🔗

[Definition 4.1]

A preadditive category with kernels, cokernels, pullbacks, and pushouts is quasi-abelian if pullbacks of strict epimorphisms are strict epimorphisms and pushouts of strict monomorphisms are strict monomorphisms. This is the definition from Schneiders (1999), used in Bridgeland's treatment of hearts of t-structures.

Construction: A Prop-valued typeclass with two fields: pullback_strictEpi (stability of strict epis under pullback) and pushout_strictMono (stability of strict monos under pushout).

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

Instance Constructor

CategoryTheory.QuasiAbelian.mk.{v, u}

Methods

pullback_strictEpi : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  CategoryTheory.IsStrictEpi g → CategoryTheory.IsStrictEpi (CategoryTheory.Limits.pullback.fst f g)

The pullback of a strict epimorphism along any morphism is a strict epimorphism.

pushout_strictMono : ∀ {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y),
  CategoryTheory.IsStrictMono f → CategoryTheory.IsStrictMono (CategoryTheory.Limits.pushout.inr f g)

The pushout of a strict monomorphism along any morphism is a strict monomorphism.

Something wrong, better idea? Suggest a change

5.19. StrictShortExact🔗

A strict short exact sequence is a ShortComplex that is short exact (mono left, epi right, exact in the middle) and where both morphisms f and g are strict. In a quasi-abelian category, kernels of strict epis are strict monos and cokernels of strict monos are strict epis.

Construction: A Prop-valued structure carrying shortExact : S.ShortExact, strict_f : IsStrict S.f, and strict_g : IsStrict S.g.

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

Constructor

CategoryTheory.StrictShortExact.mk.{v, u}

Fields

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

Something wrong, better idea? Suggest a change

5.20. isStrictMono_kernel🔗

The kernel of any morphism is a strict monomorphism. The coimage-to-image comparison for \operatorname{ker}(g) \hookrightarrow X is an isomorphism because \operatorname{ker}(g) is mono (making the coimage trivial) and an explicit inverse pair of kernel.lift morphisms establishes \operatorname{ker}(g) \cong \operatorname{Im}(\operatorname{ker}(g)).

Proof: Since \operatorname{ker.\iota}(g) is mono, its kernel is zero, so \operatorname{cokernel.\pi}(\operatorname{ker.\iota}(\operatorname{ker.\iota}(g))) is an iso. An explicit inverse pair of kernel.lift morphisms shows \operatorname{ker}(g) \cong \operatorname{ker}(\operatorname{cokernel.\pi}( \operatorname{ker.\iota}(g))), and the comparison factors through these isos.

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

Something wrong, better idea? Suggest a change

5.21. isStrictEpi_cokernel🔗

The cokernel of any morphism is a strict epimorphism. The coimage-to-image comparison for Y \twoheadrightarrow \operatorname{coker}(g) is an isomorphism because \operatorname{coker}(g) is epi (making the image trivial) and an explicit inverse pair of cokernel.desc morphisms establishes \operatorname{Coim}(\operatorname{coker.\pi}(g)) \cong \operatorname{coker}(g).

Proof: Dual to isStrictMono_kernel: since \operatorname{coker.\pi}(g) is epi, its cokernel is zero, making \operatorname{ker.\iota}(\operatorname{coker.\pi}( \operatorname{coker.\pi}(g))) an iso. An explicit inverse pair of cokernel.desc morphisms completes the argument.

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

Something wrong, better idea? Suggest a change

5.22. isStrict_of_abelian🔗

In an abelian category, every morphism is strict.

Proof: In an abelian category, Abelian.coimageImageComparison is an isomorphism by definition.

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

Something wrong, better idea? Suggest a change

5.23. isStrictMono_of_mono🔗

In an abelian category, every monomorphism is a strict monomorphism.

Proof: Combine the mono hypothesis with isStrict_of_abelian.

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

Something wrong, better idea? Suggest a change

5.24. isStrictEpi_of_epi🔗

In an abelian category, every epimorphism is a strict epimorphism.

Proof: Combine the epi hypothesis with isStrict_of_abelian.

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

Something wrong, better idea? Suggest a change

5.25. strictShortExact_of_shortExact🔗

In an abelian category, every short exact sequence is a strict short exact sequence.

Proof: Apply isStrict_of_abelian to both morphisms of the short complex.

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

Something wrong, better idea? Suggest a change

5.26. Subobject.IsStrict🔗

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.

Construction: Defined as IsStrictMono P.arrow.

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

Something wrong, better idea? Suggest a change

5.27. isStrict_iff🔗

A subobject P is strict if and only if its arrow is a strict monomorphism.

Proof: Definitional unfolding (Iff.rfl).

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

Something wrong, better idea? Suggest a change

5.28. StrictSubobject🔗

The ordered type of strict subobjects of X: subobjects whose arrows are strict monomorphisms.

Construction: An abbreviation for \{ P : Subobject X // P.IsStrict \}.

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

Something wrong, better idea? Suggest a change

5.29. isStrictArtinianObject🔗

An object X is strict-Artinian if the strict subobjects of X satisfy the descending chain condition. This is the finite-length notion relevant to quasi-abelian categories.

Construction: Defined as an ObjectProperty asserting WellFoundedLT (StrictSubobject X).

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

Something wrong, better idea? Suggest a change

5.30. IsStrictArtinianObject🔗

The proposition that X is strict-Artinian.

Construction: An abbreviation for isStrictArtinianObject.Is X.

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

Something wrong, better idea? Suggest a change

5.31. instWellFoundedLTStrictSubobjectOfIsStrictArtinianObject🔗

If X is strictly Artinian (i.e., its strict subobjects satisfy the descending chain condition), then the poset of strict subobjects of X is well-founded for <.

Construction: Extracted from the isStrictArtinianObject property via prop_of_is.

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

Something wrong, better idea? Suggest a change

5.32. isStrictNoetherianObject🔗

An object X is strict-Noetherian if the strict subobjects of X satisfy the ascending chain condition.

Construction: Defined as an ObjectProperty asserting WellFoundedGT (StrictSubobject X).

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

Something wrong, better idea? Suggest a change

5.33. IsStrictNoetherianObject🔗

The proposition that X is strict-Noetherian.

Construction: An abbreviation for isStrictNoetherianObject.Is X.

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

Something wrong, better idea? Suggest a change

5.34. instWellFoundedGTStrictSubobjectOfIsStrictNoetherianObject🔗

If X is strictly Noetherian (i.e., its strict subobjects satisfy the ascending chain condition), then the poset of strict subobjects of X is well-founded for >.

Construction: Extracted from the isStrictNoetherianObject property via prop_of_is.

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

Something wrong, better idea? Suggest a change

5.35. isStrictArtinianObject_of_isArtinianObject🔗

Ordinary Artinian objects are strict-Artinian, since strict subobjects form a subtype of all subobjects and descending chains in the subtype lift to descending chains in the full subobject lattice.

Proof: The inclusion StrictSubobject X \hookrightarrow Subobject X is order-preserving, so InvImage.wf transfers the well-foundedness.

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

Something wrong, better idea? Suggest a change

5.36. isStrictNoetherianObject_of_isNoetherianObject🔗

Ordinary Noetherian objects are strict-Noetherian, since strict subobjects form a subtype of all subobjects and ascending chains in the subtype lift to ascending chains in the full subobject lattice.

Proof: The inclusion StrictSubobject X \hookrightarrow Subobject X is order-preserving, so InvImage.wf transfers the well-foundedness.

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

Something wrong, better idea? Suggest a change

5.37. isArtinianObject_of_isStrictArtinianObject🔗

In an abelian category, strict-Artinian and Artinian coincide, because every mono is strict.

Proof: Every subobject is strict (since every mono is strict in an abelian category), so descending chains of subobjects are descending chains of strict subobjects. Apply the antitone chain condition.

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

Something wrong, better idea? Suggest a change

5.38. isNoetherianObject_of_isStrictNoetherianObject🔗

In an abelian category, strict-Noetherian and Noetherian coincide, because every mono is strict.

Proof: Every subobject is strict (since every mono is strict in an abelian category), so ascending chains of subobjects are ascending chains of strict subobjects. Apply the monotone chain condition.

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

Something wrong, better idea? Suggest a change

5.39. subobject_of_faithful_preservesMono🔗

A faithful functor F : \mathcal{A} \to \mathcal{C} that preserves monomorphisms induces an injection on subobject lattices. If Finite (Subobject (F.obj E)) in \mathcal{C}, then Finite (Subobject E) in \mathcal{A}. The key use case is the full subcategory inclusion \iota : \mathcal{P}(\phi) \hookrightarrow \mathcal{C}, transferring local finiteness of the slicing.

Proof: Construct an injective map Subobject E \to Subobject (F.obj E) by applying F to representative arrows, verify injectivity using faithfulness and preimageIso, and apply Finite.of_injective.

🔗theorem
CategoryTheory.Finite.subobject_of_faithful_preservesMono.{v, u}
  {A : Type u} [CategoryTheory.Category.{v, u} A] {C : Type u}
  [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor A C)
  [F.Full] [F.Faithful] [F.PreservesMonomorphisms] {E : A}
  (h : Finite (CategoryTheory.Subobject (F.obj E))) :
  Finite (CategoryTheory.Subobject E)
CategoryTheory.Finite.subobject_of_faithful_preservesMono.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor A C)
  [F.Full] [F.Faithful]
  [F.PreservesMonomorphisms] {E : A}
  (h :
    Finite
      (CategoryTheory.Subobject
        (F.obj E))) :
  Finite (CategoryTheory.Subobject E)

Something wrong, better idea? Suggest a change

5.40. isArtinianObject_of_faithful_preservesMono🔗

Artinian objects transfer across full faithful functors that preserve monomorphisms.

Proof: Map descending chains of subobjects in \mathcal{A} to descending chains in \mathcal{C} via the injective monotone subobject image map. Stabilization in \mathcal{C} pulls back to stabilization in \mathcal{A} by injectivity.

🔗theorem
CategoryTheory.isArtinianObject_of_faithful_preservesMono.{v, u}
  {A : Type u} [CategoryTheory.Category.{v, u} A] {C : Type u}
  [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor A C)
  [F.Full] [F.Faithful] [F.PreservesMonomorphisms] {E : A}
  [CategoryTheory.IsArtinianObject (F.obj E)] :
  CategoryTheory.IsArtinianObject E
CategoryTheory.isArtinianObject_of_faithful_preservesMono.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor A C)
  [F.Full] [F.Faithful]
  [F.PreservesMonomorphisms] {E : A}
  [CategoryTheory.IsArtinianObject
      (F.obj E)] :
  CategoryTheory.IsArtinianObject E

Something wrong, better idea? Suggest a change

5.41. isNoetherianObject_of_faithful_preservesMono🔗

Noetherian objects transfer across full faithful functors that preserve monomorphisms.

Proof: Map ascending chains of subobjects in \mathcal{A} to ascending chains in \mathcal{C} via the injective monotone subobject image map. Stabilization in \mathcal{C} pulls back to stabilization in \mathcal{A} by injectivity.

🔗theorem
CategoryTheory.isNoetherianObject_of_faithful_preservesMono.{v, u}
  {A : Type u} [CategoryTheory.Category.{v, u} A] {C : Type u}
  [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor A C)
  [F.Full] [F.Faithful] [F.PreservesMonomorphisms] {E : A}
  [CategoryTheory.IsNoetherianObject (F.obj E)] :
  CategoryTheory.IsNoetherianObject E
CategoryTheory.isNoetherianObject_of_faithful_preservesMono.{v,
    u}
  {A : Type u}
  [CategoryTheory.Category.{v, u} A]
  {C : Type u}
  [CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor A C)
  [F.Full] [F.Faithful]
  [F.PreservesMonomorphisms] {E : A}
  [CategoryTheory.IsNoetherianObject
      (F.obj E)] :
  CategoryTheory.IsNoetherianObject E

Something wrong, better idea? Suggest a change

5.42. isStrictArtinianObject_of_faithful_map_strictMono🔗

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

Proof: Map descending chains of strict subobjects in \mathcal{A} to descending chains of subobjects in \mathcal{C} via the injective monotone strict-subobject image map, then use the Artinian hypothesis in \mathcal{C} and injectivity.

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

Something wrong, better idea? Suggest a change

5.43. isStrictNoetherianObject_of_faithful_map_strictMono🔗

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

Proof: Map ascending chains of strict subobjects in \mathcal{A} to ascending chains of subobjects in \mathcal{C} via the injective monotone strict-subobject image map, then use the Noetherian hypothesis in \mathcal{C} and injectivity.

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

Something wrong, better idea? Suggest a change