Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleOrdinaryQuiverDegree

Degrees in the ordinary projective quiver #

The total numbers of arrows starting and ending at a selected projective are the sums of the dimensions of the corresponding internal projective-radical quotients. Universe lifting the vertex set preserves both stars literally up to an explicit equivalence.

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryDegreeQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
Quiver S.ProjectiveLabel
Instances For
    source
    @[instance_reducible]
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryDegreeArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : S.ProjectiveLabel) :
    Fintype (x ⟶ y)
    Instances For
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryStar_card_eq_sum_finrank {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : S.ProjectiveLabel) :
      Nat.card (Quiver.Star x) = ∑ y : S.ProjectiveLabel, Module.finrank k (S.projectiveIrreducibleHomSpace x y)

      The number of ordinary-quiver arrows starting at x is the sum of the dimensions of the internal projective irreducible spaces with first label x.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryCostar_card_eq_sum_finrank {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : S.ProjectiveLabel) :
      Nat.card (Quiver.Costar x) = ∑ y : S.ProjectiveLabel, Module.finrank k (S.projectiveIrreducibleHomSpace y x)

      The number of ordinary-quiver arrows ending at x is the sum of the dimensions of the internal projective irreducible spaces with second label x.

      source
      def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedStarEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : S.OrdinaryLiftedVertex) :
      Quiver.Star x ≃ Quiver.Star x.down

      Forgetting the universe lift gives the same ordinary-quiver star.

      Instances For
        source
        def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedCostarEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : S.OrdinaryLiftedVertex) :
        Quiver.Costar x ≃ Quiver.Costar x.down

        Forgetting the universe lift gives the same ordinary-quiver costar.

        Instances For
          source
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedStar_card_eq_sum_finrank {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : S.OrdinaryLiftedVertex) :
          Nat.card (Quiver.Star x) = ∑ y : S.ProjectiveLabel, Module.finrank k (S.projectiveIrreducibleHomSpace x.down y)

          The lifted ordinary-quiver outgoing degree has the same dimension-sum formula as the original quiver.

          source
          theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryLiftedCostar_card_eq_sum_finrank {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : S.OrdinaryLiftedVertex) :
          Nat.card (Quiver.Costar x) = ∑ y : S.ProjectiveLabel, Module.finrank k (S.projectiveIrreducibleHomSpace y x.down)

          The lifted ordinary-quiver incoming degree has the same dimension-sum formula as the original quiver.