Primitive relative multiplicities under contragredient duality #
Dualizing the minimal left almost-split map of an original primitive new mesh gives a minimal right almost-split map in the opposite primitive quotient. Uniqueness identifies its middle with the middle of the constructed opposite new mesh. Thus relative arrow multiplicities reverse at the same literal labels, just as ambient arrow multiplicities do.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.contragredient_relativeArrowMultiplicity_eq
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
[IsAlgClosed k]
[IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ]
(H : S.HasAcyclicNonzeroNonisomorphisms)
(he : IsIdempotentElem e)
(N : S.PrimitiveNewRightMeshEndpoint D)
(y : S.PrimitiveQuotientLabel D)
:
have Nop := contragredientNewMeshEndpoint H he N;
have yop := ⟨↑y, ⋯⟩;
relativeArrowMultiplicity yop Nop = relativeArrowMultiplicity y N
The relative middle multiplicity of Y → N agrees with the relative
middle multiplicity of the reversed dual arrow DN → DY.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.contragredient_relative_gt_ambient_iff
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
[IsAlgClosed k]
[IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ]
(H : S.HasAcyclicNonzeroNonisomorphisms)
(he : IsIdempotentElem e)
(N : S.PrimitiveNewRightMeshEndpoint D)
(y : S.PrimitiveQuotientLabel D)
:
have Nop := contragredientNewMeshEndpoint H he N;
have yop := ⟨↑y, ⋯⟩;
relativeArrowMultiplicity yop Nop > FiniteTauMatrix.arrowMultiplicity S.contragredientSkeleton.finiteTauCategoryData.toFiniteRightTauCategoryData ↑yop
↑Nop.label ↔ relativeArrowMultiplicity y N > FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData ↑(sourceLabel H he N) ↑y
Strict gain in the dual relative right mesh is exactly strict gain for the reversed original pair. This is the numerical core of the manuscript's negative gaining-pair construction.