Trivial stabilizers of finite-support modules

A nonzero finite-support module cannot be isomorphic to a nontrivial deck translate when the deck group is torsion-free and acts freely on objects.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModule_moduleSupport_nonempty {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.Limits.IsZero M) : (moduleSupport k M.obj.obj).Nonempty

A nonzero finite-dimensional module has a supported object.

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

A nonzero finite-support module has trivial translation stabilizer when the deck group is torsion-free and acts freely on objects.