Translation invariance of right-module arrow multiplicities

For a finite skeleton of indecomposable right modules, compatibility of the canonical left and right Auslander--Reiten meshes identifies arrows out of a noninjective label with arrows into its inverse translate. This numerical identity is independent of directedness and supplies the polarization of the standard-form mesh category.

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

In the ambient module skeleton, arrow multiplicity out of a noninjective label equals arrow multiplicity into its inverse Auslander--Reiten translate.