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} (f : 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.

A strong epimorphism that is a monomorphism is an isomorphism.