lift_mapBiprod — Mathlib

English

The lift map after applying F maps to the lift of the mapped f,g via F.map and (F.mapBiprod X Y).inv, i.e., the universal property is preserved under F.

Русский

Лифт-отображение после применения F соответствует лифту отображённых f,g через F.map и (F.mapBiprod X Y).inv, то есть универсальное свойство сохраняется под F.

LaTeX

$$$\\mathrm{biprod.lift}(F\\!f)(F\\!g) \\;\\circ\\; (F.mapBiprod X Y)^{-1} = F(\\mathrm{biprod.lift} f g)$$$

Lean4

theorem lift_mapBiprod (f : W ⟶ X) (g : W ⟶ Y) :
    biprod.lift (F.map f) (F.map g) ≫ (F.mapBiprod X Y).inv = F.map (biprod.lift f g) := by
  rw [← biprod.map_lift_mapBiprod, Category.assoc, Iso.hom_inv_id, Category.comp_id]

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