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

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} [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 of this typeclass
@[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 such that every commutative square with f at the bottom and an epimorphism at the top has a lift.

Instances of this typeclass
@[protected, instance]
@[protected, instance]

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