map_mk — Mathlib

English

Let J be a small category and F: J ⥤ MonCat a diagram. In the colimit of F, the element represented by (k, F.map f x) is equal to the element represented by (j, x) for any morphism f: j → k and x ∈ F.obj j.

Русский

Пусть J — маленькая категория и F : J ⥤ MonCat — диаграмма. В колимите диаграммы F элемент, представленный парой (k, F.map f x) равен элементу, представленному парой (j, x) при любом морфизме f: j → k и элементе x ∈ F.obj j.

LaTeX

$$$M.mk F \langle k, F.map f x \rangle = M.mk F \langle j, x \rangle$$$

Lean4

@[to_additive]
theorem map_mk {j k : J} (f : j ⟶ k) (x : F.obj j) : M.mk F ⟨k, F.map f x⟩ = M.mk F ⟨j, x⟩ :=
  M.mk_eq _ _ _ ⟨k, 𝟙 _, f, by simp⟩

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