reflectsIsomorphisms

Mathlib.CategoryTheory.Functor.ReflectsIso.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.FullyFaithful.reflectsIsomorphisms

English

A fully faithful functor reflects isomorphisms.

Русский

Полностью точный функтор отражает изоморфизмы.

LaTeX

$$$F\\text{ is FullyFaithful} \\Rightarrow F.ReflectsIsomorphisms.$$$

Lean4

theorem reflectsIsomorphisms {F : C ⥤ D} (hF : F.FullyFaithful) : F.ReflectsIsomorphisms where
  reflects _ _ := hF.isIso_of_isIso_map _

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

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

Разделы

Аффилиация

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