Kernels of projections onto abelian images

The projection of a morphism onto its abelian image has the same kernel as the morphism. This identifies the first term of the kernel-image sequence without requiring the category to be abelian. The construction complements CategoryTheory.Limits.kernelFactorThruImage, which uses the categorical image rather than the kernel of the cokernel.

noncomputable def TauCeti.Abelian.kernelFactorThruImageIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Abelian.factorThruImage f)] : CategoryTheory.Limits.kernel f ≅ CategoryTheory.Limits.kernel (CategoryTheory.Abelian.factorThruImage f)

The kernel of a morphism is isomorphic to the kernel of its projection onto the abelian image, whenever the required kernels and cokernel exist.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Abelian.kernelFactorThruImageIso_hom_comp_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Abelian.factorThruImage f)] : CategoryTheory.CategoryStruct.comp (kernelFactorThruImageIso f).hom (CategoryTheory.Limits.kernel.ι (CategoryTheory.Abelian.factorThruImage f)) = CategoryTheory.Limits.kernel.ι f

The isomorphism with the kernel of the image projection preserves the kernel inclusion.

@[simp]

theorem TauCeti.Abelian.kernelFactorThruImageIso_hom_comp_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Abelian.factorThruImage f)] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (kernelFactorThruImageIso f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.Abelian.factorThruImage f)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) h

The isomorphism with the kernel of the image projection preserves the kernel inclusion.

@[simp]

theorem TauCeti.Abelian.kernelFactorThruImageIso_inv_comp_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Abelian.factorThruImage f)] : CategoryTheory.CategoryStruct.comp (kernelFactorThruImageIso f).inv (CategoryTheory.Limits.kernel.ι f) = CategoryTheory.Limits.kernel.ι (CategoryTheory.Abelian.factorThruImage f)

The inverse isomorphism with the kernel of the image projection preserves the inclusion.

@[simp]

theorem TauCeti.Abelian.kernelFactorThruImageIso_inv_comp_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] [CategoryTheory.Limits.HasKernel f] [CategoryTheory.Limits.HasKernel (CategoryTheory.Abelian.factorThruImage f)] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (kernelFactorThruImageIso f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.Abelian.factorThruImage f)) h

The inverse isomorphism with the kernel of the image projection preserves the inclusion.