The beta count from an arbitrary displayed minimal almost-split source #
theorem
MagnitudeConjecture.FiniteTauMatrix.betaAt_eq_natCard_of_minimalRightAlmostSplit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{Ind : Type w}
[Fintype Ind]
(T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind)
(target : Ind)
(hprojective : ∀ (j : Ind), T.IsProjective j ↔ CategoryTheory.Projective (T.obj j))
{E : C}
(f : E ⟶ T.obj target)
(hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f)
(hmin : QuotientSubmoduleEquidistribution.IsRightMinimal f)
(n : ℕ)
(V : Fin n → C)
(hV : ∀ (i : Fin n), CategoryTheory.Indecomposable (V i))
(d : E ≅ ⨁ V)
:
betaAt T target = Nat.card { i : Fin n // ¬CategoryTheory.Projective (V i) }
Any finite displayed indecomposable source of a minimal right almost-split map computes the right beta count by its actual nonprojective summands.
theorem
MagnitudeConjecture.FiniteTauMatrix.betaAt_eq_natCard_of_minimalRightAlmostSplit_fintype
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{Ind : Type w}
[Fintype Ind]
(T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind)
(target : Ind)
(hprojective : ∀ (j : Ind), T.IsProjective j ↔ CategoryTheory.Projective (T.obj j))
{E : C}
(f : E ⟶ T.obj target)
(hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f)
(hmin : QuotientSubmoduleEquidistribution.IsRightMinimal f)
{ι : Type}
[Fintype ι]
(V : ι → C)
(hV : ∀ (i : ι), CategoryTheory.Indecomposable (V i))
(d : E ≅ ⨁ V)
:
betaAt T target = Nat.card { i : ι // ¬CategoryTheory.Projective (V i) }
The same count for any small finite occurrence index type.
theorem
MagnitudeConjecture.FiniteTauMatrix.nonprojective_card_le_beta_of_equivalence
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.IsIdempotentComplete C]
{Ind : Type w}
[Fintype Ind]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasFiniteBiproducts D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
(T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind)
(E : D ≌ C)
[E.functor.Additive]
(hprojective : ∀ (j : Ind), T.IsProjective j ↔ CategoryTheory.Projective (T.obj j))
{M Y : D}
(f : M ⟶ Y)
(hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f)
(hmin : QuotientSubmoduleEquidistribution.IsRightMinimal f)
(hY : CategoryTheory.Indecomposable Y)
(hnY : ¬CategoryTheory.Projective Y)
{ι : Type}
[Fintype ι]
(V : ι → D)
(hV : ∀ (i : ι), CategoryTheory.Indecomposable (V i))
(d : M ≅ ⨁ V)
:
Nat.card { i : ι // ¬CategoryTheory.Projective (V i) } ≤ beta T
An explicit minimal almost-split source in an equivalent category bounds its number of nonprojective summands by the target algebra's beta invariant.