hasCokernel_comp_iso — Mathlib

English

If f has a cokernel and g is an isomorphism, then the composite f ≫ g has a cokernel.

Русский

Если у f есть котокernel и g — изоморфизм, то композиция f ≫ g имеет котокernel.

LaTeX

$$$\forall {C} [Category C] [HasZeroMorphisms C] {X Y Z} (f : X ⟶ Y) (g : Y ⟶ Z) [HasCokernel f] [IsIso g],\; HasCokernel (f ≫ g)$$$

Lean4

instance hasCokernel_comp_iso {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasCokernel f] [IsIso g] : HasCokernel (f ≫ g) where
  exists_colimit :=
    ⟨{  cocone := CokernelCofork.ofπ (inv g ≫ cokernel.π f) (by simp)
        isColimit :=
          isColimitAux _ (fun s => cokernel.desc _ (g ≫ s.π) (by rw [← Category.assoc, CokernelCofork.condition]))
            (by simp) fun s (m : cokernel _ ⟶ _) w => by
            simp_rw [← w]
            apply coequalizer.hom_ext
            simp }⟩

Похожие утверждения