Magnitude conjecture

MagnitudeConjecture.CategoryTheory.GradedModuleHomCategory

The Hom grading on actual finite-dimensional graded modules #

Objects carry a grading, while the ambient morphisms are all module maps. The degree category therefore supplies the homogeneous morphisms required by the graded identity-splitting argument.

source
structure MagnitudeConjecture.Graded.FiniteGradedModule {k A : Type u} [Field k] [Ring A] [Algebra k A] (R : VectorGrading k A) :
Type (max u (v + 1))

A finite-dimensional graded module, with its full ungraded Hom space.

Instances For
    source
    @[instance_reducible]
    instance MagnitudeConjecture.Graded.FiniteGradedModule.instCategory {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} :
    CategoryTheory.Category.{v, max u (v + 1)} (FiniteGradedModule R)
    source
    @[instance_reducible]
    instance MagnitudeConjecture.Graded.FiniteGradedModule.instPreadditive {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} :
    CategoryTheory.Preadditive (FiniteGradedModule R)
    source
    @[instance_reducible]
    instance MagnitudeConjecture.Graded.FiniteGradedModule.instModuleHom {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} (X Y : FiniteGradedModule R) :
    Module k (X ⟶ Y)
    source
    @[instance_reducible]
    instance MagnitudeConjecture.Graded.FiniteGradedModule.instLinear {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} :
    CategoryTheory.Linear k (FiniteGradedModule R)
    source
    def MagnitudeConjecture.Graded.FiniteGradedModule.homGrading {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} :
    GradedCategory.HomGrading k (FiniteGradedModule R)

    Homogeneous components of actual module maps, with internal decomposition.

    Instances For