Magnitude conjecture

MagnitudeConjecture.Algebra.BiserialProjectivePresentation

Biserial primitive-projective presentations #

A finite-dimensional algebra is biserial when the principal right and left ideals belonging to a complete family of primitive orthogonal idempotents are biserial modules. This file records that condition on the literal primitive-projective presentations used by the support-quotient construction.

source
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.IsBiserial {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) :
Prop

A complete primitive-projective presentation is biserial when every associated principal right ideal eA and principal left ideal Ae is a biserial object.

Instances For
    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.IsBiserial.rightIdeal_top_jacobson_length_le_two {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {P : S.PrimitiveProjectivePresentation} (hP : P.IsBiserial) (p : S.ProjectiveLabel) :
    Module.length Aᵐᵒᵖ (↥(Module.jacobson Aᵐᵒᵖ ↑(rightIdealFGObj (P.idempotent p))) ⧸ Module.jacobson Aᵐᵒᵖ ↥(Module.jacobson Aᵐᵒᵖ ↑(rightIdealFGObj (P.idempotent p)))) ≤ 2

    Biseriality of a primitive-projective presentation bounds the first radical layer of every associated principal right ideal by two.

    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.IsBiserial.leftIdeal_top_jacobson_length_le_two {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {P : S.PrimitiveProjectivePresentation} (hP : P.IsBiserial) (p : S.ProjectiveLabel) :
    Module.length A (↥(Module.jacobson A ↑(leftIdealFGObj (P.idempotent p))) ⧸ Module.jacobson A ↥(Module.jacobson A ↑(leftIdealFGObj (P.idempotent p)))) ≤ 2

    Biseriality of a primitive-projective presentation bounds the first radical layer of every associated principal left ideal by two.