inr_map — Mathlib

English

Let W, X, Y, Z be objects with binary biproducts W ⊞ X and Y ⊞ Z. For f: W → Y and g: X → Z, we have biprod.inr ≫ biprod.map f g = g ≫ biprod.inr.

Русский

Пусть W, X, Y, Z — объекты с бинарными биобразованиями W ⊞ X и Y ⊞ Z. Для морфизмов f: W → Y, g: X → Z выполняется biprod.inr ≫ biprod.map f g = g ≫ biprod.inr.

LaTeX

$$$\mathrm{biprod.inr} \;\;≫\; \mathrm{biprod.map} \ f\ g = g \;\;≫\; \mathrm{biprod.inr}$$$

Lean4

@[reassoc (attr := simp)]
theorem inr_map {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
    biprod.inr ≫ biprod.map f g = g ≫ biprod.inr :=
  by
  rw [biprod.map_eq_map']
  exact IsColimit.ι_map (BinaryBiproduct.isColimit W X) _ _ ⟨WalkingPair.right⟩

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