Incoming multiplicity from minimal right almost-split maps

The total incoming-arrow multiplicity at an indecomposable endpoint is the number of indecomposable occurrences in the source of a minimal right almost-split map. Uniqueness of minimal right almost-split maps and finite Krull--Schmidt cancellation make this number independent of the chosen map and decomposition.

structure MagnitudeConjecture.CategoryTheory.RightAlmostSplitDecompositionBound {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] (Y : C) (bound : ℕ) : Type (max u v)

A minimal right almost-split map together with an explicit finite indecomposable decomposition of its source and a bound on the number of displayed summands.

• source : C
• map : self.source ⟶ Y
• decomposition : FiniteIndecomposableDecomposition self.source
• rightAlmostSplit : QuotientSubmoduleEquidistribution.IsRightAlmostSplit self.map
• rightMinimal : QuotientSubmoduleEquidistribution.IsRightMinimal self.map
• arity_le : self.decomposition.n ≤ bound

def MagnitudeConjecture.CategoryTheory.RightAlmostSplitDecompositionBound.mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {Y : C} {m n : ℕ} (w : RightAlmostSplitDecompositionBound Y m) (h : m ≤ n) : RightAlmostSplitDecompositionBound Y n

Enlarge the numerical bound without changing the displayed minimal right almost-split map.

def MagnitudeConjecture.CategoryTheory.RightAlmostSplitDecompositionBound.postcompIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {Y Z : C} {bound : ℕ} (w : RightAlmostSplitDecompositionBound Y bound) (e : Y ≅ Z) : RightAlmostSplitDecompositionBound Z bound

Transport a bounded right almost-split witness across an isomorphism of its endpoint.

def MagnitudeConjecture.CategoryTheory.ShortComplex.ShortExact.rightAlmostSplitDecompositionBound {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasBinaryBiproducts D] {S : CategoryTheory.ShortComplex D} (hS : S.ShortExact) [IsLocalRing (CategoryTheory.End S.X₁)] {bound : ℕ} (d : FiniteIndecomposableDecomposition S.X₂) (hAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit S.g) (hn : d.n ≤ bound) : RightAlmostSplitDecompositionBound S.X₃ bound

A short exact sequence whose kernel has local endomorphism ring produces a bounded minimal right almost-split witness as soon as its terminal map is right almost split and its displayed middle decomposition has the required size.

theorem MagnitudeConjecture.CategoryTheory.nonempty_leftTermIso_of_shortExact_minimalRightAlmostSplit {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] {S T : CategoryTheory.ShortComplex D} (hS : S.ShortExact) (hT : T.ShortExact) (hSAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit S.g) (hSmin : QuotientSubmoduleEquidistribution.IsRightMinimal S.g) (hTAS : QuotientSubmoduleEquidistribution.IsRightAlmostSplit T.g) (hTmin : QuotientSubmoduleEquidistribution.IsRightMinimal T.g) (e₃ : S.X₃ ≅ T.X₃) : Nonempty (S.X₁ ≅ T.X₁)

Two short exact realizations of minimal right almost-split maps with isomorphic endpoints have isomorphic left terms. This is the kernel-level form of uniqueness of minimal right almost-split maps.

theorem MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.n_eq_of_minimalRightAlmostSplit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {E E' Y : C} {f : E ⟶ Y} {g : E' ⟶ Y} (d : FiniteIndecomposableDecomposition E) (d' : FiniteIndecomposableDecomposition E') (hlocal : ∀ (i : Fin d.n), IsLocalRing (CategoryTheory.End (d.summand i))) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) (hfmin : QuotientSubmoduleEquidistribution.IsRightMinimal f) (hg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit g) (hgmin : QuotientSubmoduleEquidistribution.IsRightMinimal g) : d.n = d'.n

The sources of two minimal right almost-split maps to the same endpoint have finite indecomposable decompositions of the same size.

theorem MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.n_eq_of_map_minimalRightAlmostSplit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.IsIdempotentComplete D] (F : CategoryTheory.Functor C D) [F.Additive] {E Y : C} {f : E ⟶ Y} (d : FiniteIndecomposableDecomposition E) (hIndec : ∀ (i : Fin d.n), CategoryTheory.Indecomposable (F.obj (d.summand i))) (hlocal : ∀ (i : Fin d.n), IsLocalRing (CategoryTheory.End (F.obj (d.summand i)))) {E' : D} {g : E' ⟶ F.obj Y} (d' : FiniteIndecomposableDecomposition E') (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (F.map f)) (hfmin : QuotientSubmoduleEquidistribution.IsRightMinimal (F.map f)) (hg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit g) (hgmin : QuotientSubmoduleEquidistribution.IsRightMinimal g) : d.n = d'.n

If an additive functor preserves the displayed indecomposable summands and carries a minimal right almost-split map to a minimal right almost-split map, then the displayed source has the same number of occurrences as any minimal right almost-split source at the image endpoint.

theorem MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.n_le_of_mapOp_cokernel_bound {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.IsIdempotentComplete D] (E : Cᵒᵖ ≌ D) [E.functor.Additive] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Epi f] (d : FiniteIndecomposableDecomposition X) (hYindec : CategoryTheory.Indecomposable (E.functor.obj (Opposite.op Y))) (hYlocal : IsLocalRing (CategoryTheory.End (E.functor.obj (Opposite.op Y)))) (hIndec : ∀ (i : Fin d.n), CategoryTheory.Indecomposable (E.functor.obj (Opposite.op (d.summand i)))) (hlocal : ∀ (i : Fin d.n), IsLocalRing (CategoryTheory.End (E.functor.obj (Opposite.op (d.summand i))))) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) (hfmin : QuotientSubmoduleEquidistribution.IsRightMinimal f) {bound : ℕ} (hbound : ∀ (Z : D), CategoryTheory.Indecomposable Z → ¬CategoryTheory.Projective Z → Nonempty (RightAlmostSplitDecompositionBound Z bound)) : d.n ≤ bound

If the cokernel of the anti-equivalent image of a minimal right almost-split map has a bounded minimal right almost-split source, then the original displayed source has the same bound. This is the categorical rotation used to transfer a right-mesh arity estimate through coefficient duality.