map_comp — Mathlib

English

There is a natural equivalence between the costructured arrows for the product functor S.prod S' and the product of the costructured arrows for S and S'.

Русский

Существует естественное эквалентное соответствие между категорией costructuredArrow для продукта S.prod S' и произведением категорий costructuredArrow для S и для S'.

LaTeX

$$$$\text{CostructuredArrow} (S .\text{prod} S') (T,T') \;\simeq\; \text{CostructuredArrow} S T \times \text{CostructuredArrow} S' T'.$$$$

Lean4

@[simp]
theorem map_comp {f : S ⟶ S'} {f' : S' ⟶ S''} {h : StructuredArrow S'' T} :
    (map (f ≫ f')).obj h = (map f).obj ((map f').obj h) :=
  by
  rw [eq_mk h]
  simp

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