lift_map — Mathlib

English

For appropriate W, X, Y, Z with binary products, and morphisms f,g,h,k of suitable domains, we have prod.lift f g ≫ prod.map h k = prod.lift (f ≫ h) (g ≫ k).

Русский

Для подходящих объектов и морфизмов выполняется prod.lift f g ⋅ prod.map h k = prod.lift (f ⋅ h) (g ⋅ k).

LaTeX

$$$prod.lift f g \\;\\\\circ \\\\prod.map h k = prod.lift (f \\circ h) (g \\circ k)$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_map {V W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y)
    (k : X ⟶ Z) : prod.lift f g ≫ prod.map h k = prod.lift (f ≫ h) (g ≫ k) := by ext <;> simp

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