functorCategory_monomorphisms — Mathlib

English

Let C be a category and J any category. The collection of monomorphisms in C, when viewed in the functor category J ⥤ C, coincides with the monomorphisms defined pointwise in J ⥤ C.

Русский

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

LaTeX

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

Lean4

theorem functorCategory_monomorphisms [HasPullbacks C] : (monomorphisms C).functorCategory J = monomorphisms (J ⥤ C) :=
  by
  ext _ _ f
  simp only [functorCategory, monomorphisms.iff, NatTrans.mono_iff_mono_app]

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