prodFunctor — Mathlib

English

There is a functor inverse to prod that sends a pair of costructured arrows to a structured arrow in the product category, respecting left/right projections.

Русский

Существуют инверсии к операции произведения: она отправляет пару коструктурированных стрелок в структурированную стрелку в произведении категорий, сохраняя левую/правую проекции.

LaTeX

$$$prodInverse : CostructuredArrow S T × CostructuredArrow S' T' ⥤ CostructuredArrow (S.prod S') (T, T')$$$

Lean4

/-- Implementation; see `StructuredArrow.prodEquivalence`. -/
@[simps]
def prodFunctor : StructuredArrow (S, S') (T.prod T') ⥤ StructuredArrow S T × StructuredArrow S' T'
    where
  obj f := ⟨.mk f.hom.1, .mk f.hom.2⟩
  map η := ⟨StructuredArrow.homMk η.right.1 (by simp), StructuredArrow.homMk η.right.2 (by simp)⟩

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