English
Let f : α → C and g : β → C be diagrams with coproducts, and let p : α → β and q : ∀ a ∈ α, f a ⟶ g (p a) be a family of morphisms. Then for each a ∈ α, the injection into the left coproduct followed by the canonical map Sigma.map' equals the morphism q a followed by the corresponding injection into the right coproduct.
Русский
Пусть f : α → C и g : β → C задают диаграммы с копродуктами, и пусть p : α → β и q : ∀ a ∈ α, f a ⟶ g (p a) — семейство морфизмов. Тогда для каждого a ∈ α верна несовместимость инъекции в левый копроизведение с каноническим отображением Sigma.map' и q a, затем инъекция в правое копродукт.
LaTeX
$$$\Sigma.ι f a \;\circ\; \Sigma.map' p q \\= q a \;\circ\; \Sigma.ι g (p a)$$$
Lean4
@[reassoc (attr := simp)]
theorem ι_comp_map' {f : α → C} {g : β → C} [HasCoproduct f] [HasCoproduct g] (p : α → β) (q : ∀ (a : α), f a ⟶ g (p a))
(a : α) : Sigma.ι f a ≫ Sigma.map' p q = q a ≫ Sigma.ι g (p a) :=
colimit.ι_desc _ _
