Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardSupportedDirected

Directedness inside the supported graded category #

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.supportedDirectedQuiver {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.supportedDirectedArrowFintype {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.standardFormSupported_noniso_descent {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {m : ℕ} (a b : S.standardFormSupportedLabel m) (f : S.standardFormSupportedFamily m a ⟶ S.standardFormSupportedFamily m b) (hf : f ≠ 0) (hi : ¬CategoryTheory.IsIso f) :
      ↑b.snd < ↑a.snd

      Nonzero noninvertible maps in the supported family strictly lower shift.

      source
      def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupportedEdge {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (a b : S.standardFormSupportedLabel m) :
      Prop

      Edges between supported indecomposable representatives.

      Instances For
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupported_acyclic {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (a : S.standardFormSupportedLabel m) :
        ¬Relation.TransGen (S.standardFormSupportedEdge m) a a

        No cycle of nonzero nonisomorphisms occurs in the complete supported family.