Mathlib Map

Structures · Category theory

CategoryTheory.ObjectProperty.IsSerreClass

A Serre class in an abelian category consists of a predicate which holds for the zero object and is closed under subobjects, quotients, extensions.

Defined in
Mathlib.CategoryTheory.Abelian.SerreClass.Basic
Shape
One type argument

Extends4

Extended by0

Nothing extends this class yet.

Concrete types that are instances1

  • AddCommGrpCat

How is a type an instance?

Loading the hierarchy index…

Assumed by89

Ancestors4