mapPairIso — Mathlib

English

Given left and right isomorphisms f and g between F and G, there is a natural isomorphism F ≅ G with those components.

Русский

Даны иизоморфизмы слева и справа между F и G, существует натуральное изоморфизм F ≅ G с такими компонентами.

LaTeX

$$$$ \exists \alpha: F \cong G,\ \alpha(left)=f,\ \alpha(right)=g. $$$$

Lean4

/-- The natural isomorphism between two functors out of the walking pair, specified by its
components. -/
@[simps!]
def mapPairIso (f : F.obj ⟨left⟩ ≅ G.obj ⟨left⟩) (g : F.obj ⟨right⟩ ≅ G.obj ⟨right⟩) : F ≅ G :=
  NatIso.ofComponents
    (fun j ↦
      match j with
      | ⟨left⟩ => f
      | ⟨right⟩ => g)
    (fun ⟨⟨u⟩⟩ => by cat_disch)

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