toEssImage — Mathlib

English

If F: C → D is faithful, then the induced functor F^{essImage}: C → EssImage(F) is faithful.

Русский

Если F: C → D является верным функтором, то индуцированный функтор в эссенциальное изображение F является верным.

LaTeX

$$$\operatorname{Faithful}(F) \Rightarrow \operatorname{Faithful}(F^{\mathrm{essImage}})$$$

Lean4

/-- The induced functor of a faithful functor is faithful. -/
instance toEssImage (F : C ⥤ D) [Faithful F] : Faithful F.toEssImage :=
  by
  dsimp only [Functor.toEssImage]
  infer_instance

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