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 ≫ gis a strong epimorphism, then so isg, - if
fis 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][borceux-vol1]
@[class]
structure
category_theory.strong_epi
{C : Type u}
[category_theory.category C]
{P Q : C} :
(P ⟶ Q) → Type (max u v)
- 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.
@[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] :
Equations
def
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.
Equations
- category_theory.strong_epi_comp f g = {epi := _, has_lift := λ (X Y : C) (u : P ⟶ X) (v : R ⟶ Y) (z : X ⟶ Y) (_inst_2_1 : category_theory.mono z) (h : u ≫ z = (f ≫ g) ≫ v), let w : Q ⟶ X := category_theory.arrow.lift (category_theory.arrow.hom_mk' _) in {lift := category_theory.arrow.lift (category_theory.arrow.hom_mk' _) (category_theory.strong_epi.has_lift _), fac_left := _, fac_right := _}}
def
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)] :
If f ≫ g is a strong epimorphism, then so is g.
Equations
- category_theory.strong_epi_of_strong_epi f g = {epi := _, has_lift := λ (X Y : C) (u : Q ⟶ X) (v : R ⟶ Y) (z : X ⟶ Y) (_inst_2_1 : category_theory.mono z) (h : u ≫ z = g ≫ v), {lift := category_theory.arrow.lift (category_theory.arrow.hom_mk' _) (category_theory.strong_epi.has_lift _), fac_left := _, fac_right := _}}
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] :
A strong epimorphism that is a monomorphism is an isomorphism.