kernelSubobject_arrow' — Mathlib

English

With HasKernel f, kernelSubobjectIso f has inverse, and its inverse composed with the subobject arrow yields kernel.ι f.

Русский

При наличии HasKernel f обратная стрелка из kernelSubobject f через изоморфизм kernelSubobjectIso f даёт ядро kernel.ι f.

LaTeX

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

Lean4

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

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