preservesCokernel_zero — Mathlib

English

The kernel of the zero morphism is preserved by any functor that preserves zero morphisms; equivalently, G preserves the limit of the parallel pair 0 ⇒ 0.

Русский

Ядро нулевого отображения сохраняется любым функтором, сохраняющим нулевые морфизмы; эквивалентно, G сохраняет предел пары параллельных стрел 0 ⇒ 0.

LaTeX

$$$\text{PreservesLimit}(\text{parallelPair}(0:X\to Y,0))\ G$$$

Lean4

noncomputable instance preservesCokernel_zero : PreservesColimit (parallelPair (0 : X ⟶ Y) 0) G where
  preserves {c}
    hc :=
    ⟨by
      have := CokernelCofork.IsColimit.isIso_π c hc rfl
      refine (CokernelCofork.isColimitMapCoconeEquiv c G).symm ?_
      refine IsColimit.ofIsoColimit (CokernelCofork.IsColimit.ofId _ (G.map_zero _ _)) ?_
      exact (Cofork.ext (G.mapIso (asIso (Cofork.π c))) (by simp))⟩

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