Classifying indecomposables in Lean when End is not local: use idempotents

Mathlib's CategoryTheory.Indecomposable X (nonzero, every X ≅ Y ⊞ Z has a zero summand) has almost no API. A workable criterion: if every idempotent of X splits (e.g. IsIdempotentComplete C; isIdempotentComplete_of_abelian is an instance), then Indecomposable X ↔ ¬IsZero X ∧ ∀ e : X ⟶ X, e ≫ e = e → e = 0 ∨ e = 𝟙 X. (⇐) apply the hypothesis to α.hom ≫ biprod.fst ≫ biprod.inl ≫ α.inv. (⇒) split e and 𝟙 - e as (i,r), (i',r'), show i ≫ r' = 0 and i' ≫ r = 0, build X ≅ Y ⊞ Z with biprod.lift r r' / biprod.desc i i'. State idempotents as morphisms with e ≫ e = e rather than elements of End X (now a structure with End.of/asHom), so transport along a fully faithful additive functor is just F.map / hF.preimage. For modules, translate to Module.End R M with IsIdempotentElem; transport across M ≃ₗ N with hf.map e.conjRingEquiv and map_eq_zero_iff _ e.conjRingEquiv.injective / map_eq_one_iff. For R ⧸ I: every endomorphism is x ↦ x * f 1, so f idempotent ⇒ f 1 idempotent. Gotchas: rcases h with ⟨g⟩ | ⟨g⟩ on Nonempty A ∨ Nonempty B did NOT destructure the Nonempty; use hg | hg <;> obtain ⟨g⟩ := hg. Equiv.nontrivial goes from e : α ≃ β with [Nontrivial β] to Nontrivial α (no symm). A Nontrivial hypothesis introduced by rintro was not found by instance search in a later term; have := hM fixed it.