kernel_map_comp_kernelSubobjectIso_inv

English

There is a canonical isomorphism kernelSubobjectIsoComp between kernelSubobject (f ≫ g) and kernelSubobject g, compatible with kernels.

Русский

Существует каноническое отображение kernelSubobject(f ≫ g) ≅ kernelSubobject g, согласованное с ядрами.

LaTeX

$$$$ (kernelSubobjectIsoComp f g) : (kernelSubobject (f ≫ g) : C) \\cong (kernelSubobject g : C) $$$$

Lean4

@[reassoc]
theorem kernel_map_comp_kernelSubobjectIso_inv (sq : Arrow.mk f ⟶ Arrow.mk f') :
    kernel.map f f' sq.1 sq.2 sq.3.symm ≫ (kernelSubobjectIso _).inv =
      (kernelSubobjectIso _).inv ≫ kernelSubobjectMap sq :=
  by cat_disch

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