Lean4
/-- A formal direct factor `P : Karoubi C` of an object `P.X : C` in a
preadditive category is actually a direct factor of the image `(toKaroubi C).obj P.X`
of `P.X` in the category `Karoubi C` -/
def decomposition (P : Karoubi C) : P ⊞ P.complement ≅ (toKaroubi _).obj P.X
where
hom := biprod.desc P.decompId_i P.complement.decompId_i
inv := biprod.lift P.decompId_p P.complement.decompId_p
hom_inv_id := by
apply biprod.hom_ext'
· rw [biprod.inl_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc, add_eq_left, ← assoc]
refine (?_ =≫ _).trans zero_comp
ext
simp only [comp_f, toKaroubi_obj_X, decompId_i_f, decompId_p_f, complement_p, comp_sub, comp_id, idem, sub_self,
zero_def]
· rw [biprod.inr_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc, add_eq_right, ← assoc]
refine (?_ =≫ _).trans zero_comp
ext
simp only [complement_X, comp_f, decompId_i_f, complement_p, decompId_p_f, sub_comp, id_comp, idem, sub_self,
zero_def]
inv_hom_id := by
ext
simp only [toKaroubi_obj_X, biprod.lift_desc, add_def, comp_f, decompId_p_f, decompId_i_f, idem, complement_X,
complement_p, comp_sub, comp_id, sub_comp, id_comp, sub_self, sub_zero, add_sub_cancel, id_f, toKaroubi_obj_p]
