comp_id_monCat — Mathlib

English

For a diagram F: J ⥤ MonCat, the type ColimitType F carries a natural Monoid structure with operations defined by representatives of the colimit, i.e., multiplication is defined via quotienting by the colimit relation.

Русский

Для диаграммы F: J ⥤ MonCat тип ColimitType F имеет естественную структуру моноида, где умножение задаётся на уровнях отношения колимита через эквивалентности.

LaTeX

$$$\text{MonCat.Colimits.ColimitType}(F)$ является моноидом.$$

Lean4

@[to_additive (attr := deprecated "Proven by `simp only [MonCat.hom_id, comp_id]`" (since := "2025-01-28"))]
theorem comp_id_monCat {G : MonCat.{u}} {H : Type u} [Monoid H] (f : G →* H) : f.comp (MonCat.Hom.hom (𝟙 G)) = f := by
  simp

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