English
The sum bifunctor defines a functor from the product of the I-indexed and J-indexed families to the I ⊕ J-indexed family, with explicit action on objects and morphisms as described by the Sum.elim construction.
Русский
Бифунктор-sum задаёт функтор из произведения семей по индексам I и J в семью, индексированную по I ⊕ J, с явным действием на объекты и морфизмы через конструктор Sum.elim.
LaTeX
$$$\\text{sum} : (\\forall i, C_i) \\;⥤\\; (\\forall j, D_j) \\;⥤\\; \\forall s: I \\oplus J, \\mathrm{Sum.elim}\\,C D\,s$$$
Lean4
/-- The bifunctor combining an `I`-indexed family of objects with a `J`-indexed family of objects
to obtain an `I ⊕ J`-indexed family of objects.
-/
@[simps]
def sum : (∀ i, C i) ⥤ (∀ j, D j) ⥤ ∀ s : I ⊕ J, Sum.elim C D s
where
obj
X :=
{ obj := fun Y s =>
match s with
| .inl i => X i
| .inr j => Y j
map := fun {_} {_} f s =>
match s with
| .inl i => 𝟙 (X i)
| .inr j => f j }
map {X} {X'}
f :=
{
app := fun Y s =>
match s with
| .inl i => f i
| .inr j => 𝟙 (Y j) }
