instIsEquivalenceMapOfIsIso

Mathlib.CategoryTheory.Comma.Over.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Over.instIsEquivalenceMapOfIsIso

English

If f is an isomorphism in T, then Over.map f is an equivalence of categories.

Русский

Если f — изоморфизм в T, то Over.map f является эквивалентностью категорий.

LaTeX

$$$\\operatorname{IsIso}(f) \\Rightarrow \\operatorname{IsEquivalence}(\\mathrm{Over.map} f)$$$

Lean4

instance [IsIso f] : (Over.map f).IsEquivalence :=
  (Over.mapIso <| asIso f).isEquivalence_functor

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

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

Разделы

Аффилиация

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