Mathlib Map

Structures · Category theory

CategoryTheory.Limits.HasZeroMorphisms

A category "has zero morphisms" if there is a designated "zero morphism" in each morphism space, and compositions of zero morphisms with anything give the zero morphism.

Defined in
Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Shape
One type argument · adds zero, comp_zero, zero_comp

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by1

Concrete types that are instances16

  • CategoryTheory.Functor
  • CategoryTheory.Discrete
  • CategoryTheory.Grp
  • HomologicalComplex
  • Action
  • CategoryTheory.Mon
  • CategoryTheory.ObjectProperty.FullSubcategory
  • CategoryTheory.GradedObject
  • CategoryTheory.AddGrp
  • CategoryTheory.AddMon
  • CategoryTheory.ShortComplex
  • SemimoduleCat
  • CategoryTheory.DifferentialObject
  • SemiNormedGrp
  • SemiNormedGrp₁
  • Opposite

How is a type an instance?

Loading the hierarchy index…

Assumed by4,633

Ancestors0

No ancestors.