Theorems · Theorem · category theory
CategoryTheory.Functor.obj_mem_essImage
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor D C) (Y : D), F.essImage (F.obj Y)An object in the image is in the essential image.
- Defined in
- Mathlib.CategoryTheory.EssentialImage
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- CategoryTheory.Functorstatement and proof · cited by 16,252
- CategoryTheory.Iso.reflproof · cited by 727
- CategoryTheory.Functor.essImagestatement · cited by 82
Cited by9
Results whose statement or proof uses this declaration.
- CategoryTheory.Functor.toEssImageproof · cited by 10
- CategoryTheory.Functor.toEssImageCompιproof · cited by 2
- CategoryTheory.mem_essImage_of_counit_isSplitEpiproof · cited by 0
- CategoryTheory.mem_essImage_of_unit_isSplitMonoproof · cited by 0
- CategoryTheory.Functor.essSurj_of_surjproof · cited by 0
- CategoryTheory.Functor.toEssImageCompι_hom_appstatement · cited by 0
- CategoryTheory.Functor.toEssImageCompι_inv_appstatement · cited by 0
- CategoryTheory.Functor.toEssImage_map_homstatement · cited by 0
- CategoryTheory.Triangulated.TStructure.ιHeart_obj_memproof · cited by 0