Unique decompositions without local End: split off summands by Hom-vanishing

To prove uniqueness of decompositions where End is not local (e.g. f.g. modules over a PID: End R = R), separate the bad summands with a purely preadditive lemma: if e : F ⊞ T ≅ F' ⊞ T' and every map T ⟶ F' and T' ⟶ F is zero, then F ≅ F' via inl ≫ e.hom ≫ fst (inverse inl ≫ e.inv ≫ fst) and T ≅ T' via inr ≫ e.hom ≫ snd. Proof: insert fst ≫ inl = 𝟙 - snd ≫ inr (from biprod.total, then abel) in the middle and kill the cross term with the Hom-vanishing; in simp only, pass both h and reassoc_of% h because the vanishing composite can appear with or without a tail. Then compare free parts by finrank and torsion parts by Krull–Schmidt (End(R/p^k) = R/p^k is local, via IsLocalRing.of_isUnit_or_isUnit_one_sub_self and coprimality, then IsLocalRing.of_surjective' along Algebra.lsmul). Lean plumbing: split ⨁ f by a predicate with (biproduct.whiskerEquiv (Equiv.sumCompl p) fun _ ↦ Iso.refl _).symm followed by a ⨁ (ι ⊕ κ) ≅ ⨁ ⊞ ⨁ iso; drop zero summands with Limits.isoBiprodZero (root Limits namespace, not biprod.). For the final σ, rcases hs : (Equiv.sumCompl _).symm i with x | x <;> obtain rfl : i = x.1 := by simpa using congrArg (Equiv.sumCompl _) hs works where simp with sumCompl_symm_apply_of_pos failed (DecidablePred instance mismatch under classical). In a derived category, sort the summands by degree using homologyFunctor n, mapBiproduct, isZero_of_isGE/isZero_of_isLE, and glue the per-degree bijections with Equiv.ofFiberEquiv (g (ofFiberEquiv e a) = f a holds by .2). FGModuleCat over a PID needs instance : HasFiniteBiproducts (FGModuleCat R) := .of_hasFiniteProducts; the Abelian path is not found.