kernelIsoKer_inv_kernel_ι — Mathlib

English

The inverse of the kernel-isomorphism composed with the kernel inclusion yields the canonical kernel inclusion.

Русский

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

LaTeX

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

Lean4

@[simp, elementwise]
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation

theorem kernelIsoKer_inv_kernel_ι : (kernelIsoKer f).inv ≫ kernel.ι f = ofHom (LinearMap.ker f.hom).subtype :=
  limit.isoLimitCone_inv_π _ _

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