comp

Mathlib.CategoryTheory.Functor.FullyFaithful

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Full.comp

English

If F and G are full, then F ⋙ G is full.

Русский

Если F и G полно, то F ⋙ G полно.

LaTeX

$$$[Full F]\,[Full G] \Rightarrow Full(F \circ G)$$$

Lean4

instance comp [Full F] [Full G] : Full (F ⋙ G) where map_surjective f := ⟨F.preimage (G.preimage f), by simp⟩

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

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

Разделы

Аффилиация

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