# mathlibdocumentation

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

• the composition of two strong epimorphisms is a strong epimorphism,
• if f ≫ g is a strong epimorphism, then so is g,
• if f is both a strong epimorphism and a monomorphism, then it is an isomorphism

## Future work

There is also the dual notion of strong monomorphism.

## References

• [F. Borceux, Handbook of Categorical Algebra 1][borceux-vol1]
@[class]
structure category_theory.strong_epi {C : Type u} {P Q : C} :
(P Q) → Prop
• epi :
• has_lift : ∀ {X Y : C} {u : P X} {v : Q Y} {z : X Y} [_inst_2 : (h : u z = f v),

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
@[instance]
def category_theory.epi_of_strong_epi {C : Type u} {P Q : C} (f : P Q)  :

theorem category_theory.strong_epi_comp {C : Type u} {P Q R : C} (f : P Q) (g : Q R)  :

The composition of two strong epimorphisms is a strong epimorphism.

theorem category_theory.strong_epi_of_strong_epi {C : Type u} {P Q R : C} (f : P Q) (g : Q R) [category_theory.strong_epi (f g)] :

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

@[instance]
def category_theory.strong_epi_of_is_iso {C : Type u} {P Q : C} (f : P Q)  :

An isomorphism is in particular a strong epimorphism.

def category_theory.is_iso_of_mono_of_strong_epi {C : Type u} {P Q : C} (f : P Q)  :

A strong epimorphism that is a monomorphism is an isomorphism.

Equations