Indecomposability under finite skeletal orbit push-down

This file packages the generic orbit push-down indecomposability theorem for the literal finite-dimensional module categories and chosen deck-orbit skeleton used by the covering argument. The finite-dimensional module's local endomorphism ring is transported to its underlying raw functor, while its categorical trivial stabilizer is converted to the corresponding raw precomposition statement. Indecomposability then passes through restriction to the orbit skeleton and the two full-subcategory wrappers.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleEndUnderlyingRingEquiv {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) : CategoryTheory.End M ≃+* CategoryTheory.End M.obj.obj

The two fully faithful full-subcategory inclusions identify the endomorphism ring of a finite-dimensional module with that of its underlying raw functor.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModule_underlying_end_isLocalRing {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) : IsLocalRing (CategoryTheory.End M.obj.obj)

Localness of the finite-dimensional categorical endomorphism ring passes to the underlying raw functor.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModule_trivial_raw_translate_stabilizer {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] [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)] (M : FiniteDimensionalModuleCategory k) : (∀ (a : Additive G), Nonempty (M ≅ (CategoryTheory.shiftFunctor (FiniteDimensionalModuleCategory k) a).obj M) → a = 0) → ∀ (a : Additive G), Nonempty (M.obj.obj ≅ (CategoryTheory.shiftFunctor C a).comp M.obj.obj) → a = 0

A trivial stabilizer in the finite-dimensional module category gives the raw precomposition form required by generic orbit push-down. Module shift degree -a has underlying functor shiftFunctor C a ⋙ M.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_indecomposable_of_trivial_stabilizer {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] [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)] [IsCancelSMul G C] (M : FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) : (∀ (a : Additive G), Nonempty (M ≅ (CategoryTheory.shiftFunctor (FiniteDimensionalModuleCategory k) a).obj M) → a = 0) → CategoryTheory.Indecomposable (D.finiteDimensionalModuleOrbitSkeletonPushdown.obj M)

Manuscript-facing Gabriel 3.5: an indecomposable finite-dimensional module with trivial deck stabilizer has indecomposable literal skeletal push-down.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_of_hasShift_eq_indecomposable_of_trivial_stabilizer {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] [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)] [IsCancelSMul G C] (H : CategoryTheory.HasShift C (Additive G)) (hadd : ∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive) (hlinear : ∀ (a : Additive G), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)) (hH : H = D.hasShift) (M : FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) (htrivial : ∀ (a : Additive G), Nonempty (M ≅ (CategoryTheory.shiftFunctor (FiniteDimensionalModuleCategory k) a).obj M) → a = 0) : CategoryTheory.Indecomposable ((D.finiteDimensionalModuleOrbitSkeletonPushdown_of_hasShift_eq H hadd hlinear hH).obj M)

Indecomposability preservation transported across an explicit equality of shift instances.