Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleOrdinaryQuiverSpecialBiserialAssembly

Assembling a special-biserial ordinary-quiver presentation #

For an explicit system of ordinary-arrow representatives, the two continuation conditions can be checked before passing to the exact-kernel quotient: a two-arrow path survives precisely when the corresponding composite of selected-projective morphisms is nonzero. Together with the incoming and outgoing degree bounds supplied by a biserial primitive projective presentation, these concrete conditions assemble the literal special-biserial presentation used in the frozen manuscript.

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

At most one displayed arrow can follow any fixed ordinary arrow with nonzero composite of the selected representatives.

Instances For
    source
    def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.HasLeftContinuationBound {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) :
    Prop

    At most one displayed arrow can precede any fixed ordinary arrow with nonzero composite of the selected representatives.

    Instances For
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.lifted_arrowMap_comp_right_ne_zero_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) {x y : S.OrdinaryLiftedVertex} (a : x ⟶ y) (b : Quiver.Star y) :
      CategoryTheory.CategoryStruct.comp (BoundQuiver.arrowMap (S.ordinaryLiftedRelations D) b.snd) (BoundQuiver.arrowMap (S.ordinaryLiftedRelations D) a) ≠ 0 ↔ CategoryTheory.CategoryStruct.comp (D.hom b.snd) (D.hom a) ≠ 0

      A right two-arrow path in the lifted exact-kernel quotient is nonzero exactly when the corresponding representative composite is nonzero.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.lifted_arrowMap_comp_left_ne_zero_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) {x y : S.OrdinaryLiftedVertex} (a : x ⟶ y) (c : Quiver.Costar x) :
      CategoryTheory.CategoryStruct.comp (BoundQuiver.arrowMap (S.ordinaryLiftedRelations D) a) (BoundQuiver.arrowMap (S.ordinaryLiftedRelations D) c.snd) ≠ 0 ↔ CategoryTheory.CategoryStruct.comp (D.hom a) (D.hom c.snd) ≠ 0

      A left two-arrow path in the lifted exact-kernel quotient is nonzero exactly when the corresponding representative composite is nonzero.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.lifted_continuation_right_le_one {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) (hD : D.HasRightContinuationBound) {x y : S.OrdinaryLiftedVertex} (a : x ⟶ y) :
      Nat.card { b : Quiver.Star y // CategoryTheory.CategoryStruct.comp (BoundQuiver.arrowMap (S.ordinaryLiftedRelations D) b.snd) (BoundQuiver.arrowMap (S.ordinaryLiftedRelations D) a) ≠ 0 } ≤ 1

      The concrete right-continuation bound descends unchanged through the universe lift and exact-kernel quotient.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.lifted_continuation_left_le_one {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (D : OrdinaryArrowRepresentatives) (hD : D.HasLeftContinuationBound) {x y : S.OrdinaryLiftedVertex} (a : x ⟶ y) :
      Nat.card { c : Quiver.Costar x // CategoryTheory.CategoryStruct.comp (BoundQuiver.arrowMap (S.ordinaryLiftedRelations D) a) (BoundQuiver.arrowMap (S.ordinaryLiftedRelations D) c.snd) ≠ 0 } ≤ 1

      The concrete left-continuation bound descends unchanged through the universe lift and exact-kernel quotient.

      source
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.liftedSpecialBiserialPresentation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [IsNoetherianRing A] [IsAlgClosed k] (P : S.PrimitiveProjectivePresentation) (hP : P.IsBiserial) (D : OrdinaryArrowRepresentatives) (hRight : D.HasRightContinuationBound) (hLeft : D.HasLeftContinuationBound) :
      BoundQuiver.SpecialBiserialPresentation k S.basicAlgebra S.OrdinaryLiftedVertex

      Biserial primitive projectives and adapted ordinary-arrow representatives assemble the literal special-biserial presentation of the chosen basic algebra.

      Instances For