Auslander--Reiten translation under contragredient duality

The label-aligned contragredient skeleton turns a noninjective right A-module into a nonprojective right Aᵐᵒᵖ-module at the same label. Uniqueness of minimal left almost-split maps then identifies target Auslander--Reiten translation with inverse source translation, which is the translation identity used by the manuscript's negative new-mesh construction.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientNonprojectiveLabel {k A : Type u} [Field 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) }) : { i : Fin S.contragredientSkeleton.n // ¬CategoryTheory.Projective (S.contragredientSkeleton.fgObj i) }

A noninjective original label, dualized at the same finite coordinate, is nonprojective in the contragredient skeleton.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientRightTranslationLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (q : { i : Fin S.contragredientSkeleton.n // ¬CategoryTheory.Projective (S.contragredientSkeleton.fgObj i) }) : Fin S.contragredientSkeleton.n

Target Auslander--Reiten translation with the automatically derived Noetherian instance for the opposite-opposite algebra kept internal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredient_rightTranslationLabel_eq_inverse {k A : Type u} [Field 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) }) : S.contragredientRightTranslationLabel (S.contragredientNonprojectiveLabel x) = ↑(S.rightTranslationEquiv.symm x)

Under the label-aligned contragredient skeleton, target Auslander--Reiten translation is inverse source translation: τ_(Aᵐᵒᵖ)(D X) = D(τ_A⁻¹ X) at the level of selected labels.