functorCategory_epimorphisms — Mathlib

English

Let C be a category and J any category. The collection of epimorphisms in C, transported to the functor category J ⥤ C, matches the epimorphisms defined pointwise in J ⥤ C.

Русский

Пусть C — категория и любая J; эпиморфизмы в C, перенесённые в категорию функторов J ⥤ C, соответствуют по определению эпиморфизмам в J ⥤ C.

LaTeX

$$$ (\mathrm{epimorphisms}\ C).\mathrm{functorCategory}\ J = \mathrm{epimorphisms}\ (J \;⥤\; C) $$$

Lean4

theorem functorCategory_epimorphisms [HasPushouts C] : (epimorphisms C).functorCategory J = epimorphisms (J ⥤ C) :=
  by
  ext _ _ f
  simp only [functorCategory, epimorphisms.iff, NatTrans.epi_iff_epi_app]

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