English
In a finite setting, the left distributor is determined by its action on the biproduct components; if two morphisms agree after precomposition with every biproduct injection, they are equal.
Русский
Для конечного набора индексов достаточно проверить равенство на каждом инъекторе двоичного двупродукта; если два морфизма дают одинаковые композиции после пробных вложений, то они равны.
LaTeX
$$$$\\big(\\forall j, (X \\triangleleft \\mathrm{biproduct}.\\mathrm{ι}_f j) \\circ g = (X \\triangleleft \\mathrm{biproduct}.\\mathrm{ι}_f j) \\circ h\\big) \\Rightarrow g = h,$$$$
Lean4
@[ext]
theorem leftDistributor_ext_left {J : Type} [Finite J] {X Y : C} {f : J → C} {g h : X ⊗ ⨁ f ⟶ Y}
(w : ∀ j, (X ◁ biproduct.ι f j) ≫ g = (X ◁ biproduct.ι f j) ≫ h) : g = h := by
classical
cases nonempty_fintype J
apply (cancel_epi (leftDistributor X f).inv).mp
ext
simp [w]
