prodFunctor — Mathlib

English

Definition of the inverse functor for the product construction on costructured arrows; it sends a pair of costructured arrows to a costructured arrow for the product functor.

Русский

Определение обратного функторa для произведения в контекстеCostructuredArrow; он отправляет пару costructured arrows на costructured arrow для произведения.

LaTeX

$$$$ \text{prodInverse} : \text{CostructuredArrow } (S \times S') (T, T') \to \text{CostructuredArrow } S T \times \text{CostructuredArrow } S' T' .$$$$

Lean4

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

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