The nonprojective middle-term bound of a finite tau-category

For a nonprojective endpoint, betaAt counts the nonprojective indecomposable occurrences in its chosen right almost-split middle term. beta is the maximum of these counts. Both definitions retain repeated summands.

noncomputable def MagnitudeConjecture.FiniteTauMatrix.betaAt {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) : ℕ

Number of nonprojective indecomposable occurrences in the chosen right-mesh middle term ending at target.

@[reducible, inline]

abbrev MagnitudeConjecture.FiniteTauMatrix.NonprojectiveRightMiddleOccurrence {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) : Type

A nonprojective right-middle occurrence is a displayed indecomposable summand of the chosen right-mesh middle term whose label is nonprojective.

theorem MagnitudeConjecture.FiniteTauMatrix.betaAt_eq_natCard_nonprojective_of_rightMiddleDecomposition {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) {m : ℕ} (label : Fin m → Ind) (decomposition : Nonempty ((T.rightMesh (T.obj target)).X₂ ≅ ⨁ fun (i : Fin m) => T.obj (label i))) : betaAt T target = Nat.card { i : Fin m // ¬T.IsProjective (label i) }

betaAt counts the nonprojective occurrences in any displayed indecomposable decomposition of the chosen right-mesh middle term. Thus a later structural argument may use its own explicit decomposition instead of the noncomputable one used to define arrowMultiplicity.

theorem MagnitudeConjecture.FiniteTauMatrix.betaAt_eq_natCard_nonprojectiveRightMiddleOccurrence {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) : betaAt T target = Nat.card (NonprojectiveRightMiddleOccurrence T target)

betaAt is the literal cardinality of the nonprojective occurrences in the chosen right-mesh middle term. In particular, repeated isomorphic summands remain distinct occurrences.

theorem MagnitudeConjecture.FiniteTauMatrix.betaAt_le_rightMiddleArity {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) : betaAt T target ≤ rightMiddleArity T target

Discarding the projective summands of a right-mesh middle term can only decrease its number of indecomposable occurrences.

theorem MagnitudeConjecture.FiniteTauMatrix.betaAt_add_one_le_of_rightMiddleDecomposition_projective {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) {m : ℕ} (label : Fin m → Ind) (decomposition : Nonempty ((T.rightMesh (T.obj target)).X₂ ≅ ⨁ fun (i : Fin m) => T.obj (label i))) (i : Fin m) (hi : T.IsProjective (label i)) : betaAt T target + 1 ≤ m

If one displayed middle-term summand is projective, then the nonprojective occurrence count is at least one smaller than the total displayed arity.

theorem MagnitudeConjecture.FiniteTauMatrix.betaAt_add_one_le_of_minimalRightAlmostSplitDecomposition_projective {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) {E : C} {f : E ⟶ T.obj target} {m : ℕ} (label : Fin m → Ind) (decomposition : Nonempty (E ≅ ⨁ fun (i : Fin m) => T.obj (label i))) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) (hfmin : QuotientSubmoduleEquidistribution.IsRightMinimal f) (i : Fin m) (hi : T.IsProjective (label i)) : betaAt T target + 1 ≤ m

The preceding estimate may be read from any finite indecomposable decomposition of any right-minimal right almost-split map to the endpoint; uniqueness of minimal right almost-split sources identifies it with the chosen right mesh.

noncomputable def MagnitudeConjecture.FiniteTauMatrix.beta {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) : ℕ

Maximum number of nonprojective indecomposable occurrences in a chosen right almost-split middle term. Projective endpoints contribute zero.

theorem MagnitudeConjecture.FiniteTauMatrix.betaAt_eq_of_projective_iff_of_arrowMultiplicity_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.IsIdempotentComplete D] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind) (U : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D Ind) (hprojective : ∀ (i : Ind), T.IsProjective i ↔ U.IsProjective i) (harrow : ∀ (source target : Ind), arrowMultiplicity T source target = arrowMultiplicity U source target) (target : Ind) : betaAt T target = betaAt U target

theorem MagnitudeConjecture.FiniteTauMatrix.beta_eq_of_projective_iff_of_arrowMultiplicity_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.IsIdempotentComplete D] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind) (U : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData D Ind) (hprojective : ∀ (i : Ind), T.IsProjective i ↔ U.IsProjective i) (harrow : ∀ (source target : Ind), arrowMultiplicity T source target = arrowMultiplicity U source target) : beta T = beta U

theorem MagnitudeConjecture.FiniteTauMatrix.beta_le_iff {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) (bound : ℕ) : beta T ≤ bound ↔ ∀ (target : Ind), ¬T.IsProjective target → betaAt T target ≤ bound

A bound on beta is exactly a bound on the nonprojective middle occurrences at every nonprojective endpoint.

theorem MagnitudeConjecture.FiniteTauMatrix.beta_le_of_rightMiddleArity_le {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) (bound : ℕ) (h : ∀ (target : Ind), ¬T.IsProjective target → rightMiddleArity T target ≤ bound) : beta T ≤ bound

A uniform bound on the total arity of nonprojective right-mesh middle terms also bounds beta.

theorem MagnitudeConjecture.FiniteTauMatrix.beta_le_of_nonprojectiveRightMiddleOccurrence_embedding {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) (bound : ℕ) (embed : (target : Ind) → ¬T.IsProjective target → NonprojectiveRightMiddleOccurrence T target ↪ Fin bound) : beta T ≤ bound

To prove a uniform beta bound, it suffices to inject the nonprojective occurrences in every nonprojective right-mesh middle term into a fixed finite set.

theorem MagnitudeConjecture.FiniteTauMatrix.beta_le_of_rightMiddleDecomposition_nonprojective_card_le {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) (bound : ℕ) (display : ∀ (target : Ind), ¬T.IsProjective target → ∃ (m : ℕ) (label : Fin m → Ind), Nonempty ((T.rightMesh (T.obj target)).X₂ ≅ ⨁ fun (i : Fin m) => T.obj (label i)) ∧ Nat.card { i : Fin m // ¬T.IsProjective (label i) } ≤ bound) : beta T ≤ bound

A structural description may choose a convenient indecomposable decomposition separately at every nonprojective endpoint. Bounding the nonprojective occurrences in those displayed decompositions bounds beta, independently of all noncomputable decomposition choices in the finite-tau data.