diagonal' — Mathlib

English

There is a symmetry of the diagonal map in a bifunctor, expressing a dual version of the diagonal law: F.map (f × 𝟙) ≫ F.map (𝟙 × g) = F.map (f × g).

Русский

Существуют симметрии диагонального отображения в бифункторе, выражающие двойную диагональ: F.map (f × 𝟙) ≫ F.map (𝟙 × g) = F.map (f × g).

LaTeX

$$$F.map (f \\times 𝟙) \\;\\; \\; ≫ \\; F.map (𝟙 \\times g) = F.map (f \\times g)$$$

Lean4

@[simp]
theorem diagonal' (F : C × D ⥤ E) (X X' : C) (f : X ⟶ X') (Y Y' : D) (g : Y ⟶ Y') :
    F.map (f ×ₘ 𝟙 Y) ≫ F.map (𝟙 X' ×ₘ g) = F.map (f ×ₘ g) := by
  rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]

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