mk_map — Mathlib

English

The map morphism identifies how the colimit representatives relate along a morphism f: j → k in J.

Русский

Отображение mk фиксирует, как представители пределa соотносятся по морфизмам f: j → k в J.

LaTeX

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

Lean4

theorem mk_map {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⟩

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