English
A variant asserting that under finite index, nontrivial summand implies some column nonzero property for iso.
Русский
Вариант, утверждающий, что для конечного индекса не тривиальный суммант порождает не нулевой столбец в изоморфизме.
LaTeX
$$$\text{Column Nonzero OfIso'}(s,f)\;:\; (∀ t, biproduct.ι_S(s) ≫ f ≫ biproduct.π_T(t) = 0) \Rightarrow 𝟙_{S_s}=0$$$
Lean4
theorem column_nonzero_of_iso' {σ τ : Type} [Finite τ] {S : σ → C} [HasBiproduct S] {T : τ → C} [HasBiproduct T] (s : σ)
(f : ⨁ S ⟶ ⨁ T) [IsIso f] : (∀ t : τ, biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → 𝟙 (S s) = 0 :=
by
cases nonempty_fintype τ
intro z
have reassoced {t : τ} {W : C} (h : _ ⟶ W) : biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h := by grind
set x := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
have h₁ : x = 𝟙 (S s) := by simp [x]
have h₀ : x = 0 := by
dsimp [x]
rw [← Category.id_comp (inv f), Category.assoc, ← biproduct.total]
simp only [comp_sum_assoc]
conv_lhs =>
congr
congr
next => skip
intro j; simp only [reassoced]
simp
exact h₁.symm.trans h₀
