English
A dual extensionality property: if a map agrees on all right component injections after left distribution, then the two maps coincide.
Русский
Двойственное экстрансиальное свойство: если отображение согласовано на всех впрысках правого компонента после левого распределителя, то два отображения совпадают.
LaTeX
$$$$\\big(\\forall j, (\\mathrm{leftDistributor}(X,f) \\otimes^{\\mathrm{I}} \\mathrm{asIso}(\\mathrm{Id}_Y)) \\to g_j = h_j \\big) \\Rightarrow g=h,$$$$
Lean4
@[ext]
theorem leftDistributor_ext_right {J : Type} [Finite J] {X Y : C} {f : J → C} {g h : X ⟶ Y ⊗ ⨁ f}
(w : ∀ j, g ≫ (Y ◁ biproduct.π f j) = h ≫ (Y ◁ biproduct.π f j)) : g = h := by
classical
cases nonempty_fintype J
apply (cancel_mono (leftDistributor Y f).hom).mp
ext
simp [w]
-- One might wonder how many iterated tensor products we need simp lemmas for.
-- The answer is two: this lemma is needed to verify the pentagon identity.
