Left tau-sequences for the finite right-module category

At a noninjective selected module, the chosen minimal left almost-split monomorphism and its cokernel form the left Auslander--Reiten complex. At an injective selected module, the chosen minimal left almost-split map is epic, so its cokernel is zero. Finite componentwise biproducts extend these meshes to every finitely generated right module.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightKernelMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : S.fgObj ↑(S.rightTranslation z) ⟶ (S.minimalRightAlmostSplitAt ↑z).middle

The chosen kernel inclusion rewritten with its selected translation representative as source.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightKernelMap_leftAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit (S.rightKernelMap z)

The transported kernel inclusion is left almost split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightKernelMap_leftMinimal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : QuotientSubmoduleEquidistribution.IsLeftMinimal (S.rightKernelMap z)

The transported kernel inclusion is left minimal.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.noninjectiveLeftSourceIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : { x : Fin S.n // ¬CategoryTheory.Injective (S.fgObj x) }) : S.fgObj ↑x ≅ S.fgObj ↑(S.rightTranslation (S.rightTranslationEquiv.symm x))

Identify a noninjective label with the source of the corresponding chosen right Auslander--Reiten sequence.

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

Rotate the corresponding chosen right Auslander--Reiten complex at a noninjective selected module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.noninjectiveLeftTau {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : { x : Fin S.n // ¬CategoryTheory.Injective (S.fgObj x) }) : QuotientSubmoduleEquidistribution.Iyama.LeftTauSequence (S.noninjectiveLeftMesh x)

The noninjective left Auslander--Reiten complex is a left tau-sequence.

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

The chosen left almost-split map and its canonical cokernel at an injective selected module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.injectiveLeftTau {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : { x : Fin S.n // CategoryTheory.Injective (S.fgObj x) }) : QuotientSubmoduleEquidistribution.Iyama.LeftTauSequence (S.injectiveLeftMesh x)

The injective-boundary left complex is a left tau-sequence.

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

The unified left mesh at a selected indecomposable label.

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

Every selected-label left mesh is a left tau-sequence.

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

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

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

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

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

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

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

Every modulewise left mesh is a left tau-sequence.