Facts about epimorphisms and monomorphisms. #
The definitions of epi
and mono
are in category_theory.category
,
since they are used by some lemmas for iso
, which is used everywhere.
A split monomorphism is a morphism f : X ⟶ Y
admitting a retraction retraction f : Y ⟶ X
such that f ≫ retraction f = 𝟙 X
.
Every split monomorphism is a monomorphism.
Instances of this typeclass
- category_theory.split_mono.of_iso
- category_theory.section_split_mono
- category_theory.functor.map.split_mono
- category_theory.limits.terminal.split_mono_from
- category_theory.limits.diag.category_theory.split_mono
- category_theory.limits.split_mono_sigma_ι
- category_theory.limits.split_mono_coprod_inl
- category_theory.limits.split_mono_coprod_inr
- category_theory.limits.biproduct.ι_mono
- category_theory.limits.biprod.inl_mono
- category_theory.limits.biprod.inr_mono
Instances of other typeclasses for category_theory.split_mono
- category_theory.split_mono.has_sizeof_inst
A split epimorphism is a morphism f : X ⟶ Y
admitting a section section_ f : Y ⟶ X
such that section_ f ≫ f = 𝟙 Y
.
(Note that section
is a reserved keyword, so we append an underscore.)
Every split epimorphism is an epimorphism.
Instances of this typeclass
- category_theory.split_epi.of_iso
- category_theory.retraction_split_epi
- category_theory.functor.map.split_epi
- category_theory.limits.initial.split_epi_to
- category_theory.limits.split_epi_pi_π
- category_theory.limits.split_epi_prod_fst
- category_theory.limits.split_epi_prod_snd
- category_theory.limits.biproduct.π_epi
- category_theory.limits.biprod.fst_epi
- category_theory.limits.biprod.snd_epi
Instances of other typeclasses for category_theory.split_epi
- category_theory.split_epi.has_sizeof_inst
The chosen retraction of a split monomorphism.
Equations
Instances for category_theory.retraction
The retraction of a split monomorphism is itself a split epimorphism.
Equations
- category_theory.retraction_split_epi f = {section_ := f, id' := _}
A split mono which is epi is an iso.
The chosen section of a split epimorphism.
(Note that section
is a reserved keyword, so we append an underscore.)
Equations
Instances for category_theory.section_
The section of a split epimorphism is itself a split monomorphism.
Equations
- category_theory.section_split_mono f = {retraction := f, id' := _}
A split epi which is mono is an iso.
Every iso is a split mono.
Equations
- category_theory.split_mono.of_iso f = {retraction := category_theory.inv f _inst_2, id' := _}
Every iso is a split epi.
Equations
- category_theory.split_epi.of_iso f = {section_ := category_theory.inv f _inst_2, id' := _}
Every split mono is a mono.
Every split epi is an epi.
Every split mono whose retraction is mono is an iso.
Every split epi whose section is epi is an iso.
A category where every morphism has a trunc
retraction is computably a groupoid.
Equations
- split_mono_of_mono : Π {X Y : C} (f : X ⟶ Y) [_inst_2 : category_theory.mono f], category_theory.split_mono f
A split mono category is a category in which every monomorphism is split.
Instances for category_theory.split_mono_category
- category_theory.split_mono_category.has_sizeof_inst
- split_epi_of_epi : Π {X Y : C} (f : X ⟶ Y) [_inst_2 : category_theory.epi f], category_theory.split_epi f
A split epi category is a category in which every epimorphism is split.
Instances of this typeclass
Instances of other typeclasses for category_theory.split_epi_category
- category_theory.split_epi_category.has_sizeof_inst
In a category in which every monomorphism is split, every monomorphism splits. This is not an instance because it would create an instance loop.
In a category in which every epimorphism is split, every epimorphism splits. This is not an instance because it would create an instance loop.
Split monomorphisms are also absolute monomorphisms.
Equations
- category_theory.functor.map.split_mono f F = {retraction := F.map (category_theory.retraction f), id' := _}
Split epimorphisms are also absolute epimorphisms.
Equations
- category_theory.functor.map.split_epi f F = {section_ := F.map (category_theory.section_ f), id' := _}