# Documentation

Mathlib.CategoryTheory.EpiMono

# 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) :
instance CategoryTheory.unop_epi_of_mono {C : Type u₁} [] {A : Cᵒᵖ} {B : Cᵒᵖ} (f : A B) :
instance CategoryTheory.op_mono_of_epi {C : Type u₁} [] {A : C} {B : C} (f : A B) :
instance CategoryTheory.op_epi_of_mono {C : Type u₁} [] {A : C} {B : C} (f : A B) :
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_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) :
• exists_splitMono :

There is a splitting

IsSplitMono f is the assertion that f admits a retraction

Instances
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

structure CategoryTheory.SplitEpi {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :
Type v₁
• section_ : Y X

The map splitting f

• id :

section_ composed with f is the identity

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_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) :
• exists_splitEpi :

There is a splitting

IsSplitEpi f is the assertion that f admits a section

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

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.

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.

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

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.

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.

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 CategoryTheory.IsSplitMono.of_iso {C : Type u₁} [] {X : C} {Y : C} (f : X Y) :

Every iso is a split mono.

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

Every iso is a split epi.

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

Every split mono is a mono.

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

Every split epi is an epi.

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.

Instances For
• isSplitMono_of_mono : ∀ {X Y : C} (f : X Y) [inst : ],

All monos are split

A split mono category is a category in which every monomorphism is split.

Instances
• isSplitEpi_of_epi : ∀ {X Y : C} (f : X Y) [inst : ],

All epis are split

A split epi category is a category in which every epimorphism is split.

Instances
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 : ) :
().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.

Instances For
@[simp]
theorem CategoryTheory.SplitEpi.map_section_ {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} (se : ) (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.

Instances For
instance CategoryTheory.instIsSplitMonoObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorMap {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} (f : X Y) [hf : ] (F : ) :
instance CategoryTheory.instIsSplitEpiObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorMap {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} (f : X Y) [hf : ] (F : ) :