Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardGradedDegreeOne

Nonzero degree-one maps are irreducible in the full graded category #

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rdGradedDegreeOneQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
Quiver (Fin S.n)
Instances For
    source
    @[instance_reducible]
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rdGradedDegreeOneArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) :
    Fintype (x ⟶ y)
    Instances For
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_degreeOne_irreducible {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X Y : S.StandardFormMeshCategory) (t : ℤ) (f : { obj := S.standardFormGradedVertexFunctor.obj X, degree := t + 1 } ⟶ { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t }) (hf : f ≠ 0) :
      QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f

      Adjacent shifts leave no room for two noninvertible factors through an indecomposable.