inl_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 the commutation biprod.inl ≫ biprod.map f g = f ≫ biprod.inl.

Русский

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

LaTeX

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

Lean4

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

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