mathlib documentation

category_theory.limits.shapes.strong_epi

Strong epimorphisms

In this file, we define strong epimorphisms. A strong epimorphism is an epimorphism f, such that for every commutative square with f at the top and a monomorphism at the bottom, there is a diagonal morphism making the two triangles commute. This lift is necessarily unique (as shown in comma.lean).

Main results

Besides the definition, we show that

Future work

There is also the dual notion of strong monomorphism.

References

@[class]
structure category_theory.strong_epi {C : Type u} [category_theory.category C] {P Q : C} :
(P Q) → Prop

A strong epimorphism f is an epimorphism such that every commutative square with f at the top and a monomorphism at the bottom has a lift.

Instances

The composition of two strong epimorphisms is a strong epimorphism.

If f ≫ g is a strong epimorphism, then so is g.

@[instance]

An isomorphism is in particular a strong epimorphism.