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]
theorem
category_theory.normal_mono_category.pullback_of_mono
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_products C]
[category_theory.limits.has_kernels C]
[category_theory.normal_mono_category C]
{X Y Z : C}
(a : X ⟶ Z)
(b : Y ⟶ Z)
[category_theory.mono a]
[category_theory.mono b] :
The pullback of two monomorphisms exists.
@[irreducible]
theorem
category_theory.normal_mono_category.has_limit_parallel_pair
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_products C]
[category_theory.limits.has_kernels C]
[category_theory.normal_mono_category C]
{X Y : C}
(f g : X ⟶ Y) :
The equalizer of f and g exists.
@[protected, instance]
def
category_theory.normal_mono_category.has_equalizers
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_products C]
[category_theory.limits.has_kernels C]
[category_theory.normal_mono_category C] :
A normal_mono_category category with finite products and kernels has all equalizers.
theorem
category_theory.normal_mono_category.epi_of_zero_cokernel
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_products C]
[category_theory.limits.has_kernels C]
[category_theory.normal_mono_category C]
{X Y : C}
(f : X ⟶ Y)
(Z : C)
(l : category_theory.limits.is_colimit (category_theory.limits.cokernel_cofork.of_π 0 _)) :
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}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_products C]
[category_theory.limits.has_kernels C]
[category_theory.normal_mono_category C]
[category_theory.limits.has_zero_object C]
{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}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_coproducts C]
[category_theory.limits.has_cokernels C]
[category_theory.normal_epi_category C]
{X Y Z : C}
(a : X ⟶ Y)
(b : X ⟶ Z)
[category_theory.epi a]
[category_theory.epi b] :
The pushout of two epimorphisms exists.
@[irreducible]
theorem
category_theory.normal_epi_category.has_colimit_parallel_pair
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_coproducts C]
[category_theory.limits.has_cokernels C]
[category_theory.normal_epi_category C]
{X Y : C}
(f g : X ⟶ Y) :
The coequalizer of f and g exists.
@[protected, instance]
def
category_theory.normal_epi_category.has_coequalizers
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_coproducts C]
[category_theory.limits.has_cokernels C]
[category_theory.normal_epi_category C] :
A normal_epi_category category with finite coproducts and cokernels has all coequalizers.
theorem
category_theory.normal_epi_category.mono_of_zero_kernel
{C : Type u_1}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_coproducts C]
[category_theory.limits.has_cokernels C]
[category_theory.normal_epi_category C]
{X Y : C}
(f : X ⟶ Y)
(Z : C)
(l : category_theory.limits.is_limit (category_theory.limits.kernel_fork.of_ι 0 _)) :
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}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_coproducts C]
[category_theory.limits.has_cokernels C]
[category_theory.normal_epi_category C]
[category_theory.limits.has_zero_object C]
{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.