Magnitude conjecture

MagnitudeConjecture.CategoryTheory.GradedModuleBiproducts

Binary biproducts of shifted graded modules #

source
@[reducible, inline]
abbrev MagnitudeConjecture.Graded.FiniteGradedModule.ShiftedModule {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} :
Type (max u (v + 1))
Instances For
    source
    def MagnitudeConjecture.Graded.FiniteGradedModule.sumObject {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} (X Y : ShiftedModule) :
    ShiftedModule

    Realize both degree labels in the grading of the ordinary module product.

    Instances For
      source
      def MagnitudeConjecture.Graded.FiniteGradedModule.sumBicone {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} (X Y : ShiftedModule) :
      CategoryTheory.Limits.BinaryBicone X Y
      Instances For
        source
        instance MagnitudeConjecture.Graded.FiniteGradedModule.instHasBinaryBiproductsShiftedModule {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} :
        CategoryTheory.Limits.HasBinaryBiproducts ShiftedModule