map_lift_kernelComparison — Mathlib

English

For HasKernel f and HasKernel (G.map f), and a map h with h ≫ f = 0, the map G.map (kernel.lift f h w) composes with kernelComparison as described by the lifted objects.

Русский

Для f с ядром и G.map f с ядрами, при h с условием h ≫ f = 0, выполняется равенство, связывающее G.map (kernel.lift f h w) и kernelComparison через соответствующие подстановки.

LaTeX

$$$G.map (kernel.lift f h w) \;\circ\; kernelComparison f G = kernel.lift (G.map f) (G.map h) (by \;simp)$$$

Lean4

@[reassoc (attr := simp)]
theorem map_lift_kernelComparison [HasKernel f] [HasKernel (G.map f)] {Z : C} {h : Z ⟶ X} (w : h ≫ f = 0) :
    G.map (kernel.lift _ h w) ≫ kernelComparison f G =
      kernel.lift _ (G.map h) (by simp only [← G.map_comp, w, Functor.map_zero]) :=
  by ext; simp [← G.map_comp]

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