Pull-up of Gabriel push-down as a sum of translates

The pull-up of an orbit push-down is the coproduct of all translated copies of the original module. This is the displayed decomposition used at the start of Gabriel's Lemma 3.5.

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslate {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (M : CategoryTheory.Functor C (ModuleCat k)) (b : A) : CategoryTheory.Functor C (ModuleCat k)

The translate indexed by b in the pull-up of an orbit push-down.

theorem MagnitudeConjecture.CoveringHom.orbitPushdownArrow_zero_of_hasShift {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] {X Y : C} (h : X ⟶ Y) (b : A) : orbitPushdownArrow' ⋯ (shiftHomZero h) = (CategoryTheory.shiftFunctor C b).map h

A degree-zero orbit arrow acts diagonally on every translated summand.

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslate_lof_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 : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] {X Y : C} (h : X ⟶ Y) (b : A) : (orbitPushdownMapLinear M) ((shiftOrbitOf X Y 0) (shiftHomZero h)) ∘ₗ orbitPushdownLof M X b = orbitPushdownLof M Y b ∘ₗ ModuleCat.Hom.hom (M.map ((CategoryTheory.shiftFunctor C b).map h))

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupPushdown {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] : CategoryTheory.Functor C (ModuleCat k)

Restrict orbit push-down to degree-zero arrows, presented with its objectwise direct sums definitionally visible.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupPushdownIso {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] : orbitPullupPushdown M ≅ ShiftOrbitCategory.identityComponentFunctor.comp (orbitPushdown M)

The explicit degree-zero restriction is the underlying functor of pull-up applied to push-down.

instance MagnitudeConjecture.CoveringHom.orbitPullupPushdown_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)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] : (orbitPullupPushdown M).Additive

instance MagnitudeConjecture.CoveringHom.orbitPullupPushdown_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)] (M : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] : CategoryTheory.Functor.Linear k (orbitPullupPushdown M)

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslateLof {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] (b : A) : orbitPullupPushdownTranslate M b ⟶ orbitPullupPushdown M

Inclusion of one translate into the pull-up of the push-down.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslateComponent {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] (b : A) : orbitPullupPushdown M ⟶ orbitPullupPushdownTranslate M b

Projection from the pull-up direct sum to one translated summand.

@[simp]

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslateLof_component_self {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] (b : A) : CategoryTheory.CategoryStruct.comp (orbitPullupPushdownTranslateLof M b) (orbitPullupPushdownTranslateComponent M b) = CategoryTheory.CategoryStruct.id (orbitPullupPushdownTranslate M b)

@[simp]

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslateLof_component_self_assoc {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] (b : A) {Z : CategoryTheory.Functor C (ModuleCat k)} (h : orbitPullupPushdownTranslate M b ⟶ Z) : CategoryTheory.CategoryStruct.comp (orbitPullupPushdownTranslateLof M b) (CategoryTheory.CategoryStruct.comp (orbitPullupPushdownTranslateComponent M b) h) = h

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslateLof_component_ne {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] {b c : A} (hbc : b ≠ c) : CategoryTheory.CategoryStruct.comp (orbitPullupPushdownTranslateLof M b) (orbitPullupPushdownTranslateComponent M c) = 0

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslateLof_component_ne_assoc {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] {b c : A} (hbc : b ≠ c) {Z : CategoryTheory.Functor C (ModuleCat k)} (h : orbitPullupPushdownTranslate M c ⟶ Z) : CategoryTheory.CategoryStruct.comp (orbitPullupPushdownTranslateLof M b) (CategoryTheory.CategoryStruct.comp (orbitPullupPushdownTranslateComponent M c) h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslateCofan {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] : CategoryTheory.Limits.Cofan fun (b : A) => orbitPullupPushdownTranslate M b

The canonical cocone of all translates into the pull-up of the push-down.

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslateCofanAppHom {k : Type uK} [CommRing k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] (M : CategoryTheory.Functor C (ModuleCat k)) (t : CategoryTheory.Limits.Cofan fun (b : A) => orbitPullupPushdownTranslate M b) (X : C) (b : A) : ↑(M.obj ((CategoryTheory.shiftFunctor C b).obj X)) →ₗ[k] ↑(t.pt.obj X)

A leg of a translate cocone at one object, with its source written in the literal family used by orbitPushdownValue.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslateDesc {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] (t : CategoryTheory.Limits.Cofan fun (b : A) => orbitPullupPushdownTranslate M b) : (orbitPullupPushdownTranslateCofan M).pt ⟶ t.pt

A family of maps out of all translates extends uniquely over the pull-up of the push-down.

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslateLof_desc {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] (t : CategoryTheory.Limits.Cofan fun (b : A) => orbitPullupPushdownTranslate M b) (b : A) : CategoryTheory.CategoryStruct.comp (orbitPullupPushdownTranslateLof M b) (orbitPullupPushdownTranslateDesc M t) = t.inj b

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslateLof_desc_assoc {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] (t : CategoryTheory.Limits.Cofan fun (b : A) => orbitPullupPushdownTranslate M b) (b : A) {Z : CategoryTheory.Functor C (ModuleCat k)} (h : t.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (orbitPullupPushdownTranslateLof M b) (CategoryTheory.CategoryStruct.comp (orbitPullupPushdownTranslateDesc M t) h) = CategoryTheory.CategoryStruct.comp (t.inj b) h

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslateCofanIsColimit {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] : CategoryTheory.Limits.IsColimit (orbitPullupPushdownTranslateCofan M)

The canonical translate cocone is a categorical coproduct.

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringHom.linearOrbitPullupPushdownTranslate {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₀ : LinearModuleCategory k) (b : A) : LinearModuleCategory k

The translated summand, bundled again as a linear module.

noncomputable def MagnitudeConjecture.CoveringHom.linearOrbitPullupPushdownTranslateCofan {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₀ : LinearModuleCategory k) : CategoryTheory.Limits.Cofan fun (b : A) => linearOrbitPullupPushdownTranslate M₀ b

The translate cocone in the full category of linear modules.

noncomputable def MagnitudeConjecture.CoveringHom.linearOrbitPullupPushdownTranslateCofanUnderlying {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₀ : LinearModuleCategory k) (t : CategoryTheory.Limits.Cofan fun (b : A) => linearOrbitPullupPushdownTranslate M₀ b) : CategoryTheory.Limits.Cofan fun (b : A) => orbitPullupPushdownTranslate M₀.obj b

Forget the linear-module bundling from a translate cocone.

noncomputable def MagnitudeConjecture.CoveringHom.linearOrbitPullupPushdownTranslateCofanIsColimit {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₀ : LinearModuleCategory k) : CategoryTheory.Limits.IsColimit (linearOrbitPullupPushdownTranslateCofan M₀)

The pull-up of push-down is also the coproduct of the translates inside the full category of linear modules.