Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardIncomingCount

Nonprojective incoming occurrences in the standard-form quiver #

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.incomingCountQuiver {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.incomingCountArrowFintype {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.instEnoughProjectivesFGModuleCatMulOpposite {A : Type u} [Ring A] :
      CategoryTheory.EnoughProjectives (FGModuleCat Aᵐᵒᵖ)
      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIncoming_nonprojective_card_eq_betaAt {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) :
      Nat.card { a : MeshCategory.RightMeshData.IncomingArrow z // ¬CategoryTheory.Projective (S.fgObj a.fst) } = FiniteTauMatrix.betaAt S.finiteTauCategoryData.toFiniteRightTauCategoryData z

      Incoming arrow occurrences with nonprojective source are exactly those counted by the original right beta invariant, with all multiplicities retained.