Magnitude conjecture

MagnitudeConjecture.CategoryTheory.ShiftOrbitDecomposition

The tautological Hom decomposition of the shift-orbit category #

The abstract Gabriel Hom interface is indexed by a multiplicative group, whereas Mathlib's shift action is indexed by an additive group. This file reindexes the shift-orbit Hom direct sum along Multiplicative.ofAdd and packages the result as the exact FunctorOrbitHomDecomposition used by the local full-faithfulness theorems.

source
@[reducible, inline]
abbrev MagnitudeConjecture.CoveringHom.multiplicativeShiftHom {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (X Y : C) (a : Multiplicative A) :
Type v

Shifted Hom indexed multiplicatively, solely to match the covering-Hom interface's group convention.

Instances For
    source
    noncomputable def MagnitudeConjecture.CoveringHom.shiftHomZeroLinearEquiv {k : Type uK} [CommSemiring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (X Y : C) :
    (X ⟶ Y) ≃ₗ[k] ShiftHom X Y 0

    Degree-zero shifted Hom is linearly equivalent to ordinary Hom.

    Instances For
      source
      theorem MagnitudeConjecture.CoveringHom.shiftHomZeroLinearEquiv_nonempty {k : Type uK} [CommSemiring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (X Y : C) :
      Nonempty ((X ⟶ Y) ≃ₗ[k] ShiftHom X Y 0)

      Proof-irrelevant packaging of the degree-zero shifted-Hom coordinate, useful when specializing the equivalence at very large functor objects.

      source
      noncomputable def MagnitudeConjecture.CoveringHom.multiplicativeShiftHomDirectSumEquiv {k : Type uK} [CommSemiring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (X Y : C) :
      ShiftOrbitHom A X Y ≃ₗ[k] DirectSum (Multiplicative A) (multiplicativeShiftHom X Y)

      Reindex the additive shift degrees by their multiplicative wrapper.

      Instances For
        source
        noncomputable def MagnitudeConjecture.CoveringHom.identityComponentOrbitHomDecomposition {k : Type uK} [CommSemiring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] (X Y : C) :
        OrbitHomDecomposition (ShiftOrbitCategory.identityComponentFunctor.obj X ⟶ ShiftOrbitCategory.identityComponentFunctor.obj Y)

        The target Hom of the canonical orbit functor is tautologically the direct sum of all multiplicatively indexed shifted Hom spaces.

        Instances For
          source
          noncomputable def MagnitudeConjecture.CoveringHom.identityComponentFunctorOrbitHomDecomposition {k : Type uK} [CommSemiring k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [∀ (a : A), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] :
          FunctorOrbitHomDecomposition ShiftOrbitCategory.identityComponentFunctor multiplicativeShiftHom

          The concrete shift-orbit functor satisfies the exact functor-level Gabriel Hom decomposition interface.

          Instances For
            source
            def MagnitudeConjecture.CoveringHom.ShiftHomOrthogonal {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] :
            Prop

            Every nonzero additive shift Hom vanishes.

            Instances For
              source
              theorem MagnitudeConjecture.CoveringHom.multiplicativeShiftHom_translateHomOrthogonal {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (h : ShiftHomOrthogonal) :
              TranslateHomOrthogonal multiplicativeShiftHom

              Additive shift orthogonality is exactly the multiplicatively indexed orthogonality consumed by the generic covering-Hom interface.

              source
              theorem MagnitudeConjecture.CoveringHom.identityComponentFunctor_fullOfShiftHomOrthogonal {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] (k : Type uK) [CommSemiring k] [CategoryTheory.Linear k C] [∀ (a : A), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (h : ShiftHomOrthogonal) :
              ShiftOrbitCategory.identityComponentFunctor.Full

              Shift orthogonality makes the concrete degree-zero orbit functor full.