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
- 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 StrongMonoCategory
and StrongEpiCategory
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 #
A strong epimorphism f
is an epimorphism which has the left lifting property
with respect to monomorphisms.
- epi : CategoryTheory.Epi f
The epimorphism condition on
f
- llp : ∀ ⦃X Y : C⦄ (z : X ⟶ Y) [inst : CategoryTheory.Mono z], CategoryTheory.HasLiftingProperty f z
The left lifting property with respect to all monomorphism
Instances
A strong monomorphism f
is a monomorphism which has the right lifting property
with respect to epimorphisms.
- mono : CategoryTheory.Mono f
The monomorphism condition on
f
- rlp : ∀ ⦃X Y : C⦄ (z : X ⟶ Y) [inst : CategoryTheory.Epi z], CategoryTheory.HasLiftingProperty z f
The right lifting property with respect to all epimorphisms
Instances
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.
A strong epi category is a category in which every epimorphism is strong.
- strongEpi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [inst : CategoryTheory.Epi f], CategoryTheory.StrongEpi f
A strong epi category is a category in which every epimorphism is strong.
Instances
A strong mono category is a category in which every monomorphism is strong.
- strongMono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [inst : CategoryTheory.Mono f], CategoryTheory.StrongMono f
A strong mono category is a category in which every monomorphism is strong.