diagramIsoPair — Mathlib

English

Every functor out of the walking pair is naturally isomorphic (indeed equal) to the pair formed by its values on left and right.

Русский

Каждый функтор из WalkingPair естественно изоморфен (и на самом деле равен) паре, составленной из значений на слева и справа.

LaTeX

$$$$ F \cong \text{pair}(F(left), F(right)). $$$$

Lean4

/-- Every functor out of the walking pair is naturally isomorphic (actually, equal) to a `pair` -/
@[simps!]
def diagramIsoPair (F : Discrete WalkingPair ⥤ C) : F ≅ pair (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩) :=
  mapPairIso (Iso.refl _) (Iso.refl _)

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