prodInverse — Mathlib

English

Implementation of the inverse for the product equivalence between costructured arrows; it acts componentwise on the left and right parts.

Русский

Реализация обратного для произведения эквивалентности costructured arrows; действует по компонентам слева и справа.

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 prodInverse : CostructuredArrow S T × CostructuredArrow S' T' ⥤ CostructuredArrow (S.prod S') (T, T')
    where
  obj f := .mk (Y := (f.1.left, f.2.left)) ⟨f.1.hom, f.2.hom⟩
  map η := CostructuredArrow.homMk ⟨η.1.left, η.2.left⟩ (by simp)

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