mkHasForget₂

Mathlib.CategoryTheory.ConcreteCategory.BundledHom

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

Lean4

/-- A version of `HasForget₂.mk'` for categories defined using `@BundledHom`. -/
def mkHasForget₂ {d : Type u → Type u} {hom_d : ∀ ⦃α β : Type u⦄ (_ : d α) (_ : d β), Type u} [BundledHom hom_d]
    (obj : ∀ ⦃α⦄, c α → d α) (map : ∀ {X Y : Bundled c}, (X ⟶ Y) → (Bundled.map (@obj) X ⟶ (Bundled.map (@obj) Y)))
    (h_map : ∀ {X Y : Bundled c} (f : X ⟶ Y), ⇑(map f) = ⇑f) : HasForget₂ (Bundled c) (Bundled d) :=
  HasForget₂.mk' (Bundled.map @obj) (fun _ => rfl) map
    (by
      intro X Y f
      rw [heq_eq_eq, forget_map_eq_coe, forget_map_eq_coe, h_map f])

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

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

Разделы

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

Аффилиация

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