lift_map — Mathlib

English

For any morphism f, prod.lift (id X) 0 ≫ prod.map f f = f ≫ prod.lift (id Y) 0.

Русский

Для любого отображения f верна тождество с использованием lift и map на произведениях.

LaTeX

$$$\\operatorname{prod}.\\mathrm{lift}(\\mathrm{Id}_X,0) ≫ \\operatorname{prod}.\\mathrm{map} f f = f ≫ \\operatorname{prod}.\\mathrm{lift}(\\mathrm{Id}_Y,0)$$$

Lean4

@[reassoc]
theorem lift_map {X Y : C} (f : X ⟶ Y) : prod.lift (𝟙 X) 0 ≫ Limits.prod.map f f = f ≫ prod.lift (𝟙 Y) 0 := by simp

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