Magnitude conjecture

MagnitudeConjecture.CategoryTheory.ShiftOrbitWindow

Shift-orbit functors on finite control windows #

The manuscript uses the orbit functor only on a finite full window, which is not itself invariant under deck transformations. This file restricts the source of the ambient shift-orbit functor to such a window while retaining ambient shifted Hom summands. It also connects pairwise separation for a strict object action to the exact shifted-Hom orthogonality predicate.

source
@[reducible, inline]
abbrev MagnitudeConjecture.CoveringHom.windowInclusion {C : Type u} [CategoryTheory.Category.{v, u} C] (W : Set C) :
CategoryTheory.Functor (CoveringSeparation.WindowCategory W) C

The inclusion of a full set-valued window into the ambient category.

Instances For
    source
    noncomputable def MagnitudeConjecture.CoveringHom.windowIdentityComponentFunctor {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] (W : Set C) :
    CategoryTheory.Functor (CoveringSeparation.WindowCategory W) (ShiftOrbitCategory C A)

    The ambient degree-zero orbit functor restricted to a full control window. The target remains the ambient orbit category because the window need not be shift-invariant.

    Instances For
      source
      @[reducible, inline]
      abbrev MagnitudeConjecture.CoveringHom.windowMultiplicativeShiftHom {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (W : Set C) (X Y : CoveringSeparation.WindowCategory W) (a : Multiplicative A) :
      Type v

      Ambient shifted Homs between two objects of a full window, indexed by the multiplicative wrapper of the additive shift group.

      Instances For
        source
        noncomputable def MagnitudeConjecture.CoveringHom.windowIdentityComponentFunctorOrbitHomDecomposition {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)] (W : Set C) :
        FunctorOrbitHomDecomposition (windowIdentityComponentFunctor W) (windowMultiplicativeShiftHom W)

        The restricted concrete orbit functor has the same tautological Gabriel Hom decomposition as the ambient functor.

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

          Every nonzero ambient shift Hom between objects of the chosen window vanishes.

          Instances For
            source
            theorem MagnitudeConjecture.CoveringHom.windowMultiplicativeShiftHom_translateHomOrthogonal {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] {W : Set C} (h : WindowShiftHomOrthogonal W) :
            TranslateHomOrthogonal (windowMultiplicativeShiftHom W)
            source
            theorem MagnitudeConjecture.CoveringHom.windowIdentityComponentFunctor_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)] {W : Set C} (h : WindowShiftHomOrthogonal W) :
            (windowIdentityComponentFunctor W).Full

            Shift-Hom orthogonality on a window makes the restricted concrete orbit functor full.

            source
            theorem MagnitudeConjecture.CoveringHom.windowIdentityComponentFunctor_faithful {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] (W : Set C) :
            (windowIdentityComponentFunctor W).Faithful

            The restricted concrete window orbit functor is faithful without any orthogonality hypothesis.

            source
            structure MagnitudeConjecture.CoveringHom.ShiftObjectActionCompatibility {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [MulAction (Multiplicative A) C] :
            Type (max (max u v) w)

            Compatibility between a coherent additive right shift and a strict left multiplicative action on objects. The inverse converts the two action conventions. Only the objectwise comparison is needed to transfer Hom-orthogonality; the eventual universal-cover construction must supply it from its deck functors.

            • objIso (a : A) (X : C) : (CategoryTheory.shiftFunctor C a).obj X ≅ (Multiplicative.ofAdd a)⁻¹ • X
            Instances For
              source
              theorem MagnitudeConjecture.CoveringHom.windowShiftHomOrthogonal_of_pairwise_windowSeparated {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] [MulAction (Multiplicative A) C] (D : ShiftObjectActionCompatibility) {W : Set C} (separated : ∀ {g₁ g₂ : Multiplicative A}, g₁ ≠ g₂ → ∀ {X Y : C}, X ∈ W → Y ∈ W → ¬CoveringSeparation.homInteraction (g₁ • X) (g₂ • Y)) :
              WindowShiftHomOrthogonal W

              Pairwise Hom-interaction separation of distinct translates of a window implies the exact shifted-Hom orthogonality needed by its orbit functor.