kernelIsoKerOver — Mathlib

English

The kernel inclusion for f as an object over G matches the subtype inclusion of ker f into G.

Русский

Включение ядра как объект над G совпадает с включением ядра в G через подмножество.

LaTeX

$$$\\text{kernelIsoKerOver}(f) :\\ Over.mk(\\kernel.ι f) \\cong \\ Over.mk(\\mathrm{ofHom}(\\mathrm{AddSubgroup.subtype}(\\ker f. hom)))$$$

Lean4

/-- The categorical kernel inclusion for `f : G ⟶ H`, as an object over `G`,
agrees with the `AddSubgroup.subtype` map.
-/
def kernelIsoKerOver {G H : AddCommGrpCat.{u}} (f : G ⟶ H) :
    Over.mk (kernel.ι f) ≅ @Over.mk _ _ G (AddCommGrpCat.of f.hom.ker) (ofHom (AddSubgroup.subtype f.hom.ker)) :=
  Over.isoMk (kernelIsoKer f)

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