imageToKernel'_kernelSubobjectIso

English

In the same setting as above, the dual compatibility holds: the induced map from the image-to-kernel construction interacts with the kernel-subobject iso in a precise way, yielding an equality of composites.

Русский

В той же обстановке выполняется двойственная совместимость: индуцированное отображение из образа в ядро взаимодействует с изоморфизмом ядро-подобъекта так, что композиции совпадают.

LaTeX

$$$\\text{imageToKernel}'\\; f\\; g\\; w \\; \\circ \\; (\\kerSubobjectIso g).inv = (\\imageSubobjectIso f).inv \\circ \\text{imageToKernel } f\\; g\\; w$$$

Lean4

@[simp]
theorem imageToKernel'_kernelSubobjectIso (w : f ≫ g = 0) :
    imageToKernel' f g w ≫ (kernelSubobjectIso g).inv = (imageSubobjectIso f).inv ≫ imageToKernel f g w :=
  by
  ext
  simp [imageToKernel']

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