Primitive quotient and new meshes under contragredient duality

Contragredient duality restricts to an anti-equivalence between the literal primitive-quotient subcategories on A and Aᵐᵒᵖ. It therefore converts the noninjective source of a primitive new mesh into a nonprojective opposite endpoint. Together with translation reversal, this constructs the dual new mesh used in the manuscript's negative case.

theorem MagnitudeConjecture.RightModule.primitiveQuotientProperty_inverseImage_contragredient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) : (PrimitiveQuotientProperty (MulOpposite.op e)).inverseImage (QuotientSubmoduleEquidistribution.Contragredient.dualityEquivalence k Aᵐᵒᵖ).functor = (PrimitiveQuotientProperty e).op

The inverse image of opposite primitive annihilation under contragredient duality is original primitive annihilation.

noncomputable def MagnitudeConjecture.RightModule.primitiveQuotientContragredientEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (e : A) : (PrimitiveQuotientSubcategory e)ᵒᵖ ≌ PrimitiveQuotientSubcategory (MulOpposite.op e)

Contragredient duality restricted to the literal primitive-quotient subcategories.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientPrimitiveQuotientLabelEquiv {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) : S.PrimitiveQuotientLabel D ≃ S.contragredientSkeleton.PrimitiveQuotientLabel ⋯

Primitive-quotient labels are literally preserved by the label-aligned contragredient skeleton. The equivalence changes only the proof that the common finite coordinate survives primitive deletion.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientPrimitiveQuotientLabelObj {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) (x : S.PrimitiveQuotientLabel D) : PrimitiveQuotientSubcategory (MulOpposite.op e)

A quotient label in the original skeleton, dualized at the same finite coordinate and bundled in the opposite primitive-quotient subcategory.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientPrimitiveQuotientLabelObjIso {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) (x : S.PrimitiveQuotientLabel D) : (primitiveQuotientContragredientEquivalence e).functor.obj (Opposite.op (S.primitiveQuotientLabelObj D x)) ≅ S.contragredientPrimitiveQuotientLabelObj D x

The restricted contragredient equivalence sends a quotient label object to the same label in the opposite quotient skeleton.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.sourceLabel_not_injective_primitiveQuotient {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] (H : S.HasAcyclicNonzeroNonisomorphisms) (he : IsIdempotentElem e) (N : S.PrimitiveNewRightMeshEndpoint D) : ¬CategoryTheory.Injective (S.primitiveQuotientLabelObj D (sourceLabel H he N))

The source of a primitive new mesh is noninjective in the literal primitive-quotient subcategory, not only in the ambient category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.contragredient_sourceLabel_quotient_nonprojective {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] (H : S.HasAcyclicNonzeroNonisomorphisms) (he : IsIdempotentElem e) (N : S.PrimitiveNewRightMeshEndpoint D) : ¬CategoryTheory.Projective (S.contragredientPrimitiveQuotientLabelObj D (sourceLabel H he N))

The dual of a new-mesh source is nonprojective in the literal opposite primitive quotient.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNewRightMeshEndpoint.contragredientNewMeshEndpoint {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] (H : S.HasAcyclicNonzeroNonisomorphisms) (he : IsIdempotentElem e) (N : S.PrimitiveNewRightMeshEndpoint D) : S.contragredientSkeleton.PrimitiveNewRightMeshEndpoint ⋯

Dualizing a primitive new mesh produces the opposite primitive new-mesh endpoint labelled by the original source.