sumIsoExt_hom_app_inr — Mathlib

English

Let F,G : A ⊕ B ⥤ C with e1 : (inl)⋙F ≅ (inl)⋙G and e2 : (inr)⋙F ≅ (inr)⋙G. Then the inverse of the resulting iso F ≅ G has left component given by e1.inv.app a on inl a.

Русский

Пусть F,G : A ⊕ B ⥤ C с e1 : (inl)⋙F ≅ (inl)⋙G и e2 : (inr)⋙F ≅ (inr)⋙G. Тогда обратный изоморфизм F ≅ G имеет левый компонент равный e1.inv.app a на элементе inl a.

LaTeX

$$$ (\\text{sumIsoExt } e_1 e_2)^{-1}.\\text{app} (\\mathrm{inl}\\, a) = e_1^{-1}.\\text{app} a $$$

Lean4

@[simp]
theorem sumIsoExt_hom_app_inr (b : B) : (sumIsoExt e₁ e₂).hom.app (inr b) = e₂.hom.app b :=
  rfl

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