Weight transport along Iyama's invertible ladders

An isomorphism-invariant, binary-biproduct-additive integer weight preserves source-minus-target weight across any invertible-ladder step at which the right-mesh Euler identity holds. A global Euler hypothesis then gives constancy along a whole ladder and equality at the two boundary maps of a Nakayama pair.

structure QuotientSubmoduleEquidistribution.Iyama.AdditiveObjectWeight (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] : Type u

An isomorphism-invariant integral weight additive on binary biproducts.

• weight : C → ℤ
• iso_invariant {X Y : C} : Nonempty (X ≅ Y) → self.weight X = self.weight Y
• biprod_additive (X Y : C) : self.weight (X ⊞ Y) = self.weight X + self.weight Y

theorem QuotientSubmoduleEquidistribution.Iyama.AdditiveObjectWeight.weight_eq_zero_of_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (W : AdditiveObjectWeight C) {X : C} (hX : CategoryTheory.Limits.IsZero X) : W.weight X = 0

An additive object weight vanishes on every zero object.

theorem QuotientSubmoduleEquidistribution.Iyama.AdditiveObjectWeight.weight_finBiproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] (W : AdditiveObjectWeight C) (n : ℕ) (F : Fin n → C) : W.weight (⨁ F) = ∑ i : Fin n, W.weight (F i)

A binary-additive object weight is additive on Fin-indexed biproducts.

theorem QuotientSubmoduleEquidistribution.Iyama.AdditiveObjectWeight.weight_biproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] (W : AdditiveObjectWeight C) {J : Type w} [Fintype J] (F : J → C) : W.weight (⨁ F) = ∑ j : J, W.weight (F j)

A binary-additive object weight is additive on every finite biproduct.

def QuotientSubmoduleEquidistribution.Iyama.AdditiveObjectWeight.morphismWeight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (W : AdditiveObjectWeight C) {X Y : C} (_f : X ⟶ Y) : ℤ

Source-minus-target weight of a morphism.

def QuotientSubmoduleEquidistribution.Iyama.AdditiveObjectWeight.IsRightMeshEulerAt {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] (W : AdditiveObjectWeight C) (T : FiniteTauCategoryData C Ind) (Y : C) : Prop

The Euler identity for the chosen right mesh ending at Y.

def QuotientSubmoduleEquidistribution.Iyama.AdditiveObjectWeight.IsRightMeshEuler {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] (W : AdditiveObjectWeight C) (T : FiniteTauCategoryData C Ind) : Prop

The Euler identity holds at every chosen right mesh. This global condition is a convenient sufficient hypothesis; right-additive functions in Iyama's sense only provide it away from the projective boundary.

def QuotientSubmoduleEquidistribution.Iyama.AdditiveObjectWeight.IsRightMeshEulerOffProjectives {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] (W : AdditiveObjectWeight C) (T : FiniteTauCategoryData C Ind) : Prop

Iyama right-additivity gives the Euler identity on objects with no projective indecomposable summand.

theorem QuotientSubmoduleEquidistribution.Iyama.AdditiveObjectWeight.isRightMeshEulerOffProjectives_of_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 : FiniteTauCategoryData C Ind} (W : AdditiveObjectWeight C) (hobj : ∀ (x : Ind), ¬T.IsProjective x → W.IsRightMeshEulerAt T (T.obj x)) : W.IsRightMeshEulerOffProjectives T

Euler identities on the chosen nonprojective indecomposables propagate to every object supported on nonprojectives.

theorem QuotientSubmoduleEquidistribution.Iyama.AdditiveObjectWeight.morphismWeight_eq_of_arrowIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] (W : AdditiveObjectWeight C) {X Y X' Y' : C} {f : X ⟶ Y} {g : X' ⟶ Y'} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g) : W.morphismWeight f = W.morphismWeight g

Arrow isomorphisms preserve source-minus-target weight.

theorem QuotientSubmoduleEquidistribution.Iyama.AdditiveObjectWeight.morphismWeight_eq_of_invertibleLadderStep {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 : FiniteTauCategoryData C Ind} (W : AdditiveObjectWeight C) {XPrev YPrev XNext YNext : C} {aPrev : XPrev ⟶ YPrev} {aNext : XNext ⟶ YNext} (hstep : NakayamaLadder.InvertibleLadderStep T aPrev aNext) (hEuler : W.IsRightMeshEulerAt T YPrev) : W.morphismWeight aPrev = W.morphismWeight aNext

One invertible ladder square preserves source-minus-target weight.

theorem QuotientSubmoduleEquidistribution.Iyama.AdditiveObjectWeight.morphismWeight_eq_of_invertibleLadderOfDistance {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 : FiniteTauCategoryData C Ind} (W : AdditiveObjectWeight C) (hEuler : W.IsRightMeshEuler T) (n : ℕ) {X₀ Y₀ Xₙ Yₙ : C} {start : X₀ ⟶ Y₀} {finish : Xₙ ⟶ Yₙ} (h : NakayamaLadder.InvertibleLadderOfDistance T n start finish) : W.morphismWeight start = W.morphismWeight finish

Every two vertical arrows in a finite invertible ladder have the same source-minus-target weight.

theorem QuotientSubmoduleEquidistribution.Iyama.AdditiveObjectWeight.morphismWeight_eq_of_invertibleLadder {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 : FiniteTauCategoryData C Ind} (W : AdditiveObjectWeight C) (hEuler : W.IsRightMeshEuler T) {X₀ Y₀ Xₙ Yₙ : C} {start : X₀ ⟶ Y₀} {finish : Xₙ ⟶ Yₙ} (h : NakayamaLadder.InvertibleLadder T start finish) : W.morphismWeight start = W.morphismWeight finish

Source-minus-target weight is constant along any finite invertible ladder.

theorem QuotientSubmoduleEquidistribution.Iyama.AdditiveObjectWeight.morphismWeight_eq_of_invertibleLadderOfDistance_offProjectives {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 : FiniteTauCategoryData C Ind} (W : AdditiveObjectWeight C) (hEuler : W.IsRightMeshEulerOffProjectives T) (hSupport : NakayamaLadder.HasNonprojectiveRightSupport T) (n : ℕ) {X₀ Y₀ Xₙ Yₙ : C} {start : X₀ ⟶ Y₀} {finish : Xₙ ⟶ Yₙ} (h : NakayamaLadder.InvertibleLadderOfDistance T n start finish) : W.morphismWeight start = W.morphismWeight finish

The exact right-additive version of finite-ladder transport. Euler equality is required only on nonprojective-supported right endpoints, and hSupport is precisely Iyama's projective-free prefix theorem.

theorem QuotientSubmoduleEquidistribution.Iyama.AdditiveObjectWeight.morphismWeight_eq_of_invertibleLadder_offProjectives {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 : FiniteTauCategoryData C Ind} (W : AdditiveObjectWeight C) (hEuler : W.IsRightMeshEulerOffProjectives T) (hSupport : NakayamaLadder.HasNonprojectiveRightSupport T) {X₀ Y₀ Xₙ Yₙ : C} {start : X₀ ⟶ Y₀} {finish : Xₙ ⟶ Yₙ} (h : NakayamaLadder.InvertibleLadder T start finish) : W.morphismWeight start = W.morphismWeight finish

Source-minus-target weight is constant along a finite ladder under the precise off-projective Euler and support hypotheses.

theorem QuotientSubmoduleEquidistribution.Iyama.AdditiveObjectWeight.morphismWeight_muMinus_eq_muPlus_of_nakayamaPair {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 : FiniteTauCategoryData C Ind} (W : AdditiveObjectWeight C) (hEuler : W.IsRightMeshEuler T) {A B : Ind} (h : T.NakayamaPair A B) : W.morphismWeight (T.muMinus A) = W.morphismWeight (T.muPlus B)

The two endpoint maps of a genuine Nakayama pair have equal source-minus-target weight.

theorem QuotientSubmoduleEquidistribution.Iyama.AdditiveObjectWeight.morphismWeight_muMinus_eq_muPlus_of_nakayamaPair_offProjectives {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 : FiniteTauCategoryData C Ind} (W : AdditiveObjectWeight C) (hEuler : W.IsRightMeshEulerOffProjectives T) (hSupport : NakayamaLadder.HasNonprojectiveRightSupport T) {A B : Ind} (h : T.NakayamaPair A B) : W.morphismWeight (T.muMinus A) = W.morphismWeight (T.muPlus B)

A genuine Nakayama pair has equal endpoint weights under Iyama's exact off-projective hypotheses.