kernelComparison_comp_ι — Mathlib

English

If HasKernel f and HasKernel (G.map f), then kernelComparison f G ≫ kernel.ι (G.map f) = G.map (kernel.ι f).

Русский

Если существуют ядра f и G.map f, то композиция kernelComparison f G с kernel.ι (G.map f) равна G.map (kernel.ι f).

LaTeX

$$$kernelComparison f G \;\circ\; kernel.ι (G.map f) = G.map (kernel.ι f)$$$

Lean4

@[reassoc (attr := simp)]
theorem kernelComparison_comp_ι [HasKernel f] [HasKernel (G.map f)] :
    kernelComparison f G ≫ kernel.ι (G.map f) = G.map (kernel.ι f) :=
  kernel.lift_ι _ _ _

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