Magnitude conjecture

MagnitudeConjecture.Algebra.StatementFiniteModules

Connecting the independent module vocabulary to the proof library #

The statement's finite family is the same data as the production skeleton. Forgetting the finite-generation bundle identifies the Hom spaces linearly, so the direct Hom matrix and its magnitude agree with those in the proof.

source
def MagnitudeConjecture.Statement.IndecomposableFamily.toSkeleton {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) :
RightModule.FiniteIndecomposableSkeleton k A

View the independently specified family as a production skeleton.

Instances For
    source
    theorem MagnitudeConjecture.Statement.IndecomposableFamily.isRepresentationFinite {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) :
    RightModule.IsRepresentationFinite k A

    Existence of the independent family gives the production finite-type hypothesis.

    source
    theorem MagnitudeConjecture.Statement.IndecomposableFamily.simpleCount_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) :
    simpleCount k A S = S.toSkeleton.simpleCount

    The direct simple count is unchanged by bundling finite generation.

    source
    theorem MagnitudeConjecture.Statement.IndecomposableFamily.homMatrix_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] :
    homMatrix k A S = FiniteTauMatrix.rationalHomDimensionMatrix S.toSkeleton.finiteTauCategoryData

    The independent Hom matrix agrees with the matrix used in the proof.

    source
    theorem MagnitudeConjecture.Statement.IndecomposableFamily.magnitude_eq {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] :
    magnitude k A S = FiniteTauMatrix.categoryMagnitude S.toSkeleton.finiteTauCategoryData

    Equality of the matrices identifies their inverse sums.

    source
    theorem MagnitudeConjecture.Statement.IndecomposableFamily.homMatrix_det_ne_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] :
    (homMatrix k A S).det ≠ 0

    The Hom matrix in the independent statement is nonsingular.

    source
    theorem MagnitudeConjecture.Statement.IndecomposableFamily.magnitude_inequality_and_equality {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] :
    ↑(simpleCount k A S) ≤ magnitude k A S ∧ (magnitude k A S = ↑(simpleCount k A S) ↔ BoundQuiver.IsSpecialBiserial k A)

    The numerical assertion, with special biseriality still expressed by the production predicate. Its independent presentation connection is separate.