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 isg
, - 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 #
- 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.
- mono : category_theory.mono f
- has_lift : ∀ {X Y : C} {u : X ⟶ P} {v : Y ⟶ Q} {z : X ⟶ Y} [_inst_2 : category_theory.epi z] (h : u ≫ f = z ≫ v), category_theory.arrow.has_lift (category_theory.arrow.hom_mk' h)
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
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
.
An isomorphism is in particular a strong epimorphism.
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.
- strong_epi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [_inst_2 : category_theory.epi f], category_theory.strong_epi f
A strong epi category is a category in which every epimorphism is strong.
Instances of this typeclass
- strong_mono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [_inst_2 : category_theory.mono f], category_theory.strong_mono f
A strong mono category is a category in which every monomorphism is strong.