instEpiAppOfFunctor

Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instEpiAppOfFunctor

English

If f is epi, then for each k, the morphism f.app k is epi.

Русский

Если f — эпиморфизм, то для каждого k морфизм f.app k также эпиморфизм.

LaTeX

$$$[\\mathrm{Epi}\, f] (k) : \\; Epi (f.app k).$$$

Lean4

instance [Epi f] (k : K) : Epi (f.app k) :=
  inferInstanceAs (Epi (((evaluation K C).obj k).map f))

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

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

Разделы

Аффилиация

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