instFullCompPostOfFaithful

Mathlib.CategoryTheory.Comma.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Comma.instFullCompPostOfFaithful

English

If F is essentially surjective, then post L R F is essentially surjective.

Русский

Если F эссенциально сюръективна, то post L R F эссенциально сюръективна.

LaTeX

$$$F\text{ EssSurj} \Rightarrow (\text{post } L R F)\text{ EssSurj}$$$

Lean4

instance (L : A ⥤ T) (R : B ⥤ T) (F : T ⥤ C) [F.Faithful] : (post L R F).Full :=
  Functor.Full.of_iso (postIso L R F).symm

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

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

Разделы

Аффилиация

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