Vanishing of maps induced on quotients #
In a category with zero morphisms, a composite of two maps induced on quotients vanishes as soon as
the final quotient map kills the morphism inducing the first one. This is the complex condition
for sequences of quotients such as coker f ⟶ coker (f ≫ g) ⟶ coker g.
theorem
TauCeti.comp_eq_zero_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{Y Z Q₁ Q₂ Q₃ : C}
{g : Y ⟶ Z}
{π₁ : Y ⟶ Q₁}
{π₂ : Z ⟶ Q₂}
{π₃ : Z ⟶ Q₃}
{u : Q₁ ⟶ Q₂}
{v : Q₂ ⟶ Q₃}
(hπ₁ : CategoryTheory.Epi π₁)
(w₃ : CategoryTheory.CategoryStruct.comp g π₃ = 0)
(hu : CategoryTheory.CategoryStruct.comp π₁ u = CategoryTheory.CategoryStruct.comp g π₂)
(hv : CategoryTheory.CategoryStruct.comp π₂ v = π₃)
:
If π₁, π₂ and π₃ are quotient maps making u and v the maps induced on quotients by
g and by the identity, and π₃ kills the image of g, then u ≫ v = 0.