category

Mathlib.CategoryTheory.Widesubcategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.InducedWideCategory.category

Lean4

@[simps!]
instance category : Category (InducedWideCategory D F P)
    where
  Hom X Y := {f : F X ⟶ F Y | P f}
  id X := ⟨𝟙 (F X), P.id_mem (F X)⟩
  comp {_ _ _} f g := ⟨f.1 ≫ g.1, P.comp_mem _ _ f.2 g.2⟩

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

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

Разделы

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

Аффилиация

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