Theorems · Definition · category theory

CategoryTheory.ObjectProperty.monoModSerre

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (P : CategoryTheory.ObjectProperty C) → [P.IsSerreClass] → CategoryTheory.MorphismProperty C

The class of monomorphisms modulo a Serre class: given a Serre class P : ObjectProperty C, this is the class of morphisms f such that kernel f satisfies P.

Defined in

Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Cited by

16 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.ObjectProperty.IsSerreClass