id_tensor_π_preserves_coequalizer_inv_desc

English

In a monoidal category with coequalizers preserved by tensor, a canonical isomorphism via the tensor-left preserves the coequalizer descents and their inverses align with the corresponding universal property.

Русский

В моноидальной категории с сохранением коэквализации под тензором, каноническое изоморфизм через tensor-left сохраняет desc и их обратные согласованы с универсальным свойством.

LaTeX

$$$(Z \triangleleft coequalizer.\pi f g) \;≫\; (PreservesCoequalizer.iso (tensorLeft Z) f g).inv \;≫\; coequalizer.desc h wh = h.$$$

Lean4

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

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