instHasInitial — Mathlib

English

In the category Grp_ C of group objects in a cartesian monoidal category, the trivial group object on the terminal object of C is an initial object. Thus Grp_ C has an initial object.

Русский

В категории Grp_ C объектов группы над C тривиальный групповый объект над терминальным объектом C является начальным объектом. Следовательно, Grp_ C имеет начальное объект.

LaTeX

$$$ \mathrm{HasInitial}(\Grp_C) $$$

Lean4

instance : HasInitial (Grp_ C) :=
  hasInitial_of_unique (trivial C)

Похожие утверждения