Magnitude conjecture

MagnitudeConjecture.CategoryTheory.OrbitPushdownFunctor

Gabriel push-down as a functor on linear modules #

The objectwise direct-sum module constructed in OrbitPushdown is natural in the upstairs module. This file sends a module natural transformation diagonally across the translated summands, proves naturality for arbitrary orbit morphisms, and bundles the construction as an additive linear functor between linear-module categories.

source
noncomputable def MagnitudeConjecture.CoveringHom.orbitPushdownNatTransAppLinear {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] {M N : CategoryTheory.Functor C (ModuleCat k)} (α : M ⟶ N) (X : C) :
orbitPushdownValue M X →ₗ[k] orbitPushdownValue N X

A module natural transformation acts diagonally on the translated summands of push-down.

Instances For
    source
    @[simp]
    theorem MagnitudeConjecture.CoveringHom.orbitPushdownNatTransAppLinear_lof {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] {M N : CategoryTheory.Functor C (ModuleCat k)} (α : M ⟶ N) (X : C) (b : A) (x : ↑(M.obj ((CategoryTheory.shiftFunctor C b).obj X))) :
    (orbitPushdownNatTransAppLinear α X) ((orbitPushdownLof M X b) x) = (orbitPushdownLof N X b) ((CategoryTheory.ConcreteCategory.hom (α.app ((CategoryTheory.shiftFunctor C b).obj X))) x)
    source
    theorem MagnitudeConjecture.CoveringHom.orbitPushdownNatTransAppLinear_naturality_homogeneous {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] {M N : CategoryTheory.Functor C (ModuleCat k)} (α : M ⟶ N) {X Y : C} (a : A) (f : ShiftHom X Y a) :
    orbitPushdownNatTransAppLinear α Y ∘ₗ orbitPushdownHomogeneousMap M a f = orbitPushdownHomogeneousMap N a f ∘ₗ orbitPushdownNatTransAppLinear α X

    Diagonal action of a module map commutes with every homogeneous push-down morphism.

    source
    theorem MagnitudeConjecture.CoveringHom.orbitPushdownNatTransAppLinear_naturality {k : Type uK} [CommRing 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)] {M N : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] [N.Additive] [CategoryTheory.Functor.Linear k N] (α : M ⟶ N) {X Y : C} (f : ShiftOrbitHom A X Y) :
    orbitPushdownNatTransAppLinear α Y ∘ₗ (orbitPushdownMapLinear M) f = (orbitPushdownMapLinear N) f ∘ₗ orbitPushdownNatTransAppLinear α X

    Diagonal action of a module map commutes with arbitrary finite-support orbit morphisms.

    source
    noncomputable def MagnitudeConjecture.CoveringHom.orbitPushdownNatTrans {k : Type uK} [CommRing 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)] {M N : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] [N.Additive] [CategoryTheory.Functor.Linear k N] (α : M ⟶ N) :
    orbitPushdown M ⟶ orbitPushdown N

    Push-down of a natural transformation of upstairs modules.

    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.CoveringHom.orbitPushdownNatTrans_id {k : Type uK} [CommRing 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)] {M : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] :
      orbitPushdownNatTrans (CategoryTheory.CategoryStruct.id M) = CategoryTheory.CategoryStruct.id (orbitPushdown M)
      source
      @[simp]
      theorem MagnitudeConjecture.CoveringHom.orbitPushdownNatTrans_comp {k : Type uK} [CommRing 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)] {M N P : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] [N.Additive] [CategoryTheory.Functor.Linear k N] [P.Additive] [CategoryTheory.Functor.Linear k P] (α : M ⟶ N) (β : N ⟶ P) :
      orbitPushdownNatTrans (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (orbitPushdownNatTrans α) (orbitPushdownNatTrans β)
      source
      @[simp]
      theorem MagnitudeConjecture.CoveringHom.orbitPushdownNatTrans_add {k : Type uK} [CommRing 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)] {M N : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] [N.Additive] [CategoryTheory.Functor.Linear k N] (α β : M ⟶ N) :
      orbitPushdownNatTrans (α + β) = orbitPushdownNatTrans α + orbitPushdownNatTrans β
      source
      @[simp]
      theorem MagnitudeConjecture.CoveringHom.orbitPushdownNatTrans_smul {k : Type uK} [CommRing 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)] {M N : CategoryTheory.Functor C (ModuleCat k)} [M.Additive] [CategoryTheory.Functor.Linear k M] [N.Additive] [CategoryTheory.Functor.Linear k N] (r : k) (α : M ⟶ N) :
      orbitPushdownNatTrans (r • α) = r • orbitPushdownNatTrans α
      source
      noncomputable def MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdown {k : Type uK} [CommRing 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)] :
      CategoryTheory.Functor (LinearModuleCategory k) (LinearModuleCategory k)

      Gabriel push-down as a functor from linear modules upstairs to linear modules over the shift-orbit category.

      Instances For
        source
        instance MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdown_additive {k : Type uK} [CommRing 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)] :
        linearModuleOrbitPushdown.Additive
        source
        instance MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdown_linear {k : Type uK} [CommRing 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)] :
        CategoryTheory.Functor.Linear k linearModuleOrbitPushdown