# mathlib3documentation

category_theory.limits.shapes.normal_mono.equalizers

# Normal mono categories with finite products and kernels have all equalizers. #

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

This, and the dual result, are used in the development of abelian categories.

@[irreducible]

The pullback of two monomorphisms exists.

@[irreducible]

The equalizer of f and g exists.

@[protected, instance]

A normal_mono_category category with finite products and kernels has all equalizers.

If a zero morphism is a cokernel of f, then f is an epimorphism.

theorem category_theory.normal_mono_category.epi_of_zero_cancel {C : Type u_1} {X Y : C} (f : X Y) (hf : (Z : C) (g : Y Z), f g = 0 g = 0) :

If f ≫ g = 0 implies g = 0 for all g, then g is a monomorphism.

@[irreducible]
theorem category_theory.normal_epi_category.pushout_of_epi {C : Type u_1} {X Y Z : C} (a : X Y) (b : X Z)  :

The pushout of two epimorphisms exists.

@[irreducible]

The coequalizer of f and g exists.

@[protected, instance]

A normal_epi_category category with finite coproducts and cokernels has all coequalizers.

If a zero morphism is a kernel of f, then f is a monomorphism.

theorem category_theory.normal_epi_category.mono_of_cancel_zero {C : Type u_1} {X Y : C} (f : X Y) (hf : (Z : C) (g : Z X), g f = 0 g = 0) :

If g ≫ f = 0 implies g = 0 for all g, then f is a monomorphism.