colimit_one_eq — Mathlib

English

For a small filtered category J and a functor F: J ⥤ GrpCat, the unit element of the filtered colimit G F is represented by the class of (j,1) for any index j.

Русский

Для малой фильтрованной категории J и фактор-функторa F: J ⥤ GrpCat единица в колимите задаётся представлением класса (j,1) для любого j.

LaTeX

$$$(1 : G.{v, u} F) = G.mk F ⟨j, 1⟩$$$

Lean4

@[to_additive]
theorem colimit_one_eq (j : J) : (1 : G.{v, u} F) = G.mk F ⟨j, 1⟩ :=
  MonCat.FilteredColimits.colimit_one_eq _ _

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