Documentation

Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

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

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

source
theorem CategoryTheory.NormalMonoCategory.pullback_of_mono {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteProducts C] [Limits.HasKernels C] [IsNormalMonoCategory C] {X Y Z : C} (a : X ⟶ Z) (b : Y ⟶ Z) [Mono a] [Mono b] :
Limits.HasLimit (Limits.cospan a b)

The pullback of two monomorphisms exists.

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

The equalizer of f and g exists.

source
@[instance 100]
instance CategoryTheory.NormalMonoCategory.hasEqualizers {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteProducts C] [Limits.HasKernels C] [IsNormalMonoCategory C] :
Limits.HasEqualizers C

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

source
theorem CategoryTheory.NormalMonoCategory.epi_of_zero_cokernel {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteProducts C] [Limits.HasKernels C] [IsNormalMonoCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) (l : Limits.IsColimit (Limits.CokernelCofork.ofπ 0 ⋯)) :
Epi f

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

source
theorem CategoryTheory.NormalMonoCategory.epi_of_zero_cancel {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteProducts C] [Limits.HasKernels C] [IsNormalMonoCategory C] [Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) (hf : ∀ (Z : C) (g : Y ⟶ Z), CategoryStruct.comp f g = 0 → g = 0) :
Epi f

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

source
theorem CategoryTheory.NormalMonoCategory.preservesEpimorphisms_of_preservesCokernels {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteProducts C] [Limits.HasKernels C] [IsNormalMonoCategory C] [Limits.HasZeroObject C] {D : Type u_2} [Category.{v_2, u_2} D] [Limits.HasZeroMorphisms D] [Limits.HasZeroObject D] (F : Functor D C) [F.PreservesZeroMorphisms] [∀ {X Y : D} (f : X ⟶ Y), Limits.PreservesColimit (Limits.parallelPair f 0) F] :
F.PreservesEpimorphisms
source
theorem CategoryTheory.NormalEpiCategory.pushout_of_epi {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteCoproducts C] [Limits.HasCokernels C] [IsNormalEpiCategory C] {X Y Z : C} (a : X ⟶ Y) (b : X ⟶ Z) [Epi a] [Epi b] :
Limits.HasColimit (Limits.span a b)

The pushout of two epimorphisms exists.

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

The coequalizer of f and g exists.

source
@[instance 100]
instance CategoryTheory.NormalEpiCategory.hasCoequalizers {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteCoproducts C] [Limits.HasCokernels C] [IsNormalEpiCategory C] :
Limits.HasCoequalizers C

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

source
theorem CategoryTheory.NormalEpiCategory.mono_of_zero_kernel {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteCoproducts C] [Limits.HasCokernels C] [IsNormalEpiCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) (l : Limits.IsLimit (Limits.KernelFork.ofι 0 ⋯)) :
Mono f

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

source
theorem CategoryTheory.NormalEpiCategory.mono_of_cancel_zero {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteCoproducts C] [Limits.HasCokernels C] [IsNormalEpiCategory C] [Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) (hf : ∀ (Z : C) (g : Z ⟶ X), CategoryStruct.comp g f = 0 → g = 0) :
Mono f

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

source
theorem CategoryTheory.NormalEpiCategory.preservesMonomorphisms_of_preservesKernels {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] [Limits.HasFiniteCoproducts C] [Limits.HasCokernels C] [IsNormalEpiCategory C] [Limits.HasZeroObject C] {D : Type u_2} [Category.{v_2, u_2} D] [Limits.HasZeroMorphisms D] [Limits.HasZeroObject D] (F : Functor D C) [F.PreservesZeroMorphisms] [∀ {X Y : D} (f : X ⟶ Y), Limits.PreservesLimit (Limits.parallelPair f 0) F] :
F.PreservesMonomorphisms