kernelSubobject_arrow — Mathlib

English

There is a canonical relationship between the isomorphism kernelSubobject f and kernel f, given by equality: (kernelSubobjectIso f).hom ≫ kernel.ι f = kernelSubobject f .arrow.

Русский

Существует каноническое отношение между изоморфизмом kernelSubobject f и kernel f, задающееся равенством: (kernelSubobjectIso f).hom ≫ kernel.ι f = kernelSubobject f .arrow.

LaTeX

$$$$(kernelSubobjectIso f).hom \\circ kernel.ι f = (kernelSubobject f).arrow$$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem kernelSubobject_arrow : (kernelSubobjectIso f).hom ≫ kernel.ι f = (kernelSubobject f).arrow := by
  simp [kernelSubobjectIso]

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