English
If f: W ⊞ X → Y ⊞ Z is an isomorphism, then either 1_W = 0 or at least one of the two first-column projections of f is nonzero.
Русский
Если f: W ⊞ X → Y ⊞ Z изоморфизм, то либо 1_W = 0, либо хотя бы одна из двух первых столбцов не нулевая.
LaTeX
$$$\text{IsIso}(f) \implies (\mathbf{1}_W = 0 \lor (\mathrm{biprod.inl} \circ f \circ \mathrm{biprod.fst} \neq 0) \lor (\mathrm{biprod.inl} \circ f \circ \mathrm{biprod.snd} \neq 0))$$$
Lean4
theorem column_nonzero_of_iso {W X Y Z : C} (f : W ⊞ X ⟶ Y ⊞ Z) [IsIso f] :
𝟙 W = 0 ∨ biprod.inl ≫ f ≫ biprod.fst ≠ 0 ∨ biprod.inl ≫ f ≫ biprod.snd ≠ 0 :=
by
by_contra! h
rcases h with ⟨nz, a₁, a₂⟩
set x := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
have h₁ : x = 𝟙 W := by simp [x]
have h₀ : x = 0 := by
dsimp [x]
rw [← Category.id_comp (inv f), Category.assoc, ← biprod.total]
conv_lhs =>
slice 2 3
rw [comp_add]
simp only [Category.assoc]
rw [comp_add_assoc, add_comp]
conv_lhs =>
congr
next => skip
slice 1 3
rw [a₂]
simp only [zero_comp, add_zero]
conv_lhs =>
slice 1 3
rw [a₁]
simp only [zero_comp]
exact nz (h₁.symm.trans h₀)
