Magnitude conjecture

MagnitudeConjecture.CategoryTheory.ShiftOrbitObjectIso

Shifted objects are isomorphic in the shift-orbit category #

The orbit category identifies every object with each of its shifts. This file constructs the identification explicitly from Mathlib's shift equivalence and verifies both inverse laws against finite-support convolution.

source
noncomputable def MagnitudeConjecture.CoveringHom.shiftOrbitToShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (X : C) (a : A) :
ShiftOrbitHom A X ((CategoryTheory.shiftFunctor C a).obj X)

The homogeneous orbit morphism from an object to its degree-a shift. Its orbit degree is -a.

Instances For
    source
    noncomputable def MagnitudeConjecture.CoveringHom.shiftOrbitFromShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (X : C) (a : A) :
    ShiftOrbitHom A ((CategoryTheory.shiftFunctor C a).obj X) X

    The homogeneous orbit morphism from a degree-a shift back to the unshifted object. Its orbit degree is a.

    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.CoveringHom.shiftOrbitToShift_comp_shiftOrbitFromShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] (X : C) (a : A) :
      (shiftOrbitCompHom (shiftOrbitToShift X a)) (shiftOrbitFromShift X a) = shiftOrbitId X
      source
      @[simp]
      theorem MagnitudeConjecture.CoveringHom.shiftOrbitFromShift_comp_shiftOrbitToShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] (X : C) (a : A) :
      (shiftOrbitCompHom (shiftOrbitFromShift X a)) (shiftOrbitToShift X a) = shiftOrbitId ((CategoryTheory.shiftFunctor C a).obj X)
      source
      noncomputable def MagnitudeConjecture.CoveringHom.ShiftOrbitCategory.objectShiftIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] (X : C) (a : A) :
      (have this := X; this) ≅ have this := (CategoryTheory.shiftFunctor C a).obj X; this

      Every object is canonically isomorphic in the orbit category to each of its shifts.

      Instances For