kernel_map_comp_preserves_kernel_iso_inv

English

For any g with HasKernel and preserved by G, the map of kernels is compatible with the iso.

Русский

Для любой g с существующим ядром и сохранением через G отображение ядер совместимо с изоморфизмом.

LaTeX

$$$kernel.map (G.map f) (G.map g) (G.map p) (G.map q) \\; ≈ \\; (PreservesKernel.iso G f)^{-1} \\circ G.map (kernel.map f g p q hpq) $$$

Lean4

@[reassoc]
theorem kernel_map_comp_preserves_kernel_iso_inv {X' Y' : C} (g : X' ⟶ Y') [HasKernel g] [HasKernel (G.map g)]
    [PreservesLimit (parallelPair g 0) G] (p : X ⟶ X') (q : Y ⟶ Y') (hpq : f ≫ q = p ≫ g) :
    kernel.map (G.map f) (G.map g) (G.map p) (G.map q) (by rw [← G.map_comp, hpq, G.map_comp]) ≫
        (PreservesKernel.iso G _).inv =
      (PreservesKernel.iso G _).inv ≫ G.map (kernel.map f g p q hpq) :=
  by
  rw [Iso.comp_inv_eq, Category.assoc, PreservesKernel.iso_hom, Iso.eq_inv_comp, PreservesKernel.iso_hom,
    kernelComparison_comp_kernel_map]

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