app_zero_eq_comp_π_right — Mathlib

English

For objects A,B,X,Y in a category with colimits of shape Discrete WalkingPair, the following equality holds: coprod.map (id_X) f ≫ coprod.map g (id_B) = coprod.map g (id_A) ≫ coprod.map (id_Y) f.

Русский

Для объектов A,B,X,Y в категории с колимитами формы Discrete WalkingPair выполняется равенство: coprod.map(id_X) f ≫ coprod.map g(id_B) = coprod.map g(id_A) ≫ coprod.map(id_Y) f.

LaTeX

$$$\mathrm{coprod.map}(\mathrm{id}_X, f) \;\circ\; \mathrm{coprod.map}(g, \mathrm{id}_B) = \mathrm{coprod.map}(g, \mathrm{id}_A) \;\circ\; \mathrm{coprod.map}(\mathrm{id}_Y, f).$$$

Lean4

@[reassoc]
theorem app_zero_eq_comp_π_right (s : Cofork f g) : s.ι.app zero = g ≫ s.π := by
  rw [← s.app_one_eq_π, ← s.w right, parallelPair_map_right]

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