kernel_ι_comp — Mathlib

English

For any mono factorization F of f, the composite kernel.ι f ≫ F.e equals 0.

Русский

Для любого разложения через монофакторизацию F морфизм kernel.ι f с композицией F.e равняется 0.

LaTeX

$$$[HasKernel f] \Rightarrow [MonoFactorisation f] \Rightarrow kernel.\"ι f \\circ F.e = 0$$$

Lean4

@[simp]
theorem kernel_ι_comp [HasKernel f] (F : MonoFactorisation f) : kernel.ι f ≫ F.e = 0 := by
  rw [← cancel_mono F.m, zero_comp, Category.assoc, F.fac, kernel.condition]

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