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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.NormalMonoCategory C] {X : C} {Y : C} {Z : C} (a : X ⟶ Z) (b : Y ⟶ Z) [CategoryTheory.Mono a] [CategoryTheory.Mono b] : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan a b)

The pullback of two monomorphisms exists.

Equations

• (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan a b)) = (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan a b))

@[irreducible]

def CategoryTheory.NormalMonoCategory.hasLimit_parallelPair {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.NormalMonoCategory C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g)

The equalizer of f and g exists.

Equations

• (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g)) = (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g))

instance CategoryTheory.NormalMonoCategory.hasEqualizers {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.NormalMonoCategory C] : CategoryTheory.Limits.HasEqualizers C

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

Equations

• (_ : CategoryTheory.Limits.HasEqualizers C) = (_ : CategoryTheory.Limits.HasEqualizers C)

theorem CategoryTheory.NormalMonoCategory.epi_of_zero_cokernel {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.NormalMonoCategory C] {X : C} {Y : C} (f : X ⟶ Y) (Z : C) (l : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ 0 (_ : CategoryTheory.CategoryStruct.comp f 0 = 0))) : CategoryTheory.Epi f

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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.NormalMonoCategory C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {Y : C} (f : X ⟶ Y) (hf : ∀ (Z : C) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = 0 → g = 0) : CategoryTheory.Epi f

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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.NormalEpiCategory C] {X : C} {Y : C} {Z : C} (a : X ⟶ Y) (b : X ⟶ Z) [CategoryTheory.Epi a] [CategoryTheory.Epi b] : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span a b)

The pushout of two epimorphisms exists.

Equations

• (_ : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span a b)) = (_ : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span a b))

@[irreducible]

def CategoryTheory.NormalEpiCategory.hasColimit_parallelPair {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.NormalEpiCategory C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f g)

The coequalizer of f and g exists.

Equations

• (_ : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f g)) = (_ : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f g))

instance CategoryTheory.NormalEpiCategory.hasCoequalizers {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.NormalEpiCategory C] : CategoryTheory.Limits.HasCoequalizers C

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

Equations

• (_ : CategoryTheory.Limits.HasCoequalizers C) = (_ : CategoryTheory.Limits.HasCoequalizers C)

theorem CategoryTheory.NormalEpiCategory.mono_of_zero_kernel {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.NormalEpiCategory C] {X : C} {Y : C} (f : X ⟶ Y) (Z : C) (l : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι 0 (_ : CategoryTheory.CategoryStruct.comp 0 f = 0))) : CategoryTheory.Mono f

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} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.NormalEpiCategory C] [CategoryTheory.Limits.HasZeroObject C] {X : C} {Y : C} (f : X ⟶ Y) (hf : ∀ (Z : C) (g : Z ⟶ X), CategoryTheory.CategoryStruct.comp g f = 0 → g = 0) : CategoryTheory.Mono f

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