Magnitude conjecture

MagnitudeConjecture.CategoryTheory.FiniteSkeletonDensityInvariance

Local-density invariance between finite indecomposable skeletons #

Two complete duplicate-free skeletons of the same finite-dimensional module category have equivalent label types. Isomorphic represented modules have the same projective status and the same number of indecomposable occurrences in a minimal right almost-split source, so their right-tau local densities agree. Consequently the total local density is independent of the chosen skeleton.

source
noncomputable def MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.relabel {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : FiniteDimensionalModuleIndecomposableSkeleton) (i : Fin S.n) :
Fin T.n

The label of T representing the object at a label of S.

Instances For
    source
    noncomputable def MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.relabelIso {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : FiniteDimensionalModuleIndecomposableSkeleton) (i : Fin S.n) :
    S.obj i ≅ T.obj (S.relabel T i)

    The chosen object isomorphism underlying relabelling between complete duplicate-free indecomposable skeletons.

    Instances For
      source
      theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.relabel_injective {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : FiniteDimensionalModuleIndecomposableSkeleton) :
      Function.Injective (S.relabel T)
      source
      theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.relabel_surjective {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : FiniteDimensionalModuleIndecomposableSkeleton) :
      Function.Surjective (S.relabel T)
      source
      noncomputable def MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.relabelEquiv {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : FiniteDimensionalModuleIndecomposableSkeleton) :
      Fin S.n ≃ Fin T.n

      Any two complete duplicate-free indecomposable skeletons of the same finite-dimensional module category have canonically chosen equivalent label types.

      Instances For
        source
        @[simp]
        theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.relabelEquiv_apply {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : FiniteDimensionalModuleIndecomposableSkeleton) (i : Fin S.n) :
        (S.relabelEquiv T) i = S.relabel T i
        source
        theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightMiddleArity_eq_of_obj_iso {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] (i : Fin S.n) (j : Fin T.n) (e : S.obj i ≅ T.obj j) :
        FiniteTauMatrix.rightMiddleArity S.toFiniteRightTauCategoryData i = FiniteTauMatrix.rightMiddleArity T.toFiniteRightTauCategoryData j

        Isomorphic represented indecomposables have the same incoming right-mesh arity in any two complete skeletons.

        source
        theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.isProjective_iff_of_obj_iso {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] (i : Fin S.n) (j : Fin T.n) (e : S.obj i ≅ T.obj j) :
        S.toFiniteRightTauCategoryData.IsProjective i ↔ T.toFiniteRightTauCategoryData.IsProjective j

        Isomorphic represented indecomposables have matching projectivity predicates in any two complete skeletons.

        source
        theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.rightTauLocalDensity_eq_of_obj_iso {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] (i : Fin S.n) (j : Fin T.n) (e : S.obj i ≅ T.obj j) :
        S.rightTauLocalDensity i = T.rightTauLocalDensity j

        Isomorphic represented indecomposables have the same right-tau local density in any two complete skeletons.

        source
        theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.sum_rightTauLocalDensity_eq {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (S T : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] :
        ∑ i : Fin S.n, S.rightTauLocalDensity i = ∑ j : Fin T.n, T.rightTauLocalDensity j

        The total right-tau local density is independent of the chosen complete duplicate-free indecomposable skeleton.