Uniqueness of the size of finite indecomposable decompositions

In an idempotent-complete preadditive category, finite decompositions into indecomposables with local endomorphism rings have a well-defined number of summands. Only the cardinal consequence of Krull--Schmidt uniqueness is recorded here; no global finite skeleton is required.

The cancellation argument is the label-free specialization of the finite Krull--Schmidt proof in the vendored Iyama cone.

theorem MagnitudeConjecture.CategoryTheory.exists_isIso_component_of_retraction_finBiproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {X : C} (hX : CategoryTheory.Indecomposable X) (hlocal : IsLocalRing (CategoryTheory.End X)) (n : ℕ) (Y : Fin n → C) (hY : ∀ (i : Fin n), CategoryTheory.Indecomposable (Y i)) (f : X ⟶ ⨁ Y) (g : ⨁ Y ⟶ X) (hfg : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id X) : ∃ (i : Fin n), CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biproduct.π Y i))

A retraction of an indecomposable object from a finite biproduct of indecomposables has an invertible coordinate when the source endomorphism ring is local.

theorem MagnitudeConjecture.CategoryTheory.eq_of_nonempty_iso_finBiproduct_of_indec_local {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] (n m : ℕ) (X : Fin n → C) (Y : Fin m → C) : (∀ (i : Fin n), CategoryTheory.Indecomposable (X i)) → (∀ (i : Fin n), IsLocalRing (CategoryTheory.End (X i))) → (∀ (j : Fin m), CategoryTheory.Indecomposable (Y j)) → Nonempty (⨁ X ≅ ⨁ Y) → n = m

Two finite biproducts of indecomposables with local endomorphism rings can be isomorphic only when their index types have the same cardinality.

theorem MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.n_eq_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {X Y : C} (dX : FiniteIndecomposableDecomposition X) (dY : FiniteIndecomposableDecomposition Y) (hlocal : ∀ (i : Fin dX.n), IsLocalRing (CategoryTheory.End (dX.summand i))) (e : X ≅ Y) : dX.n = dY.n

The number of summands in a displayed finite indecomposable decomposition is invariant under isomorphism.