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

Equations