The exchange step of Krull–Schmidt

An object with local endomorphism ring which is a retract of a finite biproduct is a retract of one of the summands; a retract with nonzero source of an object with local endomorphism ring is an isomorphism. These are used in Lemma 4.6 ("Decomposing the latter over the finitely many indecomposable B-modules shows that only finitely many isomorphism classes can occur", scalar-normalization.tex).

theorem MultiplicativeBasisDeformations.isIso_of_isUnit_end {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X : C} {f : CategoryTheory.End X} (hf : IsUnit f) : CategoryTheory.IsIso (have this := f; this)

theorem MultiplicativeBasisDeformations.exists_retract_summand {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {M : C} [IsLocalRing (CategoryTheory.End M)] {ι : Type} [Fintype ι] (Y : ι → C) [CategoryTheory.Limits.HasBiproduct Y] (i : M ⟶ ⨁ Y) (p : ⨁ Y ⟶ M) (h : CategoryTheory.CategoryStruct.comp i p = CategoryTheory.CategoryStruct.id M) : ∃ (j : ι) (i' : M ⟶ Y j) (p' : Y j ⟶ M), CategoryTheory.CategoryStruct.comp i' p' = CategoryTheory.CategoryStruct.id M

Exchange: a retract with local endomorphism ring of a finite biproduct is a retract of one summand.

theorem MultiplicativeBasisDeformations.isIso_of_retract {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {M Y : C} [IsLocalRing (CategoryTheory.End Y)] (hM : ¬CategoryTheory.Limits.IsZero M) (i : M ⟶ Y) (p : Y ⟶ M) (h : CategoryTheory.CategoryStruct.comp i p = CategoryTheory.CategoryStruct.id M) : CategoryTheory.IsIso i

A retract with nonzero source of an object with local endomorphism ring is an isomorphism.