imageToKernel_comp_mono — Mathlib

English

If h is mono, there is a simplified equality for imageToKernel f (g ≫ h) w in terms of the mono-cancellation and a natural isomorphism between kernels.

Русский

Если h моно, образуется упрощённое равенство через каноническое изоморфизм ядра и связывающие отображения.

LaTeX

$$imageToKernel f (g ≫ h) w = imageToKernel f g w ≫ (Subobject.isoOfEq _ _ (kernelSubobject_comp_mono g h)).inv$$

Lean4

@[simp]
theorem imageToKernel_comp_mono {D : V} (h : C ⟶ D) [Mono h] (w) :
    imageToKernel f (g ≫ h) w =
      imageToKernel f g ((cancel_mono h).mp (by simpa using w : (f ≫ g) ≫ h = 0 ≫ h)) ≫
        (Subobject.isoOfEq _ _ (kernelSubobject_comp_mono g h)).inv :=
  by
  ext
  simp

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