Deck invariance of pull-up projector diagonals

A transformation defined downstairs in the shift-orbit category has translation-conjugate diagonal blocks after pull-up to the explicit direct sum of translates. Hence invertibility of a diagonal block is invariant under left deck translation.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupNatTrans {k : Type uK} [CommRing k] {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] {N P : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} (α : N ⟶ P) : ShiftOrbitCategory.identityComponentFunctor.comp N ⟶ ShiftOrbitCategory.identityComponentFunctor.comp P

Restrict a transformation of modules on the shift-orbit category to degree-zero arrows upstairs.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupPushdownEnd {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] (α : orbitPushdown M ⟶ orbitPushdown M) : orbitPullupPushdown M ⟶ orbitPullupPushdown M

Transport the degree-zero restriction of a push-down endomorphism to the explicit direct-sum model of pull-up.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupPushdownInclusion {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] {N : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} (j : N ⟶ orbitPushdown M) : ShiftOrbitCategory.identityComponentFunctor.comp N ⟶ orbitPullupPushdown M

Pull back an inclusion into a push-down module and transport its target to the explicit direct-sum model.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupPushdownRetraction {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] {N : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} (r : orbitPushdown M ⟶ N) : orbitPullupPushdown M ⟶ ShiftOrbitCategory.identityComponentFunctor.comp N

Pull back a retraction from a push-down module and transport its source from the explicit direct-sum model.

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownInclusion_retraction {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] {N : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} (j : N ⟶ orbitPushdown M) (r : orbitPushdown M ⟶ N) (hjr : CategoryTheory.CategoryStruct.comp j r = CategoryTheory.CategoryStruct.id N) : CategoryTheory.CategoryStruct.comp (orbitPullupPushdownInclusion M j) (orbitPullupPushdownRetraction M r) = CategoryTheory.CategoryStruct.id (ShiftOrbitCategory.identityComponentFunctor.comp N)

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownInclusion_retraction_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] {N : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} (j : N ⟶ orbitPushdown M) (r : orbitPushdown M ⟶ N) (hjr : CategoryTheory.CategoryStruct.comp j r = CategoryTheory.CategoryStruct.id N) {Z : CategoryTheory.Functor C (ModuleCat k)} (h : ShiftOrbitCategory.identityComponentFunctor.comp N ⟶ Z) : CategoryTheory.CategoryStruct.comp (orbitPullupPushdownInclusion M j) (CategoryTheory.CategoryStruct.comp (orbitPullupPushdownRetraction M r) h) = h

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownRetraction_inclusion {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] {N : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} (j : N ⟶ orbitPushdown M) (r : orbitPushdown M ⟶ N) : CategoryTheory.CategoryStruct.comp (orbitPullupPushdownRetraction M r) (orbitPullupPushdownInclusion M j) = orbitPullupPushdownEnd M (CategoryTheory.CategoryStruct.comp r j)

The projector of a pulled-back retract is the transported pull-up of its downstairs projector.

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownEnd_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 : CategoryTheory.Functor C (ModuleCat k)) [M.Additive] [CategoryTheory.Functor.Linear k M] (α β : orbitPushdown M ⟶ orbitPushdown M) : orbitPullupPushdownEnd M (α + β) = orbitPullupPushdownEnd M α + orbitPullupPushdownEnd M β

@[simp]

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownEnd_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] : orbitPullupPushdownEnd M (CategoryTheory.CategoryStruct.id (orbitPushdown M)) = CategoryTheory.CategoryStruct.id (orbitPullupPushdown M)

theorem MagnitudeConjecture.CoveringHom.isIso_of_orbitPullupNatTrans_isIso {k : Type uK} [CommRing k] {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] {N P : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} (α : N ⟶ P) [CategoryTheory.IsIso (orbitPullupNatTrans α)] : CategoryTheory.IsIso α

Restriction along the degree-zero orbit functor reflects isomorphisms, because it is the identity on objects.

theorem MagnitudeConjecture.CoveringHom.isIso_of_orbitPullupPushdownInclusion_isIso {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] {N : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} (j : N ⟶ orbitPushdown M) [CategoryTheory.IsIso (orbitPullupPushdownInclusion M j)] : CategoryTheory.IsIso j

An isomorphism after pulled-back inclusion was transported to the explicit sum already came from an isomorphism downstairs.

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

The b-th diagonal block of a pulled-back push-down endomorphism.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPushdownShiftSummandHom {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)) (a b : A) (X : C) : (orbitPullupPushdownTranslate M b).obj ((CategoryTheory.shiftFunctor C a).obj X) ⟶ (orbitPullupPushdownTranslate M (a + b)).obj X

The homogeneous orbit isomorphism from X⟦a⟧ to X carries the b-summand to the (a+b)-summand.

instance MagnitudeConjecture.CoveringHom.orbitPushdownShiftSummandHom_isIso {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)) (a b : A) (X : C) : CategoryTheory.IsIso (orbitPushdownShiftSummandHom M a b X)

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslateLof_shiftOrbitFromShift {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] (a b : A) (X : C) : CategoryTheory.CategoryStruct.comp ((orbitPullupPushdownTranslateLof M b).app ((CategoryTheory.shiftFunctor C a).obj X)) ((orbitPushdown M).map (shiftOrbitFromShift X a)) = CategoryTheory.CategoryStruct.comp (orbitPushdownShiftSummandHom M a b X) ((orbitPullupPushdownTranslateLof M (a + b)).app X)

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslateLof_shiftOrbitFromShift_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] (a b : A) (X : C) {Z : ModuleCat k} (h : (orbitPushdown M).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((orbitPullupPushdownTranslateLof M b).app ((CategoryTheory.shiftFunctor C a).obj X)) (CategoryTheory.CategoryStruct.comp ((orbitPushdown M).map (shiftOrbitFromShift X a)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (orbitPushdownShiftSummandHom M a b X) ((orbitPullupPushdownTranslateLof M (a + b)).app X)) h

theorem MagnitudeConjecture.CoveringHom.shiftOrbitFromShift_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] (a b : A) (X : C) : CategoryTheory.CategoryStruct.comp ((orbitPushdown M).map (shiftOrbitFromShift X a)) ((orbitPullupPushdownTranslateComponent M (a + b)).app X) = CategoryTheory.CategoryStruct.comp ((orbitPullupPushdownTranslateComponent M b).app ((CategoryTheory.shiftFunctor C a).obj X)) (orbitPushdownShiftSummandHom M a b X)

theorem MagnitudeConjecture.CoveringHom.shiftOrbitFromShift_orbitPullupPushdownTranslateComponent_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] (a b : A) (X : C) {Z : ModuleCat k} (h : M.obj ((CategoryTheory.shiftFunctor C (a + b)).obj X) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((orbitPushdown M).map (shiftOrbitFromShift X a)) (CategoryTheory.CategoryStruct.comp ((orbitPullupPushdownTranslateComponent M (a + b)).app X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((orbitPullupPushdownTranslateComponent M b).app ((CategoryTheory.shiftFunctor C a).obj X)) (orbitPushdownShiftSummandHom M a b X)) h

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownDiagonal_shift {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] (α : orbitPushdown M ⟶ orbitPushdown M) (a b : A) (X : C) : CategoryTheory.CategoryStruct.comp (orbitPushdownShiftSummandHom M a b X) ((orbitPullupPushdownDiagonal M α (a + b)).app X) = CategoryTheory.CategoryStruct.comp ((orbitPullupPushdownDiagonal M α b).app ((CategoryTheory.shiftFunctor C a).obj X)) (orbitPushdownShiftSummandHom M a b X)

Naturality downstairs conjugates the b-diagonal block at X⟦a⟧ to the (a+b)-diagonal block at X.

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownDiagonal_isIso_add_left {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] (α : orbitPushdown M ⟶ orbitPushdown M) (a b : A) (hb : CategoryTheory.IsIso (orbitPullupPushdownDiagonal M α b)) : CategoryTheory.IsIso (orbitPullupPushdownDiagonal M α (a + b))

Invertibility of a pulled-back diagonal block propagates under left deck translation.

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownDiagonal_isIso_iff_add_left {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] (α : orbitPushdown M ⟶ orbitPushdown M) (a b : A) : CategoryTheory.IsIso (orbitPullupPushdownDiagonal M α b) ↔ CategoryTheory.IsIso (orbitPullupPushdownDiagonal M α (a + b))

The unit-diagonal predicate of every downstairs endomorphism is invariant under left deck translation after pull-up.

theorem MagnitudeConjecture.CoveringHom.orbitPushdown_one_retract_inclusion_isIso {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] {L Q : CategoryTheory.Functor (ShiftOrbitCategory C A) (ModuleCat k)} (j : L ⟶ orbitPushdown M) (r : orbitPushdown M ⟶ L) (hjr : CategoryTheory.CategoryStruct.comp j r = CategoryTheory.CategoryStruct.id L) (j' : Q ⟶ orbitPushdown M) (r' : orbitPushdown M ⟶ Q) (hj'r' : CategoryTheory.CategoryStruct.comp j' r' = CategoryTheory.CategoryStruct.id Q) (htotal : CategoryTheory.CategoryStruct.comp r j + CategoryTheory.CategoryStruct.comp r' j' = CategoryTheory.CategoryStruct.id (orbitPushdown M)) (hindecomp : ∀ (b : A), CategoryTheory.Indecomposable (orbitPullupPushdownTranslate M b)) (hlocal : ∀ (b : A), IsLocalRing (CategoryTheory.End (orbitPullupPushdownTranslate M b))) (hpair : ∀ (b c : A), b ≠ c → ¬Nonempty (orbitPullupPushdownTranslate M b ≅ orbitPullupPushdownTranslate M c)) : CategoryTheory.IsIso j ∨ CategoryTheory.IsIso j'

Complementary retracts of a push-down module pull back to complementary retracts of the translate sum. Hence, under the Krull--Schmidt hypotheses on the translates, one of the original downstairs inclusions is an isomorphism. This is the invariant-summand core of Gabriel's indecomposability argument.