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

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

Future work #

There is also the dual notion of strong monomorphism.

References #

F. Borceux, Handbook of Categorical Algebra 1

source

@[class]

structure category_theory.strong_epi {C : Type u} [category_theory.category C] {P Q : C} (f : P ⟶ Q) :

Prop

epi : category_theory.epi f
has_lift : ∀ {X Y : C} {u : P ⟶ X} {v : Q ⟶ Y} {z : X ⟶ Y} [_inst_2 : category_theory.mono z] (h : u ≫ z = f ≫ v), category_theory.arrow.has_lift (category_theory.arrow.hom_mk' h)

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

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

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