Facts about epimorphisms and monomorphisms. #
The definitions of Epi
and Mono
are in CategoryTheory.Category
,
since they are used by some lemmas for Iso
, which is used everywhere.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
A split monomorphism is a morphism f : X ⟶ Y
with a given retraction retraction f : Y ⟶ X
such that f ≫ retraction f = 𝟙 X
.
Every split monomorphism is a monomorphism.
- retraction : Y ⟶ X
The map splitting
f
- id : CategoryTheory.CategoryStruct.comp f self.retraction = CategoryTheory.CategoryStruct.id X
f
composed withretraction
is the identity
Instances For
f
composed with retraction
is the identity
IsSplitMono f
is the assertion that f
admits a retraction
- exists_splitMono : Nonempty (CategoryTheory.SplitMono f)
There is a splitting
Instances
There is a splitting
A composition of SplitMono
is a SplitMono
. -
Equations
- smf.comp smg = { retraction := CategoryTheory.CategoryStruct.comp smg.retraction smf.retraction, id := ⋯ }
Instances For
A constructor for IsSplitMono f
taking a SplitMono f
as an argument
A split epimorphism is a morphism f : X ⟶ Y
with a given 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.
- section_ : Y ⟶ X
The map splitting
f
- id : CategoryTheory.CategoryStruct.comp self.section_ f = CategoryTheory.CategoryStruct.id Y
section_
composed withf
is the identity
Instances For
section_
composed with f
is the identity
IsSplitEpi f
is the assertion that f
admits a section
- exists_splitEpi : Nonempty (CategoryTheory.SplitEpi f)
There is a splitting
Instances
There is a splitting
A composition of SplitEpi
is a split SplitEpi
. -
Equations
- sef.comp seg = { section_ := CategoryTheory.CategoryStruct.comp seg.section_ sef.section_, id := ⋯ }
Instances For
A constructor for IsSplitEpi f
taking a SplitEpi f
as an argument
The chosen retraction of a split monomorphism.
Equations
- CategoryTheory.retraction f = ⋯.some.retraction
Instances For
The retraction of a split monomorphism has an obvious section.
Equations
- sm.splitEpi = { section_ := f, id := ⋯ }
Instances For
The retraction of a split monomorphism is itself a split epimorphism.
Equations
- ⋯ = ⋯
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
- CategoryTheory.section_ f = ⋯.some.section_
Instances For
The section of a split epimorphism has an obvious retraction.
Equations
- se.splitMono = { retraction := f, id := ⋯ }
Instances For
The section of a split epimorphism is itself a split monomorphism.
Equations
- ⋯ = ⋯
A split epi which is mono is an iso.
Every iso is a split mono.
Equations
- ⋯ = ⋯
Every iso is a split epi.
Equations
- ⋯ = ⋯
Every split mono is a mono.
Equations
- ⋯ = ⋯
Every split epi is an epi.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Every split mono whose retraction is mono is an iso.
Every split mono whose retraction is mono is an iso.
Every split epi whose section is epi 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
- CategoryTheory.Groupoid.ofTruncSplitMono all_split_mono = CategoryTheory.Groupoid.ofIsIso ⋯
Instances For
A split mono category is a category in which every monomorphism is split.
- isSplitMono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [inst : CategoryTheory.Mono f], CategoryTheory.IsSplitMono f
All monos are split
Instances
All monos are split
A split epi category is a category in which every epimorphism is split.
- isSplitEpi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [inst : CategoryTheory.Epi f], CategoryTheory.IsSplitEpi f
All epis are split
Instances
All epis are split
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
- sm.map F = { retraction := F.map sm.retraction, id := ⋯ }
Instances For
Split epimorphisms are also absolute epimorphisms.
Equations
- se.map F = { section_ := F.map se.section_, id := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯