hasForget

Mathlib.CategoryTheory.ConcreteCategory.BundledHom

URI: https://scilib.ai/kg/mathlib#CategoryTheory.BundledHom.hasForget

Lean4

/-- A category given by `BundledHom` is a concrete category. -/
instance hasForget : HasForget.{u} (Bundled c)
    where
  forget :=
    { obj := fun X => X
      map := fun {X Y} f => 𝒞.toFun X.str Y.str f
      map_id := fun X => 𝒞.id_toFun X.str
      map_comp := fun f g => by erw [𝒞.comp_toFun]; rfl }
  forget_faithful := { map_injective := by (intros; apply 𝒞.hom_ext) }

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

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

Разделы

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

Аффилиация

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