Finite Krull--Schmidt cancellation and direct finiteness

Displayed decompositions into the chosen indecomposable skeleton have a well-defined total number of summands. Consequently every split-monic endomorphism is invertible. This is the categorical direct-finiteness input used in Iyama's ladder comparison.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.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] {Ind : Type w} [Fintype Ind] (T : FiniteRightTauCategoryData C Ind) (p : Ind) (n : ℕ) (label : Fin n → Ind) (f : T.obj p ⟶ ⨁ fun (i : Fin n) => T.obj (label i)) (g : (⨁ fun (i : Fin n) => T.obj (label i)) ⟶ T.obj p) (hfg : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id (T.obj p)) : ∃ (i : Fin n), CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biproduct.π (fun (j : Fin n) => T.obj (label j)) i))

A retraction of a chosen indecomposable from a finite biproduct has an invertible coordinate.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.eq_of_nonempty_iso_finBiproduct_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteRightTauCategoryData C Ind) (n m : ℕ) (source : Fin n → Ind) (target : Fin m → Ind) : Nonempty ((⨁ fun (i : Fin n) => T.obj (source i)) ≅ ⨁ fun (j : Fin m) => T.obj (target j)) → n = m

Two displayed finite biproducts of the chosen indecomposables can be isomorphic only when they have the same number of summands.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.finBiproductBiprodIsoSum {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {n m : ℕ} (F : Fin n → C) (G : Fin m → C) : (⨁ F) ⊞ ⨁ G ≅ ⨁ Sum.elim F G

A binary biproduct of two finite biproducts is the biproduct indexed by the sum of their index types.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.isIso_of_isSplitMono_end {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteRightTauCategoryData C Ind) {X : C} (f : X ⟶ X) [CategoryTheory.IsSplitMono f] : CategoryTheory.IsIso f

A split-monic endomorphism is invertible in the finite Krull--Schmidt category recorded by FiniteTauCategoryData.