concreteCategory

Mathlib.CategoryTheory.ConcreteCategory.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.InducedCategory.concreteCategory

Lean4

instance concreteCategory {C : Type u} {D : Type u'} [Category.{v'} D] {FD : D → D → Type*} {CD : D → Type w}
    [∀ X Y, FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory.{w} D FD] (f : C → D) :
    ConcreteCategory (InducedCategory D f) (fun X Y => FD (f X) (f Y))
    where
  hom := hom (C := D)
  ofHom := ofHom (C := D)
  hom_ofHom := hom_ofHom (C := D)
  ofHom_hom := ofHom_hom (C := D)
  comp_apply := ConcreteCategory.comp_apply (C := D)
  id_apply := ConcreteCategory.id_apply (C := D)

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

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

Разделы

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

Аффилиация

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