Magnitude conjecture

MagnitudeConjecture.Algebra.RightModulePrimitiveContragredientBoundary

Primitive boundary data under contragredient duality #

The primitive multiplicity at a label is unchanged after passing to the label-aligned contragredient skeleton. Projective and injective boundary bounds exchange, while the translation-difference bound is invariant under reversing the difference and replacing right translation by inverse right translation. Consequently the boundary package on the opposite side is constructed from the original coordinate estimate rather than supplied as an independent hypothesis.

source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredientHomLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i j : Fin S.n) :
(S.fgObj i ⟶ S.fgObj j) ≃ₗ[k] S.contragredientSkeleton.fgObj j ⟶ S.contragredientSkeleton.fgObj i

Contragredient duality reverses Hom spaces between aligned skeleton objects.

Instances For
    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.contragredient_primitiveMultiplicity_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) (x : Fin S.n) :
    S.contragredientSkeleton.primitiveMultiplicity ⋯ x = S.primitiveMultiplicity D x

    Primitive multiplicity is unchanged at the same literal finite label under contragredient duality.

    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.MultiplicityCoordinateEstimate.contragredient {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) (E : S.MultiplicityCoordinateEstimate (S.primitiveMultiplicityInput D)) :
    S.contragredientSkeleton.MultiplicityCoordinateEstimate (S.contragredientSkeleton.primitiveMultiplicityInput ⋯)

    The original coordinate estimate canonically supplies its opposite-side counterpart.

    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.contragredient {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) (H : S.HasAcyclicNonzeroNonisomorphisms) (E : S.MultiplicityCoordinateEstimate (S.primitiveMultiplicityInput D)) :
    S.contragredientSkeleton.PrimitiveDirectedBoundaryData (S.contragredientSkeleton.primitiveMultiplicityInput ⋯)

    Directed primitive boundary data on the contragredient side is derived from the original directedness and coordinate estimate.