Directedness and intrinsic surplus across an algebra-module equivalence #
theorem
MagnitudeConjecture.CoveringHom.hasAcyclicFiniteModuleNonzeroNonisomorphisms_of_ranked_algebra_family
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{C : Type}
[CategoryTheory.Category.{u, 0} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(E : FiniteDimensionalModuleCategory k ≌ RightModule.FinitelyGeneratedCategory A)
[E.functor.Additive]
{ι : Type w}
(V : ι → RightModule.FinitelyGeneratedCategory A)
(rank : ι → ℤ)
(hstrict : ∀ (a b : ι) (f : V a ⟶ V b), f ≠ 0 → ¬CategoryTheory.IsIso f → rank b < rank a)
(hcomplete :
∀ (M : RightModule.FinitelyGeneratedCategory A), CategoryTheory.Indecomposable M → ∃ (a : ι), Nonempty (M ≅ V a))
:
A complete strictly ranked algebra-module family makes the equivalent finite category-module category directed.
theorem
MagnitudeConjecture.CoveringHom.finiteCategorySurplus_eq_algebra_surplus
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{C : Type}
[CategoryTheory.Category.{u, 0} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
[Fintype C]
(E : FiniteDimensionalModuleCategory k ≌ RightModule.FinitelyGeneratedCategory A)
[E.functor.Additive]
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hrep : IsLocallyRepresentationFinite)
(S : RightModule.FiniteIndecomposableSkeleton k A)
:
finiteCategorySurplus hP hrep = S.ambientARSurplus
The intrinsic surplus agrees with that of any complete algebra skeleton.