Magnitude conjecture

MagnitudeConjecture.CategoryTheory.GradedUnderlyingFG

Finitely generated underlying modules of finite graded modules #

source
def MagnitudeConjecture.Graded.FiniteGradedModule.underlyingFG {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} :
CategoryTheory.Functor (FiniteGradedModule R) (FGModuleCat A)

Forget the grading into the finitely generated module category.

Instances For
    source
    instance MagnitudeConjecture.Graded.FiniteGradedModule.instFullFGModuleCatUnderlyingFG {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} :
    underlyingFG.Full
    source
    instance MagnitudeConjecture.Graded.FiniteGradedModule.instFaithfulFGModuleCatUnderlyingFG {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} :
    underlyingFG.Faithful
    source
    instance MagnitudeConjecture.Graded.FiniteGradedModule.instAdditiveFGModuleCatUnderlyingFG {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} :
    underlyingFG.Additive
    source
    theorem MagnitudeConjecture.Graded.FiniteGradedModule.rightAlmostSplit_of_underlyingFG {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} {X Y : ShiftedModule} (f : X ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (underlyingFG.map ↑f)) :
    QuotientSubmoduleEquidistribution.IsRightAlmostSplit f

    The graded transfer only needs almost-splitness among finitely generated modules, which is the scope of the standard-form construction.

    source
    theorem MagnitudeConjecture.Graded.FiniteGradedModule.rightMinimal_of_underlyingFG {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} {X Y : ShiftedModule} (f : X ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsRightMinimal (underlyingFG.map ↑f)) :
    QuotientSubmoduleEquidistribution.IsRightMinimal f
    source
    theorem MagnitudeConjecture.Graded.FiniteGradedModule.supported_rightAlmostSplit_of_underlyingFG {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} {m : ℕ} {X Y : SupportedCategory m} (f : X ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (underlyingFG.map ↑f.hom)) :
    QuotientSubmoduleEquidistribution.IsRightAlmostSplit f

    A finite-module almost-split map restricts to any interval containing its terms.

    source
    theorem MagnitudeConjecture.Graded.FiniteGradedModule.supported_rightMinimal_of_underlyingFG {k A : Type u} [Field k] [Ring A] [Algebra k A] {R : VectorGrading k A} {m : ℕ} {X Y : SupportedCategory m} (f : X ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsRightMinimal (underlyingFG.map ↑f.hom)) :
    QuotientSubmoduleEquidistribution.IsRightMinimal f