Magnitude conjecture

MagnitudeConjecture.CategoryTheory.GradedSupportedCategory

The full category of graded modules supported in a finite interval #

source
def MagnitudeConjecture.Graded.FiniteGradedModule.intervalSupport {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} (m : ℕ) :
CategoryTheory.ObjectProperty ShiftedModule

The interval condition as a property of objects in the graded category.

Instances For
    source
    @[reducible, inline]
    abbrev MagnitudeConjecture.Graded.FiniteGradedModule.SupportedCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} (m : ℕ) :
    Type (u + 1)
    Instances For
      source
      theorem MagnitudeConjecture.Graded.FiniteGradedModule.supportedIn_sumObject {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} {m : ℕ} {X Y : ShiftedModule} (hX : SupportedIn m X) (hY : SupportedIn m Y) :
      SupportedIn m (sumObject X Y)

      Taking the concrete graded product preserves interval support.

      source
      def MagnitudeConjecture.Graded.FiniteGradedModule.supportedSumBicone {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} {m : ℕ} (X Y : SupportedCategory m) :
      CategoryTheory.Limits.BinaryBicone X Y

      The interval subcategory has the same concrete binary sums as the ambient category.

      Instances For
        source
        instance MagnitudeConjecture.Graded.FiniteGradedModule.instHasBinaryBiproductsSupportedCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} (m : ℕ) :
        CategoryTheory.Limits.HasBinaryBiproducts (SupportedCategory m)
        source
        instance MagnitudeConjecture.Graded.FiniteGradedModule.instHasZeroObjectSupportedCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} (m : ℕ) :
        CategoryTheory.Limits.HasZeroObject (SupportedCategory m)
        source
        instance MagnitudeConjecture.Graded.FiniteGradedModule.instHasFiniteBiproductsSupportedCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} (m : ℕ) :
        CategoryTheory.Limits.HasFiniteBiproducts (SupportedCategory m)
        source
        theorem MagnitudeConjecture.Graded.FiniteGradedModule.supported_indecomposable_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} {m : ℕ} (X : SupportedCategory m) :
        CategoryTheory.Indecomposable X ↔ CategoryTheory.Indecomposable X.obj

        Interval support cannot hide a nontrivial direct-sum decomposition.

        source
        theorem MagnitudeConjecture.Graded.FiniteGradedModule.supported_finiteDecomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} {m : ℕ} (X : SupportedCategory m) :
        Nonempty (CategoryTheory.FiniteIndecomposableDecomposition X)

        An ambient finite indecomposable decomposition stays inside the support interval.