Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-09 14:27 62abc4d5

View on Github →

feat(category_theory): images (#2100)

feat(category_theory): images
oops, forgot to add file
Update src/category_theory/category/default.lean Co-Authored-By: Johan Commelin johan@commelin.net
some improvements
linting
oops
Update src/category_theory/limits/shapes/images.lean

Estimated changes

Modified src/category_theory/category/default.lean

modified theorem category_theory.cancel_epi

added theorem category_theory.cancel_epi_id

modified theorem category_theory.cancel_mono

added theorem category_theory.cancel_mono_id

added theorem category_theory.epi_of_epi

added theorem category_theory.epi_of_epi_fac

added theorem category_theory.mono_of_mono

added theorem category_theory.mono_of_mono_fac

Modified src/category_theory/limits/shapes/equalizers.lean

deleted theorem category_theory.limits.coequalizer.π_epi

deleted theorem category_theory.limits.equalizer.ι_mono

Created src/category_theory/limits/shapes/images.lean

added def category_theory.limits.factor_thru_image

added theorem category_theory.limits.has_image.uniq

added theorem category_theory.limits.image.as_c

added theorem category_theory.limits.image.as_ι

added def category_theory.limits.image.c

added theorem category_theory.limits.image.c_ι

added theorem category_theory.limits.image.fac

added def category_theory.limits.image.is_image

added def category_theory.limits.image.lift

added theorem category_theory.limits.image.lift_fac

added def category_theory.limits.image.mono_factorisation

added def category_theory.limits.image.ι

added def category_theory.limits.image

added def category_theory.limits.image_mono_iso_source

added theorem category_theory.limits.image_mono_iso_source_hom_self

added theorem category_theory.limits.image_mono_iso_source_inv_ι

added def category_theory.limits.is_image.iso_ext

added def category_theory.limits.is_image.self

added structure category_theory.limits.is_image

added theorem category_theory.limits.mono_factorisation.ext

added def category_theory.limits.mono_factorisation.self

added structure category_theory.limits.mono_factorisation