essImageInclusion

Mathlib.CategoryTheory.EssentialImage

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.essImageInclusion

Lean4

/-- The essential image as a subcategory has a fully faithful inclusion into the target category. -/
@[deprecated "use F.essImage.ι" (since := "2025-03-04")]
def essImageInclusion (F : C ⥤ D) : F.EssImageSubcategory ⥤ D :=
  F.essImage.ι

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

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

Разделы

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

Аффилиация

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