of_comp_iso

Mathlib.CategoryTheory.Functor.FullyFaithful

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Faithful.of_comp_iso

English

If F is faithful and F ≅ F', then F' is faithful.

Русский

Если F верен, и F изоморфен F', то F' верен.

LaTeX

$$$[F.Faithful] (\alpha : F \cong F') \Rightarrow F'.Faithful$$$

Lean4

theorem of_comp_iso {H : C ⥤ E} [H.Faithful] (h : F ⋙ G ≅ H) : F.Faithful :=
  @Faithful.of_comp _ _ _ _ _ _ F G (Faithful.of_iso h.symm)

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

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

Разделы

Аффилиация

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