Theorems · Definition · category theory

CategoryTheory.ObjectProperty.isoModSerre

{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 isomorphisms modulo a Serre class: given a Serre class P : ObjectProperty C, this is the class of morphisms f such that kernel f and cokernel f satisfy P.

Defined in

Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Cited by

50 results in Mathlib

Foundations

Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.ObjectProperty.IsSerreClass