English
There is an equivalence between Functors from a sum and the product of the functor categories: Fun(A ⊕ A', B) ≃ Fun(A,B) × Fun(A',B).
Русский
Существует эквивалентность между функторными категориями: Fun(A ⊕ A', B) ≃ Fun(A,B) × Fun(A',B).
LaTeX
$$\mathrm{Fun}(A \oplus A', B) \simeq \mathrm{Fun}(A,B) \times \mathrm{Fun}(A',B)$$
Lean4
/-- The equivalence between functors from a sum and the product of the functor categories. -/
@[simps]
def functorEquiv : A ⊕ A' ⥤ B ≌ (A ⥤ B) × (A' ⥤ B)
where
functor :=
{ obj F := ⟨inl_ A A' ⋙ F, inr_ A A' ⋙ F⟩
map η := ⟨whiskerLeft (inl_ A A') η, whiskerLeft (inr_ A A') η⟩ }
inverse :=
{ obj F := Functor.sum' F.1 F.2
map η := NatTrans.sum' η.1 η.2 }
unitIso := NatIso.ofComponents <| fun F ↦ F.isoSum
counitIso := NatIso.ofComponents <| fun F ↦ (Functor.inlCompSum' _ _).prod (Functor.inrCompSum' _ _) ≪≫ prod.etaIso F
