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

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

@[irreducible]
def CategoryTheory.NormalMonoCategory.pullback_of_mono {C : Type u_1} [] {X : C} {Y : C} {Z : C} (a : X Z) (b : Y Z) :

The pullback of two monomorphisms exists.

Equations
• =
Instances For
@[irreducible]
def CategoryTheory.NormalMonoCategory.hasLimit_parallelPair {C : Type u_1} [] {X : C} {Y : C} (f : X Y) (g : X Y) :

The equalizer of f and g exists.

Equations
• =
Instances For
@[instance 100]

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

Equations
• =
theorem CategoryTheory.NormalMonoCategory.epi_of_zero_cokernel {C : Type u_1} [] {X : C} {Y : C} (f : X Y) (Z : C) :

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

theorem CategoryTheory.NormalMonoCategory.epi_of_zero_cancel {C : Type u_1} [] {X : C} {Y : C} (f : X Y) (hf : ∀ (Z : C) (g : Y Z), g = 0) :

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

@[irreducible]
def CategoryTheory.NormalEpiCategory.pushout_of_epi {C : Type u_1} [] {X : C} {Y : C} {Z : C} (a : X Y) (b : X Z) :

The pushout of two epimorphisms exists.

Equations
• =
Instances For
@[irreducible]
def CategoryTheory.NormalEpiCategory.hasColimit_parallelPair {C : Type u_1} [] {X : C} {Y : C} (f : X Y) (g : X Y) :

The coequalizer of f and g exists.

Equations
• =
Instances For
@[instance 100]

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

Equations
• =
theorem CategoryTheory.NormalEpiCategory.mono_of_zero_kernel {C : Type u_1} [] {X : C} {Y : C} (f : X Y) (Z : C) :

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

theorem CategoryTheory.NormalEpiCategory.mono_of_cancel_zero {C : Type u_1} [] {X : C} {Y : C} (f : X Y) (hf : ∀ (Z : C) (g : Z X), g = 0) :

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