Finite category and algebra Auslander--Reiten surplus

The projective-generator equivalence pulls a finite algebra-module skeleton back to a duplicate-free complete skeleton of finite category modules. The generic finite-tau equivalence theorem then identifies its surplus with the literal ambient algebra surplus used by primitive directed deletion.

def MagnitudeConjecture.CoveringHom.pullbackRightModuleIndecomposableSkeleton {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (E : FiniteDimensionalModuleCategory k ≌ RightModule.FinitelyGeneratedCategory A) [E.functor.Additive] (S : RightModule.FiniteIndecomposableSkeleton k A) : FiniteDimensionalModuleIndecomposableSkeleton

Pull a duplicate-free complete algebra-module skeleton back along an additive equivalence from finite category modules.

def MagnitudeConjecture.CoveringHom.pullbackRightModuleIndecomposableSkeletonObjIso {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (E : FiniteDimensionalModuleCategory k ≌ RightModule.FinitelyGeneratedCategory A) [E.functor.Additive] (S : RightModule.FiniteIndecomposableSkeleton k A) (i : Fin S.n) : E.functor.obj ((pullbackRightModuleIndecomposableSkeleton E S).obj i) ≅ S.fgObj i

The counit matches the objects of the pulled-back category skeleton with the original finitely generated algebra-module skeleton.

theorem MagnitudeConjecture.CoveringHom.pullbackRightModuleIndecomposableSkeleton_surplus_eq_ambientARSurplus {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (E : FiniteDimensionalModuleCategory k ≌ RightModule.FinitelyGeneratedCategory A) [E.functor.Additive] [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] (S : RightModule.FiniteIndecomposableSkeleton k A) : ARCount.surplus (FiniteTauMatrix.arrowMultiplicity (pullbackRightModuleIndecomposableSkeleton E S).toFiniteRightTauCategoryData) (pullbackRightModuleIndecomposableSkeleton E S).toFiniteRightTauCategoryData.IsProjective = S.ambientARSurplus

Pullback through any additive equivalence preserves the official finite-tau surplus of a complete algebra-module skeleton.

theorem MagnitudeConjecture.CoveringHom.categorySkeleton_surplus_eq_ambientARSurplus_of_equivalence {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (E : FiniteDimensionalModuleCategory k ≌ RightModule.FinitelyGeneratedCategory A) [E.functor.Additive] [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] (T : FiniteDimensionalModuleIndecomposableSkeleton) (S : RightModule.FiniteIndecomposableSkeleton k A) : ARCount.surplus (FiniteTauMatrix.arrowMultiplicity T.toFiniteRightTauCategoryData) T.toFiniteRightTauCategoryData.IsProjective = S.ambientARSurplus

Consequently, any complete finite category-module skeleton has the ambient algebra surplus of a complete algebra-module skeleton across an additive equivalence.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.finiteCategoryAlgebraSurplusFiniteDimensional {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : FiniteDimensional k (algebra hP)

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.finiteCategoryAlgebraSurplusOppositeIsNoetherian {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : IsNoetherianRing (algebra hP)ᵐᵒᵖ

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.algebraPullbackSkeleton {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (S : RightModule.FiniteIndecomposableSkeleton k (algebra hP)) : FiniteDimensionalModuleIndecomposableSkeleton

The algebra skeleton, viewed back inside the finite category module category through the projective-generator equivalence.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.algebraPullbackSkeletonObjIso {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (S : RightModule.FiniteIndecomposableSkeleton k (algebra hP)) (i : Fin S.n) : (moduleEquivalence hP).functor.obj ((algebraPullbackSkeleton hP S).obj i) ≅ S.fgObj i

The objectwise counit matching the pulled-back category skeleton with the original finitely generated algebra-module skeleton.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.algebraPullbackSkeleton_surplus_eq_ambientARSurplus {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (S : RightModule.FiniteIndecomposableSkeleton k (algebra hP)) : ARCount.surplus (FiniteTauMatrix.arrowMultiplicity (algebraPullbackSkeleton hP S).toFiniteRightTauCategoryData) (algebraPullbackSkeleton hP S).toFiniteRightTauCategoryData.IsProjective = S.ambientARSurplus

The pulled-back category skeleton and the original algebra skeleton have the same Auslander--Reiten surplus.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.categorySkeleton_surplus_eq_ambientARSurplus {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (T : FiniteDimensionalModuleIndecomposableSkeleton) (S : RightModule.FiniteIndecomposableSkeleton k (algebra hP)) : ARCount.surplus (FiniteTauMatrix.arrowMultiplicity T.toFiniteRightTauCategoryData) T.toFiniteRightTauCategoryData.IsProjective = S.ambientARSurplus

The surplus of any complete finite indecomposable category-module skeleton is the ambient surplus of any complete algebra-module skeleton under the projective-generator equivalence.