English
A functor out of a sum is uniquely characterized by its precompositions with the two inclusions. If F,G are functors A ⊕ B ⥤ C with isomorphisms e1: (inl)⋙F ≅ (inl)⋙G and e2: (inr)⋙F ≅ (inr)⋙G, then there exists a natural isomorphism F ≅ G whose left and right components agree with e1 and e2 respectively.
Русский
Функтор исходящий из суммы уникально определяется своими предобразами по двумя инъекциям. Пусть F,G : A ⊕ B ⥤ C и существуют изоморфизмы e1: (inl)⋙F ≅ (inl)⋙G и e2: (inr)⋙F ≅ (inr)⋙G. Тогда существует естественный изоморфизм F ≅ G, для которого левые и правые компоненты совпадают с e1 и e2 соответственно.
LaTeX
$$$ F \\cong G \\quad\\text{при условии} \\quad (inl\\,\\_\\_ )\\!\\circ F \\cong (inl\\,\\_\\_ )\\!\\circ G \\land (inr\\,\\_\\_ )\\!\\circ F \\cong (inr\\,\\_\\_ )\\!\\circ G. $$$$
Lean4
/-- A functor out of a sum is uniquely characterized by its precompositions with `inl_` and `inr_`.
-/
def sumIsoExt : F ≅ G :=
NatIso.ofComponents
(fun x ↦
match x with
| inl x => e₁.app x
| inr x => e₂.app x)
(fun {x y} f ↦ by
cases f
· simpa using e₁.hom.naturality _
· simpa using e₂.hom.naturality _)
