toKernelSubobject_arrow — Mathlib

English

The arrow of kernelSubobject applied to toKernelSubobject x is x.1.

Русский

Стрелка kernelSubobject, применённая к toKernelSubobject x, даёт x.1.

LaTeX

$$$(kernelSubobject f).arrow (toKernelSubobject x) = x.1$$$

Lean4

@[simp]
theorem toKernelSubobject_arrow {M N : ModuleCat R} {f : M ⟶ N} (x : LinearMap.ker f.hom) :
    (kernelSubobject f).arrow (toKernelSubobject x) = x.1 := by
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10959): the whole proof was just `simp [toKernelSubobject]`.
  simp [toKernelSubobject, -hom_comp, ← ConcreteCategory.comp_apply]

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