Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-10 06:39 e8ad2e38

View on Github →

feat(category_theory/limits): the pullback of a monomorphism is a monomorphism (#2113)

The pullback of a monomorphism is a monomorphism
The pushout of an epimorphism is an epimorphism
Fix a proof
renaming

Estimated changes

Modified src/category_theory/limits/shapes/constructions/binary_products.lean

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

added theorem category_theory.limits.pullback.hom_ext

added theorem category_theory.limits.pullback_cone.equalizer_ext

added theorem category_theory.limits.pushout.hom_ext

added theorem category_theory.limits.pushout_cocone.coequalizer_ext