Magnitude conjecture

MagnitudeConjecture.CategoryTheory.GradedMatrixBicone

Homogeneous direct-sum coordinates for finite matrix objects #

source
noncomputable def MagnitudeConjecture.GradedCategory.HomGrading.matrixBicone {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] (M : CategoryTheory.Mat_ C) :
CategoryTheory.Limits.Bicone fun (i : M.ι) => (CategoryTheory.Mat_.embedding C).obj (M.X i)

The matrix object with its singleton summand injections and projections.

Instances For
    source
    theorem MagnitudeConjecture.GradedCategory.HomGrading.matrixBicone_total {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] (M : CategoryTheory.Mat_ C) :
    ∑ i : M.ι, CategoryTheory.CategoryStruct.comp ((matrixBicone M).π i) ((matrixBicone M).ι i) = CategoryTheory.CategoryStruct.id M
    source
    theorem MagnitudeConjecture.GradedCategory.HomGrading.matrixBicone_π_homogeneous {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] (M : CategoryTheory.Mat_ C) (i : M.ι) :
    (matrixBicone M).π i ∈ G.additiveEnvelope.component M ((CategoryTheory.Mat_.embedding C).obj (M.X i)) 0

    The singleton projections have degree zero.

    source
    theorem MagnitudeConjecture.GradedCategory.HomGrading.matrixBicone_ι_homogeneous {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] (M : CategoryTheory.Mat_ C) (i : M.ι) :
    (matrixBicone M).ι i ∈ G.additiveEnvelope.component ((CategoryTheory.Mat_.embedding C).obj (M.X i)) M 0

    The singleton injections have degree zero.