Short exact kernel and cokernel sequences

This file records that the canonical kernel sequence of an epimorphism and the canonical cokernel sequence of a monomorphism are short exact.

Main statements

• TauCeti.kernelSequence_shortExact: the kernel sequence of an epimorphism is short exact.
• TauCeti.cokernelSequence_shortExact: the cokernel sequence of a monomorphism is short exact.

instance TauCeti.epi_kernelSequence_g {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.Epi (CategoryTheory.ShortComplex.kernelSequence f).g

The second map in the kernel sequence of an epimorphism is an epimorphism.

theorem TauCeti.kernelSequence_shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] : (CategoryTheory.ShortComplex.kernelSequence f).ShortExact

The kernel sequence of an epimorphism is short exact.

instance TauCeti.mono_cokernelSequence_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Mono (CategoryTheory.ShortComplex.cokernelSequence f).f

The first map in the cokernel sequence of a monomorphism is a monomorphism.

theorem TauCeti.cokernelSequence_shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : (CategoryTheory.ShortComplex.cokernelSequence f).ShortExact

The cokernel sequence of a monomorphism is short exact.