Magnitude conjecture

MagnitudeConjecture.Algebra.RightModulePrimitiveQuotientFiniteSkeleton

A finite right-module skeleton of the primitive quotient #

The intrinsic primitive-quotient skeleton already uses the surviving ambient labels. Reindex it once by a finite type of the form Fin n, so it can feed the official finite-tau construction, and compare that construction directly with the intrinsic irreducible-Hom multiplicities used by directed deletion.

source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientFiniteLabelEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) :
Fin (Nat.card (S.PrimitiveQuotientLabel D)) ≃ S.PrimitiveQuotientLabel D

The single reindexing from the literal surviving-label type to the Fin n shape required by FiniteIndecomposableSkeleton.

Instances For
    source
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientFiniteIndecomposableSkeleton {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 (primitiveQuotientAlgebra e)ᵐᵒᵖ] :
    FiniteIndecomposableSkeleton k (primitiveQuotientAlgebra e)

    The complete duplicate-free primitive-quotient skeleton, retaining the literal surviving labels through primitiveQuotientFiniteLabelEquiv.

    Instances For
      source
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientFiniteFGObjIso {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 (primitiveQuotientAlgebra e)ᵐᵒᵖ] (i : Fin (S.primitiveQuotientFiniteIndecomposableSkeleton D).n) :
      (S.primitiveQuotientFiniteIndecomposableSkeleton D).fgObj i ≅ (S.primitiveQuotientAlmostSplitSkeleton D).obj ((S.primitiveQuotientFiniteLabelEquiv D) i)

      The reindexed finite skeleton has literally the same finitely generated objects as the intrinsic primitive-quotient skeleton.

      Instances For
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientFinite_arrowMultiplicity_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) [IsNoetherianRing (primitiveQuotientAlgebra e)ᵐᵒᵖ] [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (source target : Fin (S.primitiveQuotientFiniteIndecomposableSkeleton D).n) :
        FiniteTauMatrix.arrowMultiplicity (S.primitiveQuotientFiniteIndecomposableSkeleton D).finiteTauCategoryData.toFiniteRightTauCategoryData source target = S.primitiveQuotientIrreducibleArrowMultiplicity D ((S.primitiveQuotientFiniteLabelEquiv D) source) ((S.primitiveQuotientFiniteLabelEquiv D) target)

        After the single finite reindexing, the official finite-tau arrow multiplicity is exactly the intrinsic primitive-quotient Irr dimension.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientFinite_ambientARSurplus_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) [IsNoetherianRing (primitiveQuotientAlgebra e)ᵐᵒᵖ] [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) :
        (S.primitiveQuotientFiniteIndecomposableSkeleton D).ambientARSurplus = S.primitiveQuotientARSurplus D

        The official finite-tau surplus of the reindexed quotient skeleton is the literal intrinsic primitive-quotient surplus used by directed deletion.