Finite-type almost-split data for right modules

This file connects the magnitude campaign's categorical finite indecomposable skeleton with the donor's module-theoretic finite-type almost-split existence theorem. The two notions of indecomposability are bridged through the local endomorphism ring, and no classification of modules is used.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgEndModuleEndRingEquiv {A : Type v} [Ring A] (M : FinitelyGeneratedCategory A) : CategoryTheory.End M ≃+* Module.End Aᵐᵒᵖ ↑M

The categorical endomorphism ring of an FG module agrees with its usual module endomorphism ring.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgModule_isFiniteLength {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (M : FinitelyGeneratedCategory A) : IsFiniteLength Aᵐᵒᵖ ↑M

Every finitely generated right module over a finite-dimensional algebra has finite length over the opposite algebra.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgModule_isIndecomposableModule_iff_indecomposable {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (M : FinitelyGeneratedCategory A) : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Aᵐᵒᵖ ↑M ↔ CategoryTheory.Indecomposable M

For finitely generated modules over a finite-dimensional algebra, the module-theoretic indecomposability used by the almost-split construction is equivalent to categorical indecomposability.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgObj_isIndecomposableModule {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Aᵐᵒᵖ ↑(S.fgObj i)

Each chosen categorical indecomposable is indecomposable in the donor's module-theoretic sense.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.almostSplitSkeleton {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : QuotientSubmoduleEquidistribution.IndecomposableSkeleton Aᵐᵒᵖ (Fin S.n)

The chosen finite right-module skeleton, expressed in the exact interface consumed by the finite-type almost-split construction.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.minimalRightAlmostSplitAt {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : S.almostSplitSkeleton.MinimalRightAlmostSplitDecomposition i

A chosen minimal right almost-split decomposition at every selected indecomposable right module.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.minimalLeftAlmostSplitAt {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : S.almostSplitSkeleton.MinimalLeftAlmostSplitDecomposition i

A chosen minimal left almost-split decomposition at every selected indecomposable right module.