ofFullyFaithfulToGroupoid

Mathlib.CategoryTheory.Groupoid

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Groupoid.ofFullyFaithfulToGroupoid

Lean4

/-- A category equipped with a fully faithful functor to a groupoid is fully faithful -/
def ofFullyFaithfulToGroupoid {C : Type*} [𝒞 : Category C] {D : Type u} [Groupoid.{v} D] (F : C ⥤ D)
    (h : F.FullyFaithful) : Groupoid C :=
  { 𝒞 with
    inv f := h.preimage <| Groupoid.inv (F.map f)
    inv_comp
      f := by
      apply h.map_injective
      simp
    comp_inv
      f := by
      apply h.map_injective
      simp }

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

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

Разделы

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

Аффилиация

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