ofIso — Mathlib

English

Isomorphic functors have equal essential images: F ≅ F' implies essImage F = essImage F'.

Русский

Изоморфные функторы имеют одинаковые essImage: F ≅ F' ⇒ essImage F = essImage F'.

LaTeX

$$F ≅ F' ⇒ essImage F = essImage F'$$

Lean4

/-- Being in the essential image is a "hygienic" property: it is preserved under isomorphism. -/
theorem ofIso {Y Y' : D} (h : Y ≅ Y') (hY : essImage F Y) : essImage F Y' :=
  hY.imp fun _ => Nonempty.map (· ≪≫ h)

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