Magnitude conjecture

MagnitudeConjecture.CategoryTheory.GradedHomComponents

Homogeneous components of maps #

An internal Hom grading gives finite homogeneous decompositions of every map. Taking degree zero of a composite pairs opposite degrees. This is the identity decomposition used to classify graded indecomposables as shifts.

source
noncomputable def MagnitudeConjecture.GradedCategory.HomGrading.decomposeHom {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) :
(X ⟶ Y) ≃ₗ[k] DirectSum ℤ fun (d : ℤ) => ↥(G.component X Y d)

The finite homogeneous decomposition of a map.

Instances For
    source
    noncomputable def MagnitudeConjecture.GradedCategory.HomGrading.part {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) (d : ℤ) :
    (X ⟶ Y) →ₗ[k] X ⟶ Y

    Projection onto degree d, viewed as an ambient map.

    Instances For
      source
      theorem MagnitudeConjecture.GradedCategory.HomGrading.part_mem {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} (d : ℤ) (f : X ⟶ Y) :
      (G.part X Y d) f ∈ G.component X Y d
      source
      theorem MagnitudeConjecture.GradedCategory.HomGrading.part_of_mem {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} {d : ℤ} {f : X ⟶ Y} (hf : f ∈ G.component X Y d) :
      (G.part X Y d) f = f
      source
      theorem MagnitudeConjecture.GradedCategory.HomGrading.part_of_mem_ne {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} {d e : ℤ} {f : X ⟶ Y} (hf : f ∈ G.component X Y d) (hde : d ≠ e) :
      (G.part X Y e) f = 0
      source
      theorem MagnitudeConjecture.GradedCategory.HomGrading.sum_parts {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} (f : X ⟶ Y) :
      ∑ d ∈ DFinsupp.support ((G.decomposeHom X Y) f), (G.part X Y d) f = f
      source
      theorem MagnitudeConjecture.GradedCategory.HomGrading.part_zero_comp_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 Z : C} {d : ℤ} (f : X ⟶ Y) (hf : f ∈ G.component X Y d) (g : Y ⟶ Z) :
      (G.part X Z 0) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp f ((G.part Y Z (-d)) g)

      With the first factor homogeneous of degree d, only degree -d of the second factor contributes to degree zero of their composite.

      source
      theorem MagnitudeConjecture.GradedCategory.HomGrading.part_zero_comp {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 Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
      (G.part X Z 0) (CategoryTheory.CategoryStruct.comp f g) = ∑ d ∈ DFinsupp.support ((G.decomposeHom X Y) f), CategoryTheory.CategoryStruct.comp ((G.part X Y d) f) ((G.part Y Z (-d)) g)

      Degree-zero convolution has a finite sum indexed only by the support of the first factor.

      source
      theorem MagnitudeConjecture.GradedCategory.HomGrading.part_zero_id {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 : C) :
      (G.part X X 0) (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id X

      Taking degree zero preserves the identity map.