# mathlibdocumentation

category_theory.epi_mono

theorem category_theory.left_adjoint_preserves_epi {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {X Y : C} {f : X Y} :

theorem category_theory.right_adjoint_preserves_mono {C : Type u₁} {D : Type u₂} {F : C D} {G : D C} (adj : F G) {X Y : D} {f : X Y} :

theorem category_theory.faithful_reflects_epi {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} {f : X Y} :

theorem category_theory.faithful_reflects_mono {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} {f : X Y} :

@[class]
structure category_theory.split_mono {C : Type u₁} {X Y : C} :
(X Y)Type v₁
• retraction : Y X
• id' : . "obviously"

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
@[class]
structure category_theory.split_epi {C : Type u₁} {X Y : C} :
(X Y)Type v₁
• section_ : Y X
• id' : . "obviously"

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
def category_theory.retraction {C : Type u₁} {X Y : C} (f : X Y)  :
Y X

The chosen retraction of a split monomorphism.

Equations
@[simp]
theorem category_theory.split_mono.id {C : Type u₁} {X Y : C} (f : X Y)  :

@[simp]
theorem category_theory.split_mono.id_assoc {C : Type u₁} {X Y : C} (f : X Y) {X' : C} (f' : X X') :
f = f'

@[instance]
def category_theory.retraction_split_epi {C : Type u₁} {X Y : C} (f : X Y)  :

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

Equations
def category_theory.is_iso_of_epi_of_split_mono {C : Type u₁} {X Y : C} (f : X Y)  :

A split mono which is epi is an iso.

Equations
def category_theory.section_ {C : Type u₁} {X Y : C} (f : X Y)  :
Y X

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

Equations
@[simp]
theorem category_theory.split_epi.id {C : Type u₁} {X Y : C} (f : X Y)  :
= 𝟙 Y

@[simp]
theorem category_theory.split_epi.id_assoc {C : Type u₁} {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
f f' = f'

@[instance]
def category_theory.section_split_mono {C : Type u₁} {X Y : C} (f : X Y)  :

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

Equations
def category_theory.is_iso_of_mono_of_split_epi {C : Type u₁} {X Y : C} (f : X Y)  :

A split epi which is mono is an iso.

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

Every iso is a split mono.

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

Every iso is a split epi.

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

Every split mono is a mono.

@[instance]
def category_theory.split_epi.epi {C : Type u₁} {X Y : C} (f : X Y)  :

Every split epi is an epi.

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

Equations
def category_theory.is_iso.of_epi_section {C : Type u₁} {X Y : C} {f : X Y}  :

Every split epi whose section is epi is an iso.

Equations
@[instance]
def category_theory.unop_mono_of_epi {C : Type u₁} {A B : Cᵒᵖ} (f : A B)  :

@[instance]
def category_theory.unop_epi_of_mono {C : Type u₁} {A B : Cᵒᵖ} (f : A B)  :

@[instance]
def category_theory.op_mono_of_epi {C : Type u₁} {A B : C} (f : A B)  :

@[instance]
def category_theory.op_epi_of_mono {C : Type u₁} {A B : C} (f : A B)  :

@[instance]
def category_theory.category_theory.split_mono {C : Type u₁} {D : Type u₂} {X Y : C} (f : X Y) (F : C D) :

Split monomorphisms are also absolute monomorphisms.

Equations
@[instance]
def category_theory.category_theory.split_epi {C : Type u₁} {D : Type u₂} {X Y : C} (f : X Y) (F : C D) :

Split epimorphisms are also absolute epimorphisms.

Equations