π_tensor_id_preserves_coequalizer_inv_desc

English

In the tensor-right setting, the dual statement expresses how the coequalizer π interacts with a colimMap after applying a right tensor action, preserving the desc to h.

Русский

В правой настройке тензорирования двойной параллельной пары, аналогично, описывается, как коэквалайзер π взаимодействует с colimMap после применения правого действия, сохраняя descended к h.

LaTeX

$$$(Y \triangleleft coequalizer.π f g) \;≫\; (PreservesCoequalizer.iso (tensorRight Z) f g).inv \;≫\; coequalizer.desc h wh = h.$$$

Lean4

theorem π_tensor_id_preserves_coequalizer_inv_desc {W X Y Z : C} (f g : X ⟶ Y) (h : Y ⊗ Z ⟶ W)
    (wh : (f ▷ Z) ≫ h = (g ▷ Z) ≫ h) :
    (coequalizer.π f g ▷ Z) ≫ (PreservesCoequalizer.iso (tensorRight Z) f g).inv ≫ coequalizer.desc h wh = h :=
  map_π_preserves_coequalizer_inv_desc (tensorRight Z) f g h wh

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