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 #

source
@[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
source
@[instance]
def category_theory.epi_of_strong_epi {C : Type u} [category_theory.category C] {P Q : C} (f : P ⟶ Q) [category_theory.strong_epi f] :
category_theory.epi f
source
theorem category_theory.strong_epi_comp {C : Type u} [category_theory.category C] {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) [category_theory.strong_epi f] [category_theory.strong_epi g] :
category_theory.strong_epi (f ≫ g)

The composition of two strong epimorphisms is a strong epimorphism.

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

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

source
@[instance]
def category_theory.strong_epi_of_is_iso {C : Type u} [category_theory.category C] {P Q : C} (f : P ⟶ Q) [category_theory.is_iso f] :
category_theory.strong_epi f

An isomorphism is in particular a strong epimorphism.

source
theorem category_theory.is_iso_of_mono_of_strong_epi {C : Type u} [category_theory.category C] {P Q : C} (f : P ⟶ Q) [category_theory.mono f] [category_theory.strong_epi f] :
category_theory.is_iso f

A strong epimorphism that is a monomorphism is an isomorphism.