imageToKernel — Mathlib

English

The canonical morphism from the image of f to the kernel of g exists whenever f ∘ g = 0; it is defined by factoring through the image of f and the kernel of g.

Русский

Существование канонического морфизма из образа f в ядро g при условии f ∘ g = 0; он задаётся через факторизацию через образ и ядро.

LaTeX

$$$\text{imageToKernel}(f,g,w): \mathrm{Im}(f) \to \mathrm{Ker}(g)$ where $w: f g = 0$$$

Lean4

/-- The canonical morphism `imageSubobject f ⟶ kernelSubobject g` when `f ≫ g = 0`.
-/
def imageToKernel (w : f ≫ g = 0) : (imageSubobject f : V) ⟶ (kernelSubobject g : V) :=
  Subobject.ofLE _ _ (image_le_kernel _ _ w)

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