Deck translations on finite-dimensional modules

For a locally bounded category, a finite-dimensional module is pointwise finite-dimensional and has finite object support. This file defines that literal full subcategory of linear modules and proves that coherent deck translations preserve it.

def MagnitudeConjecture.CoveringHom.moduleSupport {C : Type u} [CategoryTheory.Category.{v, u} C] (k : Type uK) [Field k] (M : CategoryTheory.Functor C (ModuleCat k)) : Set C

The object support of a module-valued functor.

def MagnitudeConjecture.CoveringHom.IsFiniteDimensionalModule {C : Type u} [CategoryTheory.Category.{v, u} C] (k : Type uK) [Field k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.ObjectProperty (LinearModuleCategory k)

A linear module is finite-dimensional when it is pointwise finite-dimensional and has finite object support.

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleCategory {C : Type u} [CategoryTheory.Category.{v, u} C] (k : Type uK) [Field k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : Type (max (max (max u uK) v) (u_1 + 1))

The full category of finite-dimensional linear modules over C.

instance MagnitudeConjecture.CoveringHom.instFiniteDimensionalCarrierObjModuleCatObjFunctorIsLinearModuleLinearModuleCategoryIsFiniteDimensionalModule {C : Type u} [CategoryTheory.Category.{v, u} C] (k : Type uK) [Field k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) (X : C) : FiniteDimensional k ↑(M.obj.obj.obj X)

theorem MagnitudeConjecture.CoveringHom.finite_moduleSupport {C : Type u} [CategoryTheory.Category.{v, u} C] (k : Type uK) [Field k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (M : FiniteDimensionalModuleCategory k) : (moduleSupport k M.obj.obj).Finite

A finite-dimensional module has finite object support.

instance MagnitudeConjecture.CoveringHom.instIsClosedUnderIsomorphismsLinearModuleCategoryIsFiniteDimensionalModule {C : Type u} [CategoryTheory.Category.{v, u} C] (k : Type uK) [Field k] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : (IsFiniteDimensionalModule k).IsClosedUnderIsomorphisms

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.moduleSupport_shift_eq_preimage {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (k : Type uK) [Field k] [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 : LinearModuleCategory k) (g : G) : moduleSupport k ((IsLinearModule k).ι.obj ((CategoryTheory.shiftFunctor (IsLinearModule k).FullSubcategory (Additive.ofMul g)).obj M)) = (fun (x : C) => g • x) ⁻¹' moduleSupport k M.obj

The support of a translated linear module is the preimage of its support under the corresponding strict left deck transformation.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.isFiniteDimensionalModule_stableUnderShift {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (k : Type uK) [Field k] [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)] : (IsFiniteDimensionalModule k).IsStableUnderShift (Additive G)

@[implicit_reducible]

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleCategoryHasShift {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (k : Type uK) [Field k] [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)] : CategoryTheory.HasShift (FiniteDimensionalModuleCategory k) (Additive G)

Coherent deck translation restricts to finite-dimensional modules.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleShiftUnderlyingIso {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (k : Type uK) [Field k] [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) : (IsFiniteDimensionalModule k).ι.obj ((CategoryTheory.shiftFunctor (IsFiniteDimensionalModule k).FullSubcategory a).obj M) ≅ (CategoryTheory.shiftFunctor (LinearModuleCategory k) a).obj M.obj

The finite-dimensional restriction forgets to the previously constructed linear-module translation.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleSupport_shift_eq_preimage {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (k : Type uK) [Field k] [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) (g : G) : moduleSupport k ((IsFiniteDimensionalModule k).ι.obj ((CategoryTheory.shiftFunctor (IsFiniteDimensionalModule k).FullSubcategory (Additive.ofMul g)).obj M)).obj = (fun (x : C) => g • x) ⁻¹' moduleSupport k M.obj.obj

The support formula for deck translation, stated directly for the finite-dimensional full subcategory.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleShiftEvaluationIso {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] (k : Type uK) [Field k] [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) (g : G) (X : C) : ((IsLinearModule k).ι.obj ((IsFiniteDimensionalModule k).ι.obj ((CategoryTheory.shiftFunctor (IsFiniteDimensionalModule k).FullSubcategory (Additive.ofMul g)).obj M))).obj X ≅ M.obj.obj.obj (g • X)

Evaluation of a translated finite-dimensional module obeys Gabriel's inverse-translation formula.