# mathlib3documentation

category_theory.limits.shapes.strong_epi

# Strong epimorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file, we define strong epimorphisms. A strong epimorphism is an epimorphism f which has the (unique) left lifting property with respect to monomorphisms. Similarly, a strong monomorphisms in a monomorphism which has the (unique) right lifting property with respect to epimorphisms.

## 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

We also define classes strong_mono_category and strong_epi_category for categories in which every monomorphism or epimorphism is strong, and deduce that these categories are balanced.

## TODO #

Show that the dual of a strong epimorphism is a strong monomorphism, and vice versa.

## References #

@[class]
structure category_theory.strong_epi {C : Type u} {P Q : C} (f : P Q) :
Prop
• epi :
• llp : ⦃X Y : C⦄ (z : X Y) [_inst_2 : ,

A strong epimorphism f is an epimorphism which has the left lifting property with respect to monomorphisms.

Instances of this typeclass
theorem category_theory.strong_epi.mk' {C : Type u} {P Q : C} {f : P Q} (hf : (X Y : C) (z : X Y), (u : P X) (v : Q Y) (sq : v), sq.has_lift) :
@[class]
structure category_theory.strong_mono {C : Type u} {P Q : C} (f : P Q) :
Prop
• mono :
• rlp : ⦃X Y : C⦄ (z : X Y) [_inst_2 : ,

A strong monomorphism f is a monomorphism which has the right lifting property with respect to epimorphisms.

Instances of this typeclass
theorem category_theory.strong_mono.mk' {C : Type u} {P Q : C} {f : P Q} (hf : (X Y : C) (z : X Y), (u : X P) (v : Y Q) (sq : v), sq.has_lift) :
@[protected, instance]
def category_theory.epi_of_strong_epi {C : Type u} {P Q : C} (f : P Q)  :
@[protected, instance]
def category_theory.mono_of_strong_mono {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_mono_comp {C : Type u} {P Q R : C} (f : P Q) (g : Q R)  :

The composition of two strong monomorphisms is a strong monomorphism.

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.

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

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

@[protected, 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.

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

An isomorphism is in particular a strong monomorphism.

theorem category_theory.strong_epi.of_arrow_iso {C : Type u} {A B A' B' : C} {f : A B} {g : A' B'}  :
theorem category_theory.strong_mono.of_arrow_iso {C : Type u} {A B A' B' : C} {f : A B} {g : A' B'}  :
theorem category_theory.strong_epi.iff_of_arrow_iso {C : Type u} {A B A' B' : C} {f : A B} {g : A' B'}  :
theorem category_theory.strong_mono.iff_of_arrow_iso {C : Type u} {A B A' B' : C} {f : A B} {g : A' B'}  :
theorem 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.

theorem category_theory.is_iso_of_epi_of_strong_mono {C : Type u} {P Q : C} (f : P Q)  :

A strong monomorphism that is an epimorphism is an isomorphism.

@[class]
structure category_theory.strong_epi_category (C : Type u)  :
Prop
• strong_epi_of_epi : {X Y : C} (f : X Y) [_inst_2 : ,

A strong epi category is a category in which every epimorphism is strong.

Instances of this typeclass
@[class]
structure category_theory.strong_mono_category (C : Type u)  :
Prop
• strong_mono_of_mono : {X Y : C} (f : X Y) [_inst_2 : ,

A strong mono category is a category in which every monomorphism is strong.

Instances of this typeclass
theorem category_theory.strong_epi_of_epi {C : Type u} {P Q : C} (f : P Q)  :
theorem category_theory.strong_mono_of_mono {C : Type u} {P Q : C} (f : P Q)  :
@[protected, instance]
@[protected, instance]