of_iso

Mathlib.CategoryTheory.Functor.EpiMono

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.preservesMonomorphisms.of_iso

English

If F preserves monomorphisms and F ≅ G, then G preserves monomorphisms.

Русский

Если F сохраняет мономорфизмы и F ≅ G, то G сохраняет мономорфизмы.

LaTeX

$$PreservesMonomorphisms F ⇒ PreservesMonomorphisms G$$

Lean4

theorem of_iso {F G : C ⥤ D} [PreservesMonomorphisms F] (α : F ≅ G) : PreservesMonomorphisms G :=
  of_natTrans α.inv

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

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

Разделы

Аффилиация

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