mathlib documentation

category_theory.limits.shapes.strong_epi

Strong epimorphisms #

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

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 #

theorem category_theory.strong_epi.mk' {C : Type u} [category_theory.category C] {P Q : C} {f : P Q} [category_theory.epi f] (hf : (X Y : C) (z : X Y), category_theory.mono z (u : P X) (v : Q Y) (sq : category_theory.comm_sq u f z v), sq.has_lift) :
@[class]
structure category_theory.strong_mono {C : Type u} [category_theory.category C] {P Q : C} (f : P Q) :
Prop

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} [category_theory.category C] {P Q : C} {f : P Q} [category_theory.mono f] (hf : (X Y : C) (z : X Y), category_theory.epi z (u : X P) (v : Y Q) (sq : category_theory.comm_sq u z f v), sq.has_lift) :

The composition of two strong epimorphisms is a strong epimorphism.

The composition of two strong monomorphisms is a strong monomorphism.

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

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

@[protected, instance]

An isomorphism is in particular a strong epimorphism.

@[protected, instance]

An isomorphism is in particular a strong monomorphism.

A strong epimorphism that is a monomorphism is an isomorphism.

A strong monomorphism that is an epimorphism is an isomorphism.

@[class]

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

Instances of this typeclass
@[class]

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

Instances of this typeclass