kernel_eq_kernel — Mathlib

English

For any i, j with r: c.Rel i j, the kernel subobject of the differential from i to j equals the kernel subobject of the differential from i to the current target i.e., kernelSubobject (C.dFrom i) = kernelSubobject (C.d i j).

Русский

Для любых i, j с r: Rel i j верно, что ядро отображения из i в j совпадает с ядром отображения из i в i (то есть kernelSubobject (C.dFrom i) = kernelSubobject (C.d i j)).

LaTeX

$$$\\\\text{kernelSubobject}(C.dFrom i) = \\\\text{kernelSubobject}(C.d i j)$$$

Lean4

theorem kernel_eq_kernel [HasKernels V] {i j j' : ι} (r : c.Rel i j) (r' : c.Rel i j') :
    kernelSubobject (C.d i j) = kernelSubobject (C.d i j') :=
  by
  rw [← d_comp_eqToHom C r r']
  apply kernelSubobject_comp_mono

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