Quotients by a composite of monomorphisms

For composable morphisms f : X ⟶ Y and g : Y ⟶ Z in an abelian category with g a monomorphism, the sequence of cokernels

0 ⟶ coker f ⟶ coker (f ≫ g) ⟶ coker g ⟶ 0

is short exact. For submodules X ⊆ Y ⊆ Z this is the third isomorphism theorem, and for singular chain complexes it is what produces the long exact homology sequence of a triple of topological spaces.

The two short exactness statements below differ only in how the three cokernels are presented: TauCeti.shortExact_cokernel_comp uses the chosen cokernels, while TauCeti.shortExact_of_isColimit_cokernelCofork takes arbitrary colimit cokernel coforks, which is what a consumer whose quotients are produced by some other colimit construction needs.

theorem TauCeti.shortExact_cokernel_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Mono g] : { X₁ := CategoryTheory.Limits.cokernel f, X₂ := CategoryTheory.Limits.cokernel (CategoryTheory.CategoryStruct.comp f g), X₃ := CategoryTheory.Limits.cokernel g, f := CategoryTheory.Limits.cokernel.map f (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X) g ⋯, g := CategoryTheory.Limits.cokernel.map (CategoryTheory.CategoryStruct.comp f g) g f (CategoryTheory.CategoryStruct.id Z) ⋯, zero := ⋯ }.ShortExact

For composable morphisms f and g in an abelian category with g a monomorphism, the sequence coker f ⟶ coker (f ≫ g) ⟶ coker g is short exact.

theorem TauCeti.shortExact_of_isColimit_cokernelCofork {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {k : X ⟶ Z} {c₁ : CategoryTheory.Limits.CokernelCofork f} {c₂ : CategoryTheory.Limits.CokernelCofork k} {c₃ : CategoryTheory.Limits.CokernelCofork g} {u : c₁.pt ⟶ c₂.pt} {v : c₂.pt ⟶ c₃.pt} (hk : CategoryTheory.CategoryStruct.comp f g = k) (hg : CategoryTheory.Mono g) (h₁ : CategoryTheory.Limits.IsColimit c₁) (h₂ : CategoryTheory.Limits.IsColimit c₂) (h₃ : CategoryTheory.Limits.IsColimit c₃) (hu : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) u = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.Cofork.π c₂)) (hv : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₂) v = CategoryTheory.Limits.Cofork.π c₃) : { X₁ := c₁.pt, X₂ := c₂.pt, X₃ := c₃.pt, f := u, g := v, zero := ⋯ }.ShortExact

The version of TauCeti.shortExact_cokernel_comp for arbitrary colimit cokernel coforks: if c₁, c₂ and c₃ exhibit cokernels of f, of f ≫ g and of g, and u and v are the maps induced between their points, then c₁.pt ⟶ c₂.pt ⟶ c₃.pt is short exact. The monomorphism hypothesis on g is explicit because the three cokernels typically present g in forms that agree only up to unfolding.