skeletonEquivalence

Mathlib.CategoryTheory.Skeletal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.skeletonEquivalence

Lean4

/-- The equivalence between the skeleton and the category itself. -/
@[simps]
noncomputable def skeletonEquivalence : Skeleton C ≌ C
    where
  functor := fromSkeleton C
  inverse := toSkeletonFunctor C
  unitIso :=
    NatIso.ofComponents (fun X ↦ InducedCategory.isoMk (Nonempty.some <| Quotient.mk_out X.out).symm) fun _ ↦
      .symm <| Iso.inv_hom_id_assoc _ _
  counitIso := NatIso.ofComponents preCounitIso
  functor_unitIso_comp _ := Iso.inv_hom_id _

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

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

Разделы

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

Аффилиация

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