preservesKernel_zero — Mathlib

English

The cokernel of a zero map is preserved by any functor that preserves zero morphisms; in other words, if f = 0, then the functor G preserves the cokernel of f.

Русский

Кокernel нулевого отображения сохраняется любым функтором, сохраняющим нулевые морфизмы; другими словами, если f = 0, то G сохраняет cokernel f.

LaTeX

$$$\text{PreservesColimit}(\text{parallelPair}(f,0))\ G$ whenever $f=0$$$

Lean4

instance preservesKernel_zero : PreservesLimit (parallelPair (0 : X ⟶ Y) 0) G where
  preserves {c}
    hc :=
    ⟨by
      have := KernelFork.IsLimit.isIso_ι c hc rfl
      refine (KernelFork.isLimitMapConeEquiv c G).symm ?_
      refine IsLimit.ofIsoLimit (KernelFork.IsLimit.ofId _ (G.map_zero _ _)) ?_
      exact (Fork.ext (G.mapIso (asIso (Fork.ι c))).symm (by simp))⟩

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