Commit 2023-01-01 13:25 ba128cbf

View on Github →

feat: port CategoryTheory.EssentialImage (#1132)

depends on: #1126 Notes:

some instances are not derived automatically by the syntax deriving, https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/deriving.20instances/near/317057641
the dot notation does not seem to work for essImage.witness.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/EssentialImage.lean

added def CategoryTheory.Functor.EssImageSubcategory

added def CategoryTheory.Functor.essImage.getIso

added theorem CategoryTheory.Functor.essImage.ofIso

added theorem CategoryTheory.Functor.essImage.ofNatIso

added def CategoryTheory.Functor.essImage.witness

added def CategoryTheory.Functor.essImage

added def CategoryTheory.Functor.essImageInclusion

added theorem CategoryTheory.Functor.essImage_eq_of_natIso

added def CategoryTheory.Functor.objObjPreimageIso

added def CategoryTheory.Functor.objPreimage

added theorem CategoryTheory.Functor.obj_mem_essImage

added def CategoryTheory.Functor.toEssImage

added def CategoryTheory.Functor.toEssImageCompEssentialImageInclusion