instFullObjCompPostOfFaithful

Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.StructuredArrow.instFullObjCompPostOfFaithful

← MathLib Explorer

English

If G is faithful, then (post S F G) is full.

Русский

Если G вернообразна, то (post S F G) полно.

LaTeX

$$$(\mathrm{post}\ S\ F\ G).Full \quad\text{when } G\text{ is faithful}$$$

Lean4

instance (S : C) (F : B ⥤ C) (G : C ⥤ D) [G.Faithful] : (post S F G).Full where
  map_surjective f := ⟨homMk f.right (G.map_injective (by simpa using f.w.symm)), by simp⟩

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

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

Разделы

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

Аффилиация

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