English
The sum of two natural transformations α : F ⟶ G and β : H ⟶ I is a natural transformation F.sum' H ⟶ G.sum' I defined componentwise by α on left parts and β on right parts, with naturality given by cases on the morphism.
Русский
Сумма двух натуральных преобразований α : F ⟶ G и β : H ⟶ I задаёт натуральное преобразование F.sum' H ⟶ G.sum' I, компонентно заданное α на левых частях и β на правых частях, с натуральностью по случаям на морфизм.
LaTeX
$$$ (\\alpha, \\beta) : (F \\sum' H) \\rightarrow (G \\sum' I) $ с определением на инклузиях: $((F \\sum' H).map f) = \\begin{cases} \\alpha.app X, & X \\text{ в A}, \\\\ \\beta.app X, & X \\text{ в B}. \\end{cases} $$$
Lean4
/-- The sum of two natural transformations, where all functors have the same target category. -/
def sum' {F G : A ⥤ C} {H I : B ⥤ C} (α : F ⟶ G) (β : H ⟶ I) : F.sum' H ⟶ G.sum' I
where
app
X :=
match X with
| inl X => α.app X
| inr X => β.app X
naturality X Y f := by cases f <;> simp
