Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardGradedDegreeBounds

Uniform degree bounds and strict descent between graded representatives #

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rdGradedDegreeBoundsQuiver {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.rdGradedDegreeBoundsArrowFintype {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_uniform_bound {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      ∃ (h : ℕ), 1 ≤ h ∧ ∀ (X Y : S.StandardFormMeshCategory) (d : ℤ), d < 0 ∨ ↑h < d → S.standardFormIntegerHomGrading.component X Y d = ⊥

      One positive finite bound controls all nonzero homogeneous mesh maps.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_zero_of_ne {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) (h : X ≠ Y) :
      S.standardFormIntegerHomGrading.component X Y 0 = ⊥

      Distinct vertices have no degree-zero maps.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGraded_strict_descent {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) (s t : ℤ) (f : { obj := S.standardFormGradedVertexFunctor.obj X, degree := s } ⟶ { obj := S.standardFormGradedVertexFunctor.obj Y, degree := t }) (hf : f ≠ 0) (hXY : X ≠ Y ∨ s ≠ t) :
      t < s

      A nonzero map between distinct shifted representatives strictly decreases shift.