π_mapOfIsColimit — Mathlib

English

For cc an IsColimit cokernel cofork of f, and cc' for f', and φ between Arrow mk f and Arrow mk f', the equality involving cc.π and mapOfIsColimit hf cc' φ holds, expressing functoriality of π.

Русский

Для cc — изколимитного коканалового когорка над f и cc' над f', и φ между стрелками f и f', выполняется равенство cc.π ≫ mapOfIsColimit hf cc' φ = φ.right ≫ cc'.π.

LaTeX

$$$\forall cc hf cc'\; (φ):\; cc.π \;≫\; mapOfIsColimit hf cc' φ = φ.right \;≫\; cc'.π$$$

Lean4

@[reassoc (attr := simp)]
theorem π_mapOfIsColimit {cc : CokernelCofork f} (hf : IsColimit cc) (cc' : CokernelCofork f')
    (φ : Arrow.mk f ⟶ Arrow.mk f') : cc.π ≫ mapOfIsColimit hf cc' φ = φ.right ≫ cc'.π :=
  hf.fac _ _

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