f

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.f

Lean4

/-- The obvious morphism `colimit (kernel (g y)) ⟶ X` (which is an epimorphism
if `J` is filtered, see `epi_f`.). -/
noncomputable def f : colimit (kernel (g y)) ⟶ X :=
  IsColimit.map (colimit.isColimit _) (constCocone _ X) (kernel.ι _)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru