kernelIsoKer_hom_ker_subtype — Mathlib

English

The forward map of the kernel-iso composed with the inclusion of the kernel-subtype equals the kernel inclusion.

Русский

Впереди отображение ядра-изоморфизма, композиция с включением подмодуля ядра равна включению ядра.

LaTeX

$$$$(kernelIsoKer f).hom \\circ ofHom(ker f.hom).subtype = kernel.ι f $$$$

Lean4

@[simp, elementwise]
theorem kernelIsoKer_hom_ker_subtype :
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation
    (kernelIsoKer f).hom ≫ ofHom (LinearMap.ker f.hom).subtype = kernel.ι f :=
  IsLimit.conePointUniqueUpToIso_inv_comp _ (limit.isLimit _) WalkingParallelPair.zero

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