Magnitude conjecture

MagnitudeConjecture.CategoryTheory.DeckShiftAction

Coherent shifts from a left deck action #

Mathlib's HasShift is a coherent right action by endofunctors. The manuscript writes its deck group as a left action. This file records the exact conversion convention: additive degree g is the deck transformation g⁻¹. It packages the coherent functor data as a ShiftMkCore, constructs the actual HasShift instance, and supplies the object-action comparison used by control-window separation.

source
structure MagnitudeConjecture.CoveringHom.CoherentDeckShift (C : Type u) [CategoryTheory.Category.{v, u} C] (G : Type w) [Group G] [MulAction G C] :
Type (max (max u v) w)

Coherent inverse deck-translation functors in Mathlib's right-action orientation. The functor at additive degree g acts on objects as the inverse of the manuscript's left deck transformation g.

  • core : CategoryTheory.ShiftMkCore C (Additive G)
  • objIso (g : G) (X : C) : (self.core.F (Additive.ofMul g)).obj X ≅ g⁻¹ • X
Instances For
    source
    @[implicit_reducible]
    def MagnitudeConjecture.CoveringHom.CoherentDeckShift.hasShift {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) :
    CategoryTheory.HasShift C (Additive G)

    The actual Mathlib shift instance constructed from coherent deck translation functors.

    Instances For
      source
      def MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftObjectActionCompatibility {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) :
      ShiftObjectActionCompatibility

      The constructed shift functors agree objectwise with inverse left deck translations.

      Instances For
        source
        theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.windowShiftHomOrthogonal_of_pairwise_windowSeparated {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (D : CoherentDeckShift C G) {W : Set C} (separated : ∀ {g₁ g₂ : G}, g₁ ≠ g₂ → ∀ {X Y : C}, X ∈ W → Y ∈ W → ¬CoveringSeparation.homInteraction (g₁ • X) (g₂ • Y)) :
        WindowShiftHomOrthogonal W

        Pairwise separation of distinct left deck translates gives shifted-Hom orthogonality for the coherent deck shift on the selected window.

        source
        theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.additiveShift {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.Preadditive C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] (a : Additive G) :
        (CategoryTheory.shiftFunctor C a).Additive
        source
        theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearShift {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] {k : Type uK} [CommSemiring k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (a : Additive G) :
        CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)
        source
        theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.windowIdentityComponentFunctor_full_of_pairwise_windowSeparated {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] {k : Type uK} [CommSemiring k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] {W : Set C} (separated : ∀ {g₁ g₂ : G}, g₁ ≠ g₂ → ∀ {X Y : C}, X ∈ W → Y ∈ W → ¬CoveringSeparation.homInteraction (g₁ • X) (g₂ • Y)) :
        (windowIdentityComponentFunctor W).Full

        A separated window for coherent deck shifts has a full canonical functor to the concrete shift-orbit category.