Indecomposability of orbit push-down

The invariant-summand argument implies that an orbit push-down is indecomposable when the upstairs module has local endomorphism ring and trivial translate stabilizer. Localness passes to every translate by precomposition with the shift autoequivalences, while trivial stabilizer makes the translates pairwise nonisomorphic.

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslate_pairwise_noniso_of_trivial_stabilizer {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)) (htrivial : ∀ (a : A), Nonempty (M ≅ (CategoryTheory.shiftFunctor C a).comp M) → a = 0) (b c : A) (hbc : b ≠ c) : ¬Nonempty (orbitPullupPushdownTranslate M b ≅ orbitPullupPushdownTranslate M c)

Trivial translate stabilizer makes the full family of translates pairwise nonisomorphic.

noncomputable def MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslateEndRingEquiv {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.End M ≃+* CategoryTheory.End (orbitPullupPushdownTranslate M b)

Precomposition by a deck shift identifies the endomorphism rings of a module and its translate.

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslate_end_isLocalRing {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)) (hlocal : IsLocalRing (CategoryTheory.End M)) (b : A) : IsLocalRing (CategoryTheory.End (orbitPullupPushdownTranslate M b))

A local endomorphism ring passes from a module to every translate.

theorem MagnitudeConjecture.CoveringHom.orbitPullupPushdownTranslate_indecomposable_of_local_end {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)) (hlocal : IsLocalRing (CategoryTheory.End M)) (b : A) : CategoryTheory.Indecomposable (orbitPullupPushdownTranslate M b)

Every translate of a module with local endomorphism ring is indecomposable.

theorem MagnitudeConjecture.CoveringHom.orbitPushdown_indecomposable {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] (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.Indecomposable (orbitPushdown M)

If the translates form a pairwise nonisomorphic Krull--Schmidt family, the orbit push-down of M is indecomposable.

theorem MagnitudeConjecture.CoveringHom.orbitPushdown_indecomposable_of_local_end_of_trivial_stabilizer {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] (hlocal : IsLocalRing (CategoryTheory.End M)) (htrivial : ∀ (a : A), Nonempty (M ≅ (CategoryTheory.shiftFunctor C a).comp M) → a = 0) : CategoryTheory.Indecomposable (orbitPushdown M)

Gabriel's invariant-summand conclusion: a module with local endomorphism ring and trivial translate stabilizer has indecomposable orbit push-down.