instIsEquivalenceFunctor

Mathlib.CategoryTheory.EssentiallySmall

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShrinkHoms.instIsEquivalenceFunctor

English

The ShrinkHoms construction yields an equivalence of categories.

Русский

Конструкция ShrinkHoms даёт эквивалентность категорий.

LaTeX

$$$(\mathrm{ShrinkHoms}.functor\, C).IsEquivalence$$$

Lean4

instance : (functor C).IsEquivalence :=
  (equivalence C).isEquivalence_functor

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

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

Разделы

Аффилиация

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