mathlib documentation

category_theory.epi_mono

Facts about epimorphisms and monomorphisms. #

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]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem category_theory.left_adjoint_preserves_epi {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {X Y : C} {f : X Y} (hf : category_theory.epi f) :
theorem category_theory.right_adjoint_preserves_mono {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} {G : D C} (adj : F G) {X Y : D} {f : X Y} (hf : category_theory.mono f) :
@[protected, instance]
@[protected, instance]
theorem category_theory.faithful_reflects_epi {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) [category_theory.faithful F] {X Y : C} {f : X Y} (hf : category_theory.epi (F.map f)) :
theorem category_theory.faithful_reflects_mono {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) [category_theory.faithful F] {X Y : C} {f : X Y} (hf : category_theory.mono (F.map f)) :
@[class]
structure category_theory.split_mono {C : Type u₁} [category_theory.category C] {X Y : C} (f : X Y) :
Type v₁

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 of this typeclass
Instances of other typeclasses for category_theory.split_mono
  • category_theory.split_mono.has_sizeof_inst
@[class]
structure category_theory.split_epi {C : Type u₁} [category_theory.category C] {X Y : C} (f : X Y) :
Type v₁

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 of this typeclass
Instances of other typeclasses for category_theory.split_epi
  • category_theory.split_epi.has_sizeof_inst
def category_theory.retraction {C : Type u₁} [category_theory.category C] {X Y : C} (f : X Y) [category_theory.split_mono f] :
Y X

The chosen retraction of a split monomorphism.

Equations
Instances for category_theory.retraction
@[simp]
theorem category_theory.split_mono.id_assoc {C : Type u₁} [category_theory.category C] {X Y : C} (f : X Y) [category_theory.split_mono f] {X' : C} (f' : X X') :
@[protected, instance]

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

Equations

A split mono which is epi is an iso.

def category_theory.section_ {C : Type u₁} [category_theory.category C] {X Y : C} (f : X Y) [category_theory.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]
@[simp]
theorem category_theory.split_epi.id_assoc {C : Type u₁} [category_theory.category C] {X Y : C} (f : X Y) [category_theory.split_epi f] {X' : C} (f' : Y X') :
@[protected, instance]

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

Equations

A split epi which is mono is an iso.

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

Every iso is a split mono.

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

Every iso is a split epi.

Equations
@[protected, instance]

Every split mono is a mono.

@[protected, instance]

Every split epi is an epi.

Every split mono whose retraction is mono is an iso.

Every split epi whose section is epi is an iso.

noncomputable def category_theory.groupoid.of_trunc_split_mono {C : Type u₁} [category_theory.category C] (all_split_mono : Π {X Y : C} (f : X Y), trunc (category_theory.split_mono f)) :

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

Equations
@[class]
structure category_theory.split_mono_category (C : Type u₁) [category_theory.category C] :
Type (max u₁ v₁)

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₁) [category_theory.category C] :
Type (max u₁ v₁)

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

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

Equations

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

Equations
@[protected, instance]

Split monomorphisms are also absolute monomorphisms.

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

Split epimorphisms are also absolute epimorphisms.

Equations