Mathlib v3 is deprecated. Go to Mathlib v4

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