mk_surjective — Mathlib

English

The canonical projection into the colimit, given by mk, is surjective onto each colimit object in the filtered colimit construction.

Русский

Каноническое отображение mk на конструкторе фильтрованных пределом достижимо до каждого элемента колимита.

LaTeX

$$$$ \\exists j\\, \\exists x\\ (\\text{Mk } F \\langle j,x\\rangle = m) $$$$

Lean4

theorem mk_surjective (m : M F) : ∃ (j : J) (x : F.obj j), M.mk F ⟨j, x⟩ = m :=
  (F ⋙ forget (ModuleCat R)).ιColimitType_jointly_surjective m

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