kernelSubobjectIso_comp_kernel_map

English

For a square sq between f, f', f'', the relation between kernel.map, kernelSubobjectIso and kernelSubobjectMap is that the two canonical ways of transporting kernels agree up to composition with iso inverses.

Русский

При квадрате между f, f', f'' согласование отображения ядра через kernelSubobjectIso и kernelSubobjectMap согласуется через обращения изоморфизмов.

LaTeX

$$$$ (kernel.map f f' \\; sq.left \\; sq.right) \\; \\gg (kernelSubobjectIso f').inv = (kernelSubobjectIso f).inv \\; \\gg kernelSubobjectMap sq $$$$

Lean4

@[reassoc]
theorem kernelSubobjectIso_comp_kernel_map (sq : Arrow.mk f ⟶ Arrow.mk f') :
    (kernelSubobjectIso _).hom ≫ kernel.map f f' sq.1 sq.2 sq.3.symm =
      kernelSubobjectMap sq ≫ (kernelSubobjectIso _).hom :=
  by simp [← Iso.comp_inv_eq, kernel_map_comp_kernelSubobjectIso_inv]

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