Right tau-sequences for the literal right-module category

At a nonprojective indecomposable, the chosen minimal right almost-split map and its kernel form the usual Auslander--Reiten complex. At a projective indecomposable, the boundary complex is 0 ⟶ rad P ⟶ P. Finite componentwise biproducts extend these label meshes to every finitely generated right module.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.nonprojectiveRightMesh {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) : CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)

The kernel--middle--endpoint complex at a nonprojective chosen indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.nonprojectiveRightTau {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) : QuotientSubmoduleEquidistribution.Iyama.RightTauSequence (S.nonprojectiveRightMesh x)

The nonprojective Auslander--Reiten complex is a right tau-sequence.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveRightMesh {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (_hp : CategoryTheory.Projective (S.fgObj p)) : CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)

The projective boundary complex 0 ⟶ rad P ⟶ P.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveRightTau {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) : QuotientSubmoduleEquidistribution.Iyama.RightTauSequence (S.projectiveRightMesh p hp)

The projective boundary complex is a right tau-sequence.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.labelRightMesh {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)

The unified right mesh at a chosen indecomposable label.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.labelRightTau {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : QuotientSubmoduleEquidistribution.Iyama.RightTauSequence (S.labelRightMesh x)

Every chosen-label right mesh is a right tau-sequence.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.labelRightMesh_X₃ {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : (S.labelRightMesh x).X₃ = S.fgObj x

The right endpoint of the unified label mesh is literally the selected indecomposable.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ChosenLabelDecomposition {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : Type v

A chosen decomposition of an arbitrary FG module into the fixed indecomposable labels.

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

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.chosenLabelDecomposition {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : S.ChosenLabelDecomposition X

Choose one finite label decomposition for every FG module.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.moduleRightMesh {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : CategoryTheory.ShortComplex (FinitelyGeneratedCategory A)

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

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.moduleRightTermIso {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : (S.moduleRightMesh X).X₃ ≅ X

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

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.moduleRightTau {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : QuotientSubmoduleEquidistribution.Iyama.RightTauSequence (S.moduleRightMesh X)

Every modulewise right mesh is a right tau-sequence.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightTauInput {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : RightTauInput S

Finite representation type constructs all right-mesh input required by the generic finite right tau-category interface.