The finite right-module category as finite tau-category data

This file packages the finite Krull--Schmidt and nilpotent-radical fields of the generic FiniteRightTauCategoryData interface for the literal category of finitely generated right modules over a representation-finite finite-dimensional algebra. After this construction, the remaining inputs are exactly the chosen right and left Auslander--Reiten meshes and their translation compatibility.

structure MagnitudeConjecture.RightModule.RightTauInput {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : Type (v + 1)

The genuinely tau-theoretic inputs still needed after the finite right-module skeleton, Krull--Schmidt properties, and nilpotent categorical radical have been constructed.

• rightMesh : FinitelyGeneratedCategory A → CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)
• rightTermIso (X : FinitelyGeneratedCategory A) : (self.rightMesh X).X₃ ≅ X
• rightTau (X : FinitelyGeneratedCategory A) : QuotientSubmoduleEquidistribution.Iyama.RightTauSequence (self.rightMesh X)

structure MagnitudeConjecture.RightModule.TauInput {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : Type (v + 1)

The remaining two-sided tau-theoretic input, after the finite Krull--Schmidt module-category fields have been discharged.

• right : RightTauInput S
• leftMesh : FinitelyGeneratedCategory A → CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)
• leftTermIso (X : FinitelyGeneratedCategory A) : (self.leftMesh X).X₁ ≅ X
• leftTau (X : FinitelyGeneratedCategory A) : QuotientSubmoduleEquidistribution.Iyama.LeftTauSequence (self.leftMesh X)
• tauPlusEquiv : { X : Fin S.n // ¬CategoryTheory.Limits.IsZero (self.right.rightMesh (S.fgObj X)).X₁ } ≃ { Y : Fin S.n // ¬CategoryTheory.Limits.IsZero (self.leftMesh (S.fgObj Y)).X₃ }
• rightLeftMeshIso (X : { X : Fin S.n // ¬CategoryTheory.Limits.IsZero (self.right.rightMesh (S.fgObj X)).X₁ }) : self.right.rightMesh (S.fgObj ↑X) ≅ self.leftMesh (S.fgObj ↑(self.tauPlusEquiv X))

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.toFiniteRightTauCategoryData {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : RightTauInput S) : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData (FinitelyGeneratedCategory A) (Fin S.n)

A representation-finite finite-dimensional right-module category supplies all finite Krull--Schmidt and nilpotent-radical fields of FiniteRightTauCategoryData. The input contains only chosen right AR meshes.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.toFiniteTauCategoryData {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (D : TauInput S) : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData (FinitelyGeneratedCategory A) (Fin S.n)

A two-sided AR-mesh input completes the literal finitely generated right-module category to the generic finite tau-category interface.