ofNatIso — Mathlib

English

The map ι from the EssImage subcategory to D is injective on morphisms: if F.essImage.ι.map f = F.essImage.ι.map g then f = g.

Русский

Отображение ι из подсегмента EssImage в D инъективно на морфизмах: если F.essImage.ι.map f = F.essImage.ι.map g, то f = g.

LaTeX

$$F.essImage.ι.map f = F.essImage.ι.map g \Rightarrow f = g$$

Lean4

/-- If `Y` is in the essential image of `F` then it is in the essential image of `F'` as long as
`F ≅ F'`.
-/
theorem ofNatIso {F' : C ⥤ D} (h : F ≅ F') {Y : D} (hY : essImage F Y) : essImage F' Y :=
  hY.imp fun X => Nonempty.map fun t => h.symm.app X ≪≫ t

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