Right tau-data on a finite-dimensional module skeleton

Minimal right almost-split maps and their kernels give the chosen right mesh at each indecomposable label. Finite componentwise biproducts extend these meshes to every object and assemble the generic finite right-tau interface.

noncomputable def MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.labelRightMesh {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) (y : Fin S.n) : CategoryTheory.ShortComplex (FiniteDimensionalModuleCategory k)

The kernel--source--endpoint complex of the chosen minimal right almost-split morphism at a skeleton label.

theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.labelRightTau {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] (y : Fin S.n) : QuotientSubmoduleEquidistribution.Iyama.RightTauSequence (S.labelRightMesh y)

Every label mesh is a right tau-sequence. At a nonprojective endpoint the terminal map is epic and its kernel inclusion is left almost split; at a projective endpoint the terminal map is monic and its kernel is zero.

theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.labelRightMesh_X₃ {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) (y : Fin S.n) : (S.labelRightMesh y).X₃ = S.obj y

The right endpoint of a label mesh is definitionally its skeleton object.

structure MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.ChosenLabelDecomposition {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) (X : FiniteDimensionalModuleCategory k) : Type (max u v)

A chosen decomposition of an arbitrary finite-dimensional module into the fixed skeleton labels.

• n : ℕ
• label : Fin self.n → Fin S.n
• iso : X ≅ ⨁ fun (i : Fin self.n) => S.obj (self.label i)

noncomputable def MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.chosenLabelDecomposition {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) (X : FiniteDimensionalModuleCategory k) : S.ChosenLabelDecomposition X

Choose one label decomposition for every finite-dimensional module.

noncomputable def MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.moduleRightMesh {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) (X : FiniteDimensionalModuleCategory k) : CategoryTheory.ShortComplex (FiniteDimensionalModuleCategory k)

Extend the labelwise right meshes to every module by finite componentwise biproduct.

noncomputable def MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.moduleRightTermIso {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) (X : FiniteDimensionalModuleCategory k) : (S.moduleRightMesh X).X₃ ≅ X

The modulewise right mesh has the supplied module as its endpoint.

theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.moduleRightTau {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] (X : FiniteDimensionalModuleCategory k) : QuotientSubmoduleEquidistribution.Iyama.RightTauSequence (S.moduleRightMesh X)

Every modulewise right mesh is a right tau-sequence.

noncomputable def MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.toFiniteRightTauCategoryData {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData (FiniteDimensionalModuleCategory k) (Fin S.n)

A finite indecomposable skeleton and enough projectives construct the complete finite right-tau-category interface.