kernelIsoKer_inv_comp_ι — Mathlib

English

The canonical composite of kernelIsomorphism and kernel injection equals the standard kernel inclusion.

Русский

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

LaTeX

$$$(\\text{kernelIsoKer } f)^{-1} \\circ \\kernel.ι f = \\mathrm{ofHom}(\\mathrm{AddSubgroup.subtype}(\\ker f))$$$

Lean4

@[simp]
theorem kernelIsoKer_inv_comp_ι {G H : AddCommGrpCat.{u}} (f : G ⟶ H) :
    (kernelIsoKer f).inv ≫ kernel.ι f = ofHom (AddSubgroup.subtype f.hom.ker) := by simp [kernelIsoKer]

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