# 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.

instance CategoryTheory.unop_mono_of_epi {C : Type u₁} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (f : A B) :
Equations
• =
instance CategoryTheory.unop_epi_of_mono {C : Type u₁} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (f : A B) :
Equations
• =
instance CategoryTheory.op_mono_of_epi {C : Type u₁} [] {A : C} {B : C} (f : A B) :
Equations
• =
instance CategoryTheory.op_epi_of_mono {C : Type u₁} [] {A : C} {B : C} (f : A B) :
Equations
• =
theorem CategoryTheory.SplitMono.ext_iff {C : Type u₁} :
∀ {inst : } {X Y : C} {f : X Y} (x y : ), x = y x.retraction = y.retraction
theorem CategoryTheory.SplitMono.ext {C : Type u₁} :
∀ {inst : } {X Y : C} {f : X Y} (x y : ), x.retraction = y.retractionx = y
structure CategoryTheory.SplitMono {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
Type v₁

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.

Instances For
@[simp]
theorem CategoryTheory.SplitMono.id {C : Type u₁} [] {X : C} {Y : C} {f : X Y} (self : ) :

f composed with retraction is the identity

@[simp]
theorem CategoryTheory.SplitMono.id_assoc {C : Type u₁} [] {X : C} {Y : C} {f : X Y} (self : ) {Z : C} (h : X Z) :
class CategoryTheory.IsSplitMono {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

IsSplitMono f is the assertion that f admits a retraction

• exists_splitMono :

There is a splitting

Instances
theorem CategoryTheory.IsSplitMono.exists_splitMono {C : Type u₁} [] {X : C} {Y : C} {f : X Y} [self : ] :

There is a splitting

theorem CategoryTheory.IsSplitMono.mk' {C : Type u₁} [] {X : C} {Y : C} {f : X Y} (sm : ) :

A constructor for IsSplitMono f taking a SplitMono f as an argument

theorem CategoryTheory.SplitEpi.ext {C : Type u₁} :
∀ {inst : } {X Y : C} {f : X Y} (x y : ), x.section_ = y.section_x = y
theorem CategoryTheory.SplitEpi.ext_iff {C : Type u₁} :
∀ {inst : } {X Y : C} {f : X Y} (x y : ), x = y x.section_ = y.section_
structure CategoryTheory.SplitEpi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
Type v₁

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.

Instances For
@[simp]
theorem CategoryTheory.SplitEpi.id {C : Type u₁} [] {X : C} {Y : C} {f : X Y} (self : ) :

section_ composed with f is the identity

@[simp]
theorem CategoryTheory.SplitEpi.id_assoc {C : Type u₁} [] {X : C} {Y : C} {f : X Y} (self : ) {Z : C} (h : Y Z) :
class CategoryTheory.IsSplitEpi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

IsSplitEpi f is the assertion that f admits a section

• exists_splitEpi :

There is a splitting

Instances
theorem CategoryTheory.IsSplitEpi.exists_splitEpi {C : Type u₁} [] {X : C} {Y : C} {f : X Y} [self : ] :

There is a splitting

theorem CategoryTheory.IsSplitEpi.mk' {C : Type u₁} [] {X : C} {Y : C} {f : X Y} (se : ) :

A constructor for IsSplitEpi f taking a SplitEpi f as an argument

noncomputable def CategoryTheory.retraction {C : Type u₁} [] {X : C} {Y : C} (f : X Y) [hf : ] :
Y X

The chosen retraction of a split monomorphism.

Equations
• = .some.retraction
Instances For
@[simp]
theorem CategoryTheory.IsSplitMono.id_assoc {C : Type u₁} [] {X : C} {Y : C} (f : X Y) [hf : ] {Z : C} (h : X Z) :
@[simp]
theorem CategoryTheory.IsSplitMono.id {C : Type u₁} [] {X : C} {Y : C} (f : X Y) [hf : ] :
def CategoryTheory.SplitMono.splitEpi {C : Type u₁} [] {X : C} {Y : C} {f : X Y} (sm : ) :

The retraction of a split monomorphism has an obvious section.

Equations
• sm.splitEpi = { section_ := f, id := }
Instances For
instance CategoryTheory.retraction_isSplitEpi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

The retraction of a split monomorphism is itself a split epimorphism.

Equations
• =
theorem CategoryTheory.isIso_of_epi_of_isSplitMono {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

A split mono which is epi is an iso.

noncomputable def CategoryTheory.section_ {C : Type u₁} [] {X : C} {Y : C} (f : X Y) [hf : ] :
Y X

The chosen section of a split epimorphism. (Note that section is a reserved keyword, so we append an underscore.)

Equations
• = .some.section_
Instances For
@[simp]
theorem CategoryTheory.IsSplitEpi.id_assoc {C : Type u₁} [] {X : C} {Y : C} (f : X Y) [hf : ] {Z : C} (h : Y Z) :
@[simp]
theorem CategoryTheory.IsSplitEpi.id {C : Type u₁} [] {X : C} {Y : C} (f : X Y) [hf : ] :
def CategoryTheory.SplitEpi.splitMono {C : Type u₁} [] {X : C} {Y : C} {f : X Y} (se : ) :

The section of a split epimorphism has an obvious retraction.

Equations
• se.splitMono = { retraction := f, id := }
Instances For
instance CategoryTheory.section_isSplitMono {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

The section of a split epimorphism is itself a split monomorphism.

Equations
• =
theorem CategoryTheory.isIso_of_mono_of_isSplitEpi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

A split epi which is mono is an iso.

@[instance 100]
instance CategoryTheory.IsSplitMono.of_iso {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

Every iso is a split mono.

Equations
• =
@[instance 100]
instance CategoryTheory.IsSplitEpi.of_iso {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

Every iso is a split epi.

Equations
• =
theorem CategoryTheory.SplitMono.mono {C : Type u₁} [] {X : C} {Y : C} {f : X Y} (sm : ) :
@[instance 100]
instance CategoryTheory.IsSplitMono.mono {C : Type u₁} [] {X : C} {Y : C} (f : X Y) [hf : ] :

Every split mono is a mono.

Equations
• =
theorem CategoryTheory.SplitEpi.epi {C : Type u₁} [] {X : C} {Y : C} {f : X Y} (se : ) :
@[instance 100]
instance CategoryTheory.IsSplitEpi.epi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) [hf : ] :

Every split epi is an epi.

Equations
• =
theorem CategoryTheory.IsIso.of_mono_retraction' {C : Type u₁} [] {X : C} {Y : C} {f : X Y} (hf : ) [CategoryTheory.Mono hf.retraction] :

Every split mono whose retraction is mono is an iso.

theorem CategoryTheory.IsIso.of_mono_retraction {C : Type u₁} [] {X : C} {Y : C} (f : X Y) [hf : ] [hf' : ] :

Every split mono whose retraction is mono is an iso.

theorem CategoryTheory.IsIso.of_epi_section' {C : Type u₁} [] {X : C} {Y : C} {f : X Y} (hf : ) [CategoryTheory.Epi hf.section_] :

Every split epi whose section is epi is an iso.

theorem CategoryTheory.IsIso.of_epi_section {C : Type u₁} [] {X : C} {Y : C} (f : X Y) [hf : ] [hf' : ] :

Every split epi whose section is epi is an iso.

noncomputable def CategoryTheory.Groupoid.ofTruncSplitMono {C : Type u₁} [] (all_split_mono : ∀ {X Y : C} (f : X Y), ) :

A category where every morphism has a Trunc retraction is computably a groupoid.

Equations
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 : ],

All monos are split

Instances
theorem CategoryTheory.SplitMonoCategory.isSplitMono_of_mono {C : Type u₁} [] [self : ] {X : C} {Y : C} (f : X Y) :

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 : ],

All epis are split

Instances
theorem CategoryTheory.SplitEpiCategory.isSplitEpi_of_epi {C : Type u₁} [] [self : ] {X : C} {Y : C} (f : X Y) :

All epis are split

theorem CategoryTheory.isSplitMono_of_mono {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

In a category in which every monomorphism is split, every monomorphism splits. This is not an instance because it would create an instance loop.

theorem CategoryTheory.isSplitEpi_of_epi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

In a category in which every epimorphism is split, every epimorphism splits. This is not an instance because it would create an instance loop.

@[simp]
theorem CategoryTheory.SplitMono.map_retraction {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} (sm : ) (F : ) :
(sm.map F).retraction = F.map sm.retraction
def CategoryTheory.SplitMono.map {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} (sm : ) (F : ) :

Split monomorphisms are also absolute monomorphisms.

Equations
• sm.map F = { retraction := F.map sm.retraction, id := }
Instances For
@[simp]
theorem CategoryTheory.SplitEpi.map_section_ {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} (se : ) (F : ) :
(se.map F).section_ = F.map se.section_
def CategoryTheory.SplitEpi.map {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} (se : ) (F : ) :

Split epimorphisms are also absolute epimorphisms.

Equations
• se.map F = { section_ := F.map se.section_, id := }
Instances For
instance CategoryTheory.instIsSplitMonoMap {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} (f : X Y) [hf : ] (F : ) :
Equations
• =
instance CategoryTheory.instIsSplitEpiMap {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} (f : X Y) [hf : ] (F : ) :
Equations
• =