prodEquivalence — Mathlib

English

There is a canonical equivalence between StructuredArrow (S,S')(T.prod T') and 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

/-- The natural equivalence
`StructuredArrow (S, S') (T.prod T') ≌ StructuredArrow S T × StructuredArrow S' T'`. -/
@[simps]
def prodEquivalence : StructuredArrow (S, S') (T.prod T') ≌ StructuredArrow S T × StructuredArrow S' T'
    where
  functor := StructuredArrow.prodFunctor S S' T T'
  inverse := StructuredArrow.prodInverse S S' T T'
  unitIso := NatIso.ofComponents (fun f => Iso.refl _) (by simp)
  counitIso := NatIso.ofComponents (fun f => Iso.refl _) (by simp)

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