Label weights in a finite Krull--Schmidt category

Isomorphic displayed decompositions into the chosen indecomposable skeleton have equal sums under every commutative-monoid-valued label weight. It follows that an arbitrary integer-valued label weight extends to an isomorphism-invariant, biproduct-additive weight on all objects.

This is the classification-free weight extension used in Iyama's strictness argument.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.sum_weight_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) {M : Type z} [AddCommMonoid M] (weight : Ind → M) (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)) → ∑ i : Fin n, weight (source i) = ∑ j : Fin m, weight (target j)

Isomorphic displayed decompositions have the same total under every commutative-monoid-valued label weight.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.label_multiplicity_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) [DecidableEq Ind] (p : Ind) (n m : ℕ) (source : Fin n → Ind) (target : Fin m → Ind) (e : Nonempty ((⨁ fun (i : Fin n) => T.obj (source i)) ≅ ⨁ fun (j : Fin m) => T.obj (target j))) : (∑ i : Fin n, if source i = p then 1 else 0) = ∑ j : Fin m, if target j = p then 1 else 0

In particular, every chosen indecomposable label occurs with the same multiplicity in two isomorphic displayed decompositions.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.chosenDecompositionSize {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) : ℕ

Number of factors in one noncomputably chosen decomposition.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.chosenDecompositionLabel {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) : Fin (T.chosenDecompositionSize X) → Ind

Labels in one noncomputably chosen decomposition.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.chosenDecompositionIso {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) : X ≅ ⨁ fun (i : Fin (T.chosenDecompositionSize X)) => T.obj (T.chosenDecompositionLabel X i)

The isomorphism exhibiting the chosen decomposition.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.chosenLabelWeight {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) (weight : Ind → ℤ) (X : C) : ℤ

Sum a label weight over the chosen finite decomposition of an object.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.chosenLabelWeight_iso_invariant {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) (weight : Ind → ℤ) {X Y : C} (e : Nonempty (X ≅ Y)) : T.chosenLabelWeight weight X = T.chosenLabelWeight weight Y

Chosen label weight is invariant under object isomorphism.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.chosenLabelWeight_biprod_additive {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) (weight : Ind → ℤ) (X Y : C) : T.chosenLabelWeight weight (X ⊞ Y) = T.chosenLabelWeight weight X + T.chosenLabelWeight weight Y

Chosen label weight is additive under binary biproducts.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.additiveObjectWeightOfLabelWeight {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) (weight : Ind → ℤ) : AdditiveObjectWeight C

Every integer-valued weight on the chosen indecomposable labels extends canonically (up to the irrelevant decomposition choice) to an isomorphism-invariant additive object weight.

@[simp]

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.additiveObjectWeightOfLabelWeight_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) (weight : Ind → ℤ) (A : Ind) : (T.additiveObjectWeightOfLabelWeight weight).weight (T.obj A) = weight A