Lean4
/-- Every object in `Mat_ C` is isomorphic to the biproduct of its summands.
-/
@[simps]
def isoBiproductEmbedding (M : Mat_ C) : M ≅ ⨁ fun i => (embedding C).obj (M.X i)
where
hom := biproduct.lift fun i j _ => if h : j = i then eqToHom (congr_arg M.X h) else 0
inv := biproduct.desc fun i _ k => if h : i = k then eqToHom (congr_arg M.X h) else 0
hom_inv_id := by
simp only [biproduct.lift_desc]
funext i j
dsimp [id_def]
rw [Finset.sum_apply, Finset.sum_apply, Finset.sum_eq_single i]; rotate_left
· intro b _ hb
dsimp
rw [Fintype.univ_ofSubsingleton, Finset.sum_singleton, dif_neg hb.symm, zero_comp]
· intro h
simp at h
simp
inv_hom_id := by
apply biproduct.hom_ext
intro i
apply biproduct.hom_ext'
intro j
simp only [Category.id_comp, Category.assoc, biproduct.lift_π, biproduct.ι_desc_assoc, biproduct.ι_π]
ext ⟨⟩ ⟨⟩
simp only [embedding, comp_apply, comp_dite, dite_comp, comp_zero, zero_comp, Finset.sum_dite_eq', Finset.mem_univ,
ite_true, eqToHom_refl, Category.comp_id]
split_ifs with h
· subst h
simp
· rfl
