English
The direct sum of two categories C and D, denoted C ⊕ D, is a category whose objects are either from C or from D, morphisms exist only within each summand, and identities and composition are defined accordingly by lifting via ULift where appropriate.
Русский
Прямая сумма категорий C и D, обозначаемая C ⊕ D, является категорией, чьи объекты принадлежат либо C, либо D; морфизмы существуют только внутри каждого слагаемого, тождества и композиция задаются соответственно через подъем через ULift.
LaTeX
$$$$ \text{Sum}(C,D) \text{ is the category with } \mathrm{Hom}(X,Y)=\\begin{cases} (X \\to Y) & X,Y\\in C, \\\\ \\text{empty} & X\\in C, Y\\in D \\\\ \\text{empty} & X\\in D, Y\\in C \\\\ (X \\to Y) & X,Y\\in D \end{cases} $$$$
Lean4
/-- `sum C D` gives the direct sum of two categories.
-/
instance sum : Category.{max v₁ v₂} (C ⊕ D)
where
Hom X
Y :=
match X, Y with
| inl X, inl Y => ULift.{max v₁ v₂} (X ⟶ Y)
| inl _, inr _ => PEmpty
| inr _, inl _ => PEmpty
| inr X, inr Y => ULift.{max v₁ v₂} (X ⟶ Y)
id
X :=
match X with
| inl X => ULift.up (𝟙 X)
| inr X => ULift.up (𝟙 X)
comp {X Y Z} f
g :=
match X, Y, Z, f, g with
| inl _, inl _, inl _, f, g => ULift.up <| f.down ≫ g.down
| inr _, inr _, inr _, f, g => ULift.up <| f.down ≫ g.down
