mathlib documentation

category_theory.functor.epi_mono

Preservation and reflection of monomorphisms and epimorphisms #

We provide typeclasses that state that a functor preserves or reflects monomorphisms or epimorphisms.

@[protected, instance]
@[protected, instance]
def category_theory.functor.map_epi {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) [F.preserves_epimorphisms] {X Y : C} (f : X Y) [category_theory.epi f] :
@[class]
structure category_theory.functor.reflects_monomorphisms {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) :
Prop

A functor reflects monomorphisms if morphisms that are mapped to monomorphisms are themselves monomorphisms.

Instances of this typeclass
theorem category_theory.functor.mono_of_mono_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) [F.reflects_monomorphisms] {X Y : C} {f : X Y} (h : category_theory.mono (F.map f)) :
@[class]
structure category_theory.functor.reflects_epimorphisms {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) :
Prop

A functor reflects epimorphisms if morphisms that are mapped to epimorphisms are themselves epimorphisms.

Instances of this typeclass
theorem category_theory.functor.epi_of_epi_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) [F.reflects_epimorphisms] {X Y : C} {f : X Y} (h : category_theory.epi (F.map f)) :
@[protected, instance]
@[protected, instance]
@[protected, instance]

If F is a fully faithful functor, split epimorphisms are preserved and reflected by F.

Equations

If F is a fully faithful functor, split monomorphisms are preserved and reflected by F.

Equations
@[simp]
theorem category_theory.functor.epi_map_iff_epi {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) {X Y : C} (f : X Y) [hF₁ : F.preserves_epimorphisms] [hF₂ : F.reflects_epimorphisms] :
@[simp]
theorem category_theory.functor.mono_map_iff_mono {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) {X Y : C} (f : X Y) [hF₁ : F.preserves_monomorphisms] [hF₂ : F.reflects_monomorphisms] :
theorem category_theory.adjunction.strong_epi_map_of_strong_epi {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] {F : C D} {F' : D C} {A B : C} (adj : F F') (f : A B) [h₁ : F'.preserves_monomorphisms] [h₂ : F.preserves_epimorphisms] [category_theory.strong_epi f] :