imageToKernel_comp_right — Mathlib

English

Composing with h on the right yields a relation between imageToKernel f (g ≫ h) and imageToKernel f g: imageToKernel f (g ≫ h) w = imageToKernel f g w ≫ Subobject.ofLE _ _ (kernelSubobject_comp_le g h).inv.

Русский

Правый композиционный переход: imageToKernel f (g ≫ h) = imageToKernel f g ⋯

LaTeX

$$$imageToKernel f (g \gg h) w = imageToKernel f g w \;\circ\; (\mathrm{kernelSubobject}(g) \;\text{desc} \; (\mathrm{kernelSubobject}(g \gg h)))^{-1}$$$

Lean4

theorem imageToKernel_comp_right {D : V} (h : C ⟶ D) (w : f ≫ g = 0) :
    imageToKernel f (g ≫ h) (by simp [reassoc_of% w]) =
      imageToKernel f g w ≫ Subobject.ofLE _ _ (kernelSubobject_comp_le g h) :=
  by
  ext
  simp

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