Mathlib Map

Structures · Category theory

CategoryTheory.MonObj

A monoid object internal to a monoidal category. When the monoidal category is preadditive, this is also sometimes called an "algebra object".

Defined in
Mathlib.CategoryTheory.Monoidal.Mon
Shape
One type argument · adds one, mul, one_mul, mul_one, mul_assoc
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by3

Forgetful instances

Every CategoryTheory.MonObj is also a

Concrete types that are instances6

  • CategoryTheory.Functor
  • CategoryTheory.Over
  • CategoryTheory.Grp
  • CategoryTheory.Mon
  • CategoryTheory.MonoidalOpposite
  • Opposite

How is a type an instance?

Loading the hierarchy index…

Assumed by263

Ancestors18