Theorems · Definition · category theory

CategoryTheory.Functor.objPreimage

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

Given an essentially surjective functor, we can find a preimage for every object Y in the codomain. Applying the functor to this preimage will yield an object isomorphic to Y, see obj_obj_preimage_iso.

Defined in

Mathlib.CategoryTheory.EssentialImage

Cited by

49 results in Mathlib

Foundations

Depth 10 from the axioms · uses Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.EssSurj