Magnitude conjecture

MagnitudeConjecture.CategoryTheory.FiniteDimensionalModuleDirected

Directed finite-support module categories #

The covering argument uses directedness before choosing any finite global skeleton: every intermediate object-deletion category still has a directed category of finite-support modules. This file records that literal property and proves its inheritance under extension by zero.

source
def MagnitudeConjecture.CoveringHom.FiniteModuleNonzeroNonisomorphism {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M N : FiniteDimensionalModuleCategory k) :
Prop

A nonzero nonisomorphism whose source and target are indecomposable finite-support modules.

Instances For
    source
    def MagnitudeConjecture.CoveringHom.HasAcyclicFiniteModuleNonzeroNonisomorphisms {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] :
    Prop

    The manuscript's assertion that mod C is directed, expressed without choosing a global set of indecomposable representatives.

    Instances For
      source
      theorem MagnitudeConjecture.CoveringHom.hasAcyclicFiniteModuleNonzeroNonisomorphisms_of_ranked_realization {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {E : Type uE} [CategoryTheory.Category.{vE, uE} E] [CategoryTheory.Preadditive E] (F : CategoryTheory.Functor E (FiniteDimensionalModuleCategory k)) [F.Full] [F.Faithful] (rank : E → ℤ) (hstrict : ∀ {X Y : E}, (∃ (f : X ⟶ Y), f ≠ 0 ∧ ¬CategoryTheory.IsIso f) → rank Y < rank X) (hdense : ∀ (M : FiniteDimensionalModuleCategory k), CategoryTheory.Indecomposable M → ∃ (X : E), Nonempty (F.obj X ≅ M)) :
      HasAcyclicFiniteModuleNonzeroNonisomorphisms

      A full faithful realization of all indecomposable finite modules from a category whose nonzero nonisomorphisms strictly decrease an integer rank makes the finite-module category directed.

      source
      theorem MagnitudeConjecture.CoveringHom.hasAcyclicFiniteModuleNonzeroNonisomorphisms_of_equivalence {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type u'} [CategoryTheory.Category.{v, u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor (FiniteDimensionalModuleCategory k) (FiniteDimensionalModuleCategory k)) [F.Additive] [F.IsEquivalence] (H : HasAcyclicFiniteModuleNonzeroNonisomorphisms) :
      HasAcyclicFiniteModuleNonzeroNonisomorphisms

      Directedness of finite-support module categories is invariant under an additive equivalence.

      source
      theorem MagnitudeConjecture.ObjectDeletion.hasAcyclicFiniteModuleNonzeroNonisomorphisms_deletion {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S : Set C) (H : CoveringHom.HasAcyclicFiniteModuleNonzeroNonisomorphisms) :
      CoveringHom.HasAcyclicFiniteModuleNonzeroNonisomorphisms

      Directedness of the finite-support module category is inherited by every literal object-deletion quotient.