Magnitude conjecture

MagnitudeConjecture.CategoryTheory.FiniteCategoryAlgebraBridge

The finite linear category--algebra bridge #

For a finite linear category, pointwise local representation-finiteness is global. Combining the resulting finite indecomposable skeleton with the projective-generator equivalence identifies the finite category algebra as representation-finite and transfers the manuscript's directedness condition to any duplicate-free algebra-module skeleton.

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

Transport a duplicate-free finite skeleton of category modules forward along an additive equivalence to finitely generated right modules.

Instances For
    source
    def MagnitudeConjecture.CoveringHom.pushforwardRightModuleIndecomposableSkeletonObjIso {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (E : FiniteDimensionalModuleCategory k ≌ RightModule.FinitelyGeneratedCategory A) [E.functor.Additive] (S : FiniteDimensionalModuleIndecomposableSkeleton) (i : Fin S.n) :
    (pushforwardRightModuleIndecomposableSkeleton E S).fgObj i ≅ E.functor.obj (S.obj i)

    The pushed-forward skeleton object, rebundled as finitely generated, is canonically the image of the original category-module skeleton object.

    Instances For
      source
      noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryModuleIndecomposableSkeleton {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hrep : IsLocallyRepresentationFinite) :
      FiniteDimensionalModuleIndecomposableSkeleton

      On a finite base category, the finitely many local fibers assemble into a complete finite indecomposable module skeleton.

      Instances For
        source
        theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.algebra_isRepresentationFinite {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hrep : IsLocallyRepresentationFinite) :
        RightModule.IsRepresentationFinite k (algebra hP)

        A finite locally representation-finite linear category has a representation-finite category algebra.

        source
        theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.algebraSkeleton_hasAcyclicNonzeroNonisomorphisms {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (H : HasAcyclicFiniteModuleNonzeroNonisomorphisms) (S : RightModule.FiniteIndecomposableSkeleton k (algebra hP)) :
        S.HasAcyclicNonzeroNonisomorphisms

        Directedness of the finite module category transfers through the category-algebra equivalence to every chosen algebra-module skeleton.