Incoming AR multiplicity at string projectives

The projective-boundary minimal right almost-split map has source the Jacobson radical. For a string presentation that radical has one indecomposable uniserial summand for every displayed arrow ending at the vertex. Hence the incoming Auslander--Reiten arity at the corresponding projective is the literal incoming-arrow count.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientCategoryAlgebraFiniteDimensional {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) : FiniteDimensional k P.quotientCategoryAlgebra

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientCategoryAlgebraOppositeIsNoetherian {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) : IsNoetherianRing P.quotientCategoryAlgebraᵐᵒᵖ

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arCountQuotientFGHasFiniteBiproducts {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) : CategoryTheory.Limits.HasFiniteBiproducts (FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ)

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arCountQuotientFGHasBinaryBiproducts {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) : CategoryTheory.Limits.HasBinaryBiproducts (FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ)

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexModule_nontrivial {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (y : Q) : Nontrivial ↑(P.representedVertexModule y)

A represented canonical projective is nonzero, witnessed by its trivial path basis vector.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexModule_projective {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (y : Q) : CategoryTheory.Projective (P.representedVertexModule y)

A represented canonical projective is categorically projective.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexModuleEnd_isLocalRing {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (y : Q) : IsLocalRing (Module.End P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.representedVertexModule y))

The ordinary module endomorphism ring of a represented canonical projective is local.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexModule_indecomposable {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (y : Q) : CategoryTheory.Indecomposable (P.representedVertexModule y)

A represented canonical projective is indecomposable.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexRadicalInclusion {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (y : Q) : P.representedVertexRadicalFGObj y ⟶ P.representedVertexModule y

The literal inclusion of the represented projective's radical.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexRadicalInclusion_isRightAlmostSplit {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (y : Q) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (P.representedVertexRadicalInclusion y)

The radical inclusion at a represented string projective is right almost split.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexRadicalInclusion_isRightMinimal {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (y : Q) : QuotientSubmoduleEquidistribution.IsRightMinimal (P.representedVertexRadicalInclusion y)

The radical inclusion at a represented string projective is right minimal.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexSkeletonIso {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) (y : Q) : P.representedVertexModule y ≅ S.fgObj (MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexSkeletonIndex✝ P S y)

The represented canonical projective is the chosen skeleton object at its unique label.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexProjectiveLabel {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) (y : Q) : S.ProjectiveLabel

The unique indecomposable-projective label corresponding to a displayed vertex.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.eq_of_representedVertexModule_iso {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (eModule : P.representedVertexModule x ≅ P.representedVertexModule y) : x = y

An isomorphism between represented canonical projectives remembers the displayed vertex.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexProjectiveLabel_injective {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) : Function.Injective (P.representedVertexProjectiveLabel S)

Distinct displayed vertices have distinct projective labels.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexProjectiveLabel_surjective {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) : Function.Surjective (P.representedVertexProjectiveLabel S)

Every indecomposable projective label is represented by a displayed vertex.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexProjectiveEquiv {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) : Q ≃ S.ProjectiveLabel

Displayed vertices are equivalent to the projective labels of any duplicate-free module skeleton.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.rightMiddleArity_representedVertexProjectiveLabel {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) (y : Q) : FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData (P.representedVertexProjectiveLabel S y).label = Nat.card (DisplayedIncomingArrow y)

The incoming AR arity at the projective represented by y is the number of displayed quiver arrows ending at y.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.rightMiddleArity_le_two_of_projective {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) (i : Fin S.n) (hi : S.finiteTauCategoryData.IsProjective i) : FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData i ≤ 2

Incoming right-mesh arity is at most two at every projective string module as well: the radical of its represented vertex projective has one indecomposable summand for each displayed incoming arrow.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.StringPresentation.DisplayedArrow (Q : Type u) [Quiver Q] : Type u

The literal type of all displayed arrows, grouped by their target vertex.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.projectiveTargetArrowCount {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) : ℕ

The manuscript's ell: the total incoming AR-arrow multiplicity at indecomposable projective targets.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.projectiveIncomingArity_eq_projectiveTargetArrowCount {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) : FiniteTauMatrix.projectiveIncomingArity S.finiteTauCategoryData = P.projectiveTargetArrowCount S

The generic finite-tau projective incoming count is the same sum as the string-projective target count, merely indexed by the tau-projective subtype instead of structured projective labels.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.projectiveTargetArrowCount_eq_natCard_displayedArrow {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) : P.projectiveTargetArrowCount S = Nat.card (DisplayedArrow Q)

For a string presentation, the number of AR arrows ending at projective modules is the number of displayed quiver arrows.

@[instance_reducible]

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.stringTauProjectiveDecidablePred {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) : DecidablePred S.finiteTauCategoryData.IsProjective

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.surplus_eq_oneMiddleMeshCount_sub_natCard_displayedArrow {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (S : RightModule.FiniteIndecomposableSkeleton k P.quotientCategoryAlgebra) (hbound : ∀ (Y : Fin S.n), ¬S.finiteTauCategoryData.IsProjective Y → FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData Y ≤ 2) : ARCount.surplus (FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData) S.finiteTauCategoryData.IsProjective = ↑(FiniteTauMatrix.oneMiddleMeshCount S.finiteTauCategoryData) - ↑(Nat.card (DisplayedArrow Q))

Under the two-middle bound, the AR surplus of a representation-finite string presentation is E₁ - |Q₁|. This is the exact numerical reduction used in the frozen manuscript before the Butler--Ringel bijection identifies the two terms.