Magnitude conjecture

MagnitudeConjecture.Algebra.RightModulePrimitiveContragredientSign

The sign of a primitive new mesh under contragredient duality #

The deleted simple for the opposite primitive idempotent is the contragredient dual of the original deleted simple. Together with reversal of the two ambient markers, this identifies positivity of the dual new mesh with vanishing of maps from the original left marker to the deleted simple. The manuscript's marker-complement theorem then turns every negative mesh into a positive dual mesh.

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredient_primitiveSinkLabel_eq_primitiveSourceLabel {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) [IsNoetherianRing Aᵐᵒᵖᵐᵒᵖ] :
S.primitiveSinkLabel D = S.contragredientSkeleton.primitiveSourceLabel ⋯

Under the label-aligned contragredient skeleton, the original primitive injective label is the primitive projective label for op e.

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveDeletedSimple_simple {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) :
CategoryTheory.Simple (S.primitiveDeletedSimple D)

The deleted simple is a simple object of the finitely generated module category.

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveDeletedSimple_op_simple {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) :
CategoryTheory.Simple (Opposite.op (S.primitiveDeletedSimple D))

The opposite of the deleted simple is simple in the opposite category.

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientPrimitiveDeletedSimple_simple {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) :
CategoryTheory.Simple ((QuotientSubmoduleEquidistribution.Contragredient.dualityEquivalence k Aᵐᵒᵖ).functor.obj (Opposite.op (S.primitiveDeletedSimple D)))

The contragredient dual of the deleted simple is a simple object.

source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientPrimitiveDeletedSimpleIso {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) :
S.contragredientSkeleton.primitiveDeletedSimple ⋯ ≅ (QuotientSubmoduleEquidistribution.Contragredient.dualityEquivalence k Aᵐᵒᵖ).functor.obj (Opposite.op (S.primitiveDeletedSimple D))

The simple top for op e is canonically isomorphic to the contragredient dual of the original deleted simple.

Instances For
    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientNewMeshEndpoint_rightMarker_eq_leftMarker {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) :
    ↑(PrimitiveNewRightMeshEndpoint.contragredientNewMeshEndpoint H he N).rightMarker = ↑(PrimitiveNewRightMeshEndpoint.leftMarker H he N)

    The right marker of the dual new mesh is the dual of the original left marker, at the same label in the aligned skeleton.

    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientNewMeshEndpoint_isPositive_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) :
    (PrimitiveNewRightMeshEndpoint.contragredientNewMeshEndpoint H he N).IsPositive ↔ ∀ (f : S.fgObj ↑(PrimitiveNewRightMeshEndpoint.leftMarker H he N) ⟶ S.primitiveDeletedSimple D), f = 0

    Positivity of the dual new mesh is exactly vanishing of all maps from the original left marker to the original deleted simple.

    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientNewMeshEndpoint_isPositive_of_not_isPositive {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) (B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D)) (N : S.PrimitiveNewRightMeshEndpoint D) (hnegative : ¬N.IsPositive) :
    (PrimitiveNewRightMeshEndpoint.contragredientNewMeshEndpoint H he N).IsPositive

    The marker-complement theorem converts a negative original mesh into a positive contragredient mesh.