prod'_δ_snd — Mathlib

English

For the product of two monoidal functors F and G, the second component of the monoidal structure map δ at objects X and Y in C is exactly the δ-map of G at X and Y.

Русский

Для произведения двух моноидальных функторов F и G вторая компонента моноидальной структуры отображения δ в точках X, Y из C равна δ‑меподу G в X и Y.

LaTeX

$$$\\\\pi_2\\\\left(\\\\delta(\\\\mathrm{prod}' F G)(X,Y)\\\\right) = \\\\delta_G(X,Y).$$$

Lean4

@[simp]
theorem prod'_δ_snd (X Y : C) : (δ (prod' F G) X Y).2 = δ G X Y :=
  by
  change G.map (𝟙 _) ≫ _ = _
  rw [Functor.map_id, Category.id_comp]
  rfl

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