Theorems · Definition · category theory

CategoryTheory.Functor.essImage

{C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → CategoryTheory.ObjectProperty D

The essential image of a functor F consists of those objects in the target category which are isomorphic to an object in the image of the function F.obj. In other words, this is the closure under isomorphism of the function F.obj. This is the "non-evil" way of describing the image of a functor.

Defined in

Mathlib.CategoryTheory.EssentialImage

Cited by

82 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category