of_comp_faithful

Mathlib.CategoryTheory.Functor.FullyFaithful

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

← MathLib Explorer

English

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

Русский

Если F ⋙ G полно, а G верен, то F полно.

LaTeX

$$$[ Full (F \circ G) ] \land [ G.Faithful] \Rightarrow Full F$$$

Lean4

/-- If `F ⋙ G` is full and `G` is faithful, then `F` is full. -/
theorem of_comp_faithful [Full <| F ⋙ G] [G.Faithful] : Full F where
  map_surjective f := ⟨(F ⋙ G).preimage (G.map f), G.map_injective ((F ⋙ G).map_preimage _)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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