# mathlib3documentation

category_theory.epi_mono

# Facts about epimorphisms and monomorphisms. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The definitions of epi and mono are in category_theory.category, since they are used by some lemmas for iso, which is used everywhere.

@[protected, instance]
def category_theory.unop_mono_of_epi {C : Type u₁} {A B : Cᵒᵖ} (f : A B)  :
@[protected, instance]
def category_theory.unop_epi_of_mono {C : Type u₁} {A B : Cᵒᵖ} (f : A B)  :
@[protected, instance]
def category_theory.op_mono_of_epi {C : Type u₁} {A B : C} (f : A B)  :
@[protected, instance]
def category_theory.op_epi_of_mono {C : Type u₁} {A B : C} (f : A B)  :
@[nolint, ext]
structure category_theory.split_mono {C : Type u₁} {X 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 category_theory.split_mono
• category_theory.split_mono.has_sizeof_inst
theorem category_theory.split_mono.ext {C : Type u₁} {_inst_1 : category_theory.category C} {X Y : C} {f : X Y} (x y : category_theory.split_mono f) (h : x.retraction = y.retraction) :
x = y
theorem category_theory.split_mono.ext_iff {C : Type u₁} {_inst_1 : category_theory.category C} {X Y : C} {f : X Y} (x y : category_theory.split_mono f) :
x = y
@[simp]
theorem category_theory.split_mono.id {C : Type u₁} {X Y : C} {f : X Y} (self : category_theory.split_mono f) :
f self.retraction = 𝟙 X
@[simp]
theorem category_theory.split_mono.id_assoc {C : Type u₁} {X Y : C} {f : X Y} (self : category_theory.split_mono f) {X' : C} (f' : X X') :
f self.retraction f' = f'
@[class]
structure category_theory.is_split_mono {C : Type u₁} {X Y : C} (f : X Y) :
Prop
• exists_split_mono :

is_split_mono f is the assertion that f admits a retraction

Instances of this typeclass
theorem category_theory.is_split_mono.mk' {C : Type u₁} {X Y : C} {f : X Y} (sm : category_theory.split_mono f) :

A constructor for is_split_mono f taking a split_mono f as an argument

theorem category_theory.split_epi.ext_iff {C : Type u₁} {_inst_1 : category_theory.category C} {X Y : C} {f : X Y} (x y : category_theory.split_epi f) :
x = y
theorem category_theory.split_epi.ext {C : Type u₁} {_inst_1 : category_theory.category C} {X Y : C} {f : X Y} (x y : category_theory.split_epi f) (h : x.section_ = y.section_) :
x = y
@[nolint, ext]
structure category_theory.split_epi {C : Type u₁} {X 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 category_theory.split_epi
• category_theory.split_epi.has_sizeof_inst
@[simp]
theorem category_theory.split_epi.id {C : Type u₁} {X Y : C} {f : X Y} (self : category_theory.split_epi f) :
self.section_ f = 𝟙 Y
@[simp]
theorem category_theory.split_epi.id_assoc {C : Type u₁} {X Y : C} {f : X Y} (self : category_theory.split_epi f) {X' : C} (f' : Y X') :
self.section_ f f' = f'
@[class]
structure category_theory.is_split_epi {C : Type u₁} {X Y : C} (f : X Y) :
Prop
• exists_split_epi :

is_split_epi f is the assertion that f admits a section

Instances of this typeclass
theorem category_theory.is_split_epi.mk' {C : Type u₁} {X Y : C} {f : X Y} (se : category_theory.split_epi f) :

A constructor for is_split_epi f taking a split_epi f as an argument

noncomputable def category_theory.retraction {C : Type u₁} {X Y : C} (f : X Y)  :
Y X

The chosen retraction of a split monomorphism.

Equations
Instances for category_theory.retraction
@[simp]
theorem category_theory.is_split_mono.id {C : Type u₁} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.is_split_mono.id_assoc {C : Type u₁} {X Y : C} (f : X Y) {X' : C} (f' : X X') :
f = f'
def category_theory.split_mono.split_epi {C : Type u₁} {X Y : C} {f : X Y} (sm : category_theory.split_mono f) :

The retraction of a split monomorphism has an obvious section.

Equations
@[protected, instance]
def category_theory.retraction_is_split_epi {C : Type u₁} {X Y : C} (f : X Y)  :

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

theorem category_theory.is_iso_of_epi_of_is_split_mono {C : Type u₁} {X Y : C} (f : X Y)  :

A split mono which is epi is an iso.

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

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_
@[simp]
theorem category_theory.is_split_epi.id {C : Type u₁} {X Y : C} (f : X Y) [hf : category_theory.is_split_epi f] :
= 𝟙 Y
@[simp]
theorem category_theory.is_split_epi.id_assoc {C : Type u₁} {X Y : C} (f : X Y) [hf : category_theory.is_split_epi f] {X' : C} (f' : Y X') :
f f' = f'
def category_theory.split_epi.split_mono {C : Type u₁} {X Y : C} {f : X Y} (se : category_theory.split_epi f) :

The section of a split epimorphism has an obvious retraction.

Equations
@[protected, instance]
def category_theory.section_is_split_mono {C : Type u₁} {X Y : C} (f : X Y) [hf : category_theory.is_split_epi f] :

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

theorem category_theory.is_iso_of_mono_of_is_split_epi {C : Type u₁} {X Y : C} (f : X Y)  :

A split epi which is mono is an iso.

@[protected, instance]
def category_theory.is_split_mono.of_iso {C : Type u₁} {X Y : C} (f : X Y)  :

Every iso is a split mono.

@[protected, instance]
def category_theory.is_split_epi.of_iso {C : Type u₁} {X Y : C} (f : X Y)  :

Every iso is a split epi.

theorem category_theory.split_mono.mono {C : Type u₁} {X Y : C} {f : X Y} (sm : category_theory.split_mono f) :
@[protected, instance]
def category_theory.is_split_mono.mono {C : Type u₁} {X Y : C} (f : X Y)  :

Every split mono is a mono.

theorem category_theory.split_epi.epi {C : Type u₁} {X Y : C} {f : X Y} (se : category_theory.split_epi f) :
@[protected, instance]
def category_theory.is_split_epi.epi {C : Type u₁} {X Y : C} (f : X Y) [hf : category_theory.is_split_epi f] :

Every split epi is an epi.

theorem category_theory.is_iso.of_mono_retraction' {C : Type u₁} {X Y : C} {f : X Y} (hf : category_theory.split_mono f)  :

Every split mono whose retraction is mono is an iso.

theorem category_theory.is_iso.of_mono_retraction {C : Type u₁} {X Y : C} (f : X Y)  :

Every split mono whose retraction is mono is an iso.

theorem category_theory.is_iso.of_epi_section' {C : Type u₁} {X Y : C} {f : X Y} (hf : category_theory.split_epi f)  :

Every split epi whose section is epi is an iso.

theorem category_theory.is_iso.of_epi_section {C : Type u₁} {X Y : C} (f : X Y) [hf : category_theory.is_split_epi f] [hf' : category_theory.epi ] :

Every split epi whose section is epi is an iso.

noncomputable def category_theory.groupoid.of_trunc_split_mono {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
@[class]
structure category_theory.split_mono_category (C : Type u₁)  :
• is_split_mono_of_mono : {X Y : C} (f : X Y) [_inst_2 : ,

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
@[class]
structure category_theory.split_epi_category (C : Type u₁)  :
• is_split_epi_of_epi : {X Y : C} (f : X Y) [_inst_2 : ,

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
theorem category_theory.is_split_mono_of_mono {C : Type u₁} {X 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 category_theory.is_split_epi_of_epi {C : Type u₁} {X 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.

def category_theory.split_mono.map {C : Type u₁} {D : Type u₂} {X Y : C} {f : X Y} (sm : category_theory.split_mono f) (F : C D) :

Split monomorphisms are also absolute monomorphisms.

Equations
@[simp]
theorem category_theory.split_mono.map_retraction {C : Type u₁} {D : Type u₂} {X Y : C} {f : X Y} (sm : category_theory.split_mono f) (F : C D) :
@[simp]
theorem category_theory.split_epi.map_section_ {C : Type u₁} {D : Type u₂} {X Y : C} {f : X Y} (se : category_theory.split_epi f) (F : C D) :
(se.map F).section_ = F.map se.section_
def category_theory.split_epi.map {C : Type u₁} {D : Type u₂} {X Y : C} {f : X Y} (se : category_theory.split_epi f) (F : C D) :

Split epimorphisms are also absolute epimorphisms.

Equations
@[protected, instance]
def category_theory.functor.map.is_split_mono {C : Type u₁} {D : Type u₂} {X Y : C} (f : X Y) (F : C D) :
@[protected, instance]
def category_theory.functor.map.is_split_epi {C : Type u₁} {D : Type u₂} {X Y : C} (f : X Y) [hf : category_theory.is_split_epi f] (F : C D) :