equivalence

Mathlib.CategoryTheory.Limits.Indization.Category

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Ind.equivalence

Lean4

/-- The defining properties of `Ind C` are that its morphisms live in `v` and that it is equivalent
to the full subcategory of `Cᵒᵖ ⥤ Type v` containing the ind-objects. -/
noncomputable def equivalence : Ind C ≌ ObjectProperty.FullSubcategory (IsIndObject (C := C)) :=
  (ShrinkHoms.equivalence _).symm

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

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

Разделы

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

Аффилиация

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