The additive Auslander equivalence of the literal factor category

The biproduct of the surviving indecomposable representatives is a finite additive generator of the literal factor category. Applying the generic additive-generator equivalence therefore identifies that factor category with the finitely generated projective modules over its Auslander algebra.

This is the finite algebraic ambient category in which the manuscript's smaller, boundary-projective restricted Yoneda realization will be analyzed.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorAuslanderEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (K : Set (Fin S.n)) : S.FactorCategory K ≌ (CategoryTheory.finiteProjectiveModules (CategoryTheory.End (S.factorAdditiveGenerator K))ᵐᵒᵖ).FullSubcategory

The literal factor category is the category of finitely generated projective modules over the opposite endomorphism ring of its surviving additive generator.