Multiplicities under contragredient duality

A label-aligned anti-equivalence preserves finite Krull--Schmidt multiplicities. For module skeletons, the two-sided tau-category identity then rewrites an arrow leaving a noninjective module as an arrow entering its inverse Auslander--Reiten translate. These are the two numerical transports used by the manuscript's negative new-mesh construction.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecomposableMultiplicity_map_alignedAntiEquivalence {k A C : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Ring C] [Algebra k C] [FiniteDimensional k C] [IsNoetherianRing Cᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (T : FiniteIndecomposableSkeleton k C) (D : S.almostSplitSkeleton.AlignedAntiEquivalence T.almostSplitSkeleton) (p : Fin S.n) (M : FinitelyGeneratedCategory A) : T.indecomposableMultiplicity (D.labelEquiv p) (D.categoryEquiv.functor.obj (Opposite.op M)) = S.indecomposableMultiplicity p M

A label-aligned anti-equivalence preserves the multiplicity of every selected indecomposable in every finitely generated module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredient_arrowMultiplicity_eq_reverse {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] (x : { i : Fin S.n // ¬CategoryTheory.Injective (S.fgObj i) }) (y : Fin S.n) : FiniteTauMatrix.arrowMultiplicity S.contragredientSkeleton.finiteTauCategoryData.toFiniteRightTauCategoryData y ↑(S.contragredientNonprojectiveLabel x) = FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑x) y

An ambient arrow between selected modules reverses under contragredient duality. The proof compares the dual right almost-split middle with the original left almost-split middle and then uses translation invariance of arrow multiplicities.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientSkeleton_hasAcyclicNonzeroNonisomorphisms {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] (H : S.HasAcyclicNonzeroNonisomorphisms) : S.contragredientSkeleton.HasAcyclicNonzeroNonisomorphisms

Cycle-freeness of nonzero nonisomorphisms is preserved by the label-aligned contragredient skeleton. An opposite arrow is carried back to an original arrow with its direction reversed, so an opposite cycle would give an original cycle.