Mathlib Map

Structures · Category theory

CategoryTheory.Limits.HasZeroObject

A category "has a zero object" if it has an object which is both initial and terminal.

Defined in
Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Shape
One type argument · adds zero
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by1

Forgetful instances

Provided automatically by

Concrete types that are instances26

  • CategoryTheory.Functor
  • CategoryTheory.Discrete
  • ModuleCat
  • CategoryTheory.Grp
  • HomologicalComplex
  • CategoryTheory.Mon
  • AddCommGrpCat
  • CategoryTheory.ObjectProperty.FullSubcategory
  • Rep
  • CommGrpCat
  • GrpCat
  • AddGrpCat
  • HomotopyCategory
  • CategoryTheory.MorphismProperty.Localization
  • DerivedCategory
  • CategoryTheory.GradedObject
  • CategoryTheory.AddGrp
  • CategoryTheory.AddMon
  • SemimoduleCat
  • CategoryTheory.DifferentialObject
  • CategoryTheory.OppositeShift
  • CategoryTheory.MorphismProperty.Localization'
  • CategoryTheory.PullbackShift
  • SemiNormedGrp
  • SemiNormedGrp₁
  • Opposite

How is a type an instance?

Loading the hierarchy index…

Assumed by1,881

Ancestors0

No ancestors.