lift_comp_kernelIsoOfEq_hom — Mathlib

English

There is a commutative relation between kernel.lift and kernel.map when mapping between kernels of linked morphisms.

Русский

Существует коммутивное отношение между kernel.lift и kernel.map при отображении между ядрами связанных морфизмов.

LaTeX

$$$\\forall f,g\\; (w:\\; f\\circ g=0)\\; (f',g')\\; (w': f'\\circ g'=0)\\; (p:q):\\; X\\to X', (r:Z\\to Z')\\; (h1) (h2):\\;\\operatorname{IsKernel}\\; \\dots \\Rightarrow \\text{равенство между lifts и maps}$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_comp_kernelIsoOfEq_hom {Z} {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) (e : Z ⟶ X) (he) :
    kernel.lift _ e he ≫ (kernelIsoOfEq h).hom = kernel.lift _ e (by simp [← h, he]) := by subst h; simp

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