English
If an iso between biproducts exists with nontrivial direct summands, then some matrix entry is nonzero.
Русский
Если существует изоморфизм между биопродуктами с не тривиальными разложениями, тогда найдется ненулевой элемент в матрице перехода.
LaTeX
$$$\exists t, biprod.ι_S(s) ≫ f ≫ biprod.π_T(t) \neq 0$$$
Lean4
/-- If `f : ⨁ S ⟶ ⨁ T` is an isomorphism, and `s` is a non-trivial summand of the source,
then there is some `t` in the target so that the `s, t` matrix entry of `f` is nonzero.
-/
def columnNonzeroOfIso {σ τ : Type} [Fintype τ] {S : σ → C} [HasBiproduct S] {T : τ → C} [HasBiproduct T] (s : σ)
(nz : 𝟙 (S s) ≠ 0) (f : ⨁ S ⟶ ⨁ T) [IsIso f] : Trunc (Σ' t : τ, biproduct.ι S s ≫ f ≫ biproduct.π T t ≠ 0) := by
classical
apply truncSigmaOfExists
have t := Biproduct.column_nonzero_of_iso'.{v} s f
by_contra h
simp only [not_exists_not] at h
exact nz (t h)
