Commit 2020-04-17 05:53 0567b7fa

View on Github →

feat(category_theory/limits): strong epimorphisms and strong epi-mono factorizations (#2433) This PR contains the changes I mentioned in #2374. It contains:

the definition of a lift of a commutative square
the definition of a strong epimorphism
a proof that every regular epimorphism is strong
the definition of a strong epi-mono factorization
the class has_strong_epi_images
the construction has_strong_epi_images -> has_image_maps
a small number of changes which should have been part of #2423

Estimated changes

Modified src/category_theory/comma.lean

added theorem category_theory.arrow.lift.fac_left

added theorem category_theory.arrow.lift.fac_right

added def category_theory.arrow.lift

added theorem category_theory.arrow.lift_mk'_left

added theorem category_theory.arrow.lift_mk'_right

added theorem category_theory.arrow.w

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

added theorem category_theory.limits.image.fac_lift

added theorem category_theory.limits.is_image.fac_lift

added def category_theory.limits.strong_epi_mono_factorisation.to_mono_is_image

added structure category_theory.limits.strong_epi_mono_factorisation

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

added def category_theory.limits.cokernel_cofork.is_colimit.desc'

deleted def category_theory.limits.cokernel_cofork.is_limit.desc'

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

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

added def category_theory.normal_epi.desc'

added def category_theory.normal_mono.lift'

added def category_theory.regular_epi.desc'

added def category_theory.regular_mono.lift'

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

added def category_theory.mono_strong_epi_is_iso

added def category_theory.strong_epi_comp

added def category_theory.strong_epi_of_strong_epi