prodInverse — Mathlib

English

There is a natural equivalence between StructuredArrow (S,S')(T.prod T') and the product StructuredArrow S T × StructuredArrow S' T'.

Русский

Существует естественная эквивалентность между StructuredArrow (S,S')(T.prod T') и произведением StructuredArrow S T × StructuredArrow S' T'.

LaTeX

$$$prodEquivalence : StructuredArrow (S,S') (T.prod T') \simeq StructuredArrow S T \times StructuredArrow S' T'$$$

Lean4

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

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