Deck translations of representable modules

Inverse precomposition sends the covariant representable at X to the covariant representable at the correspondingly shifted object. Consequently, freeness of the deck action on isomorphism classes of category objects gives trivial deck stabilizers for finite-dimensional representables.

def MagnitudeConjecture.CoveringHom.IsFreeOnIsomorphismClasses {C : Type u_1} {G : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [Group G] [MulAction G C] : Prop

Freeness of an action on categorical vertices, i.e. on isomorphism classes of objects rather than only on the underlying object type.

theorem MagnitudeConjecture.CoveringHom.IsFreeOnIsomorphismClasses.restrict {C : Type u_1} {G : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [Group G] [MulAction G C] (hfree : IsFreeOnIsomorphismClasses) (N : Subgroup G) : IsFreeOnIsomorphismClasses

Freeness on isomorphism classes restricts to every subgroup.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearCoyonedaRestrictionLinearModule {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {E : Type u'} [CategoryTheory.Category.{v', u'} E] [CategoryTheory.Preadditive E] [CategoryTheory.Linear k E] (F : CategoryTheory.Functor C E) [F.Additive] [CategoryTheory.Functor.Linear k F] (X : E) : LinearModuleCategory k

Restriction of a covariant representable along a linear functor.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.representableShiftLinearEquiv {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)] (a : Additive G) (X Y : C) : (X ⟶ (D.core.F (-a)).obj Y) ≃ₗ[k] (D.core.F a).obj X ⟶ Y

The linear adjunction isomorphism between morphisms into an inverse shift and morphisms out of the corresponding positive shift.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearCoyonedaPrecompositionIso {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)] (a : Additive G) (X : C) : (D.core.F (-a)).comp ((CategoryTheory.linearCoyoneda k C).obj (Opposite.op X)) ≅ (CategoryTheory.linearCoyoneda k C).obj (Opposite.op ((D.core.F a).obj X))

Inverse precomposition of a covariant linear representable is the representable at the positively shifted source object.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearCoyonedaRestrictionShiftIso {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)] {E : Type u'} [CategoryTheory.Category.{v', u'} E] [MulAction G E] [CategoryTheory.Preadditive E] [CategoryTheory.Linear k E] (DE : CoherentDeckShift E G) [∀ (a : Additive G), (DE.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (DE.core.F a)] (F : CategoryTheory.Functor C E) [F.Additive] [CategoryTheory.Functor.Linear k F] (hcomm : F.CommShift (Additive G)) (a : Additive G) (X : E) : (CategoryTheory.shiftFunctor (LinearModuleCategory k) a).obj (linearCoyonedaRestrictionLinearModule F X) ≅ linearCoyonedaRestrictionLinearModule F ((DE.core.F a).obj X)

A translated restriction of a covariant representable along a shift-compatible functor is represented by the correspondingly translated ambient object.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearCoyonedaLinearModuleShiftIso {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)] (a : Additive G) (X : C) : (CategoryTheory.shiftFunctor (LinearModuleCategory k) a).obj (linearCoyonedaLinearModule X) ≅ linearCoyonedaLinearModule ((D.core.F a).obj X)

A translated covariant representable is represented by the correspondingly translated source object.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalLinearCoyonedaShiftIso {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)] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (a : Additive G) (X : C) : (CategoryTheory.shiftFunctor (FiniteDimensionalModuleCategory k) a).obj (finiteDimensionalLinearCoyoneda X ⋯) ≅ finiteDimensionalLinearCoyoneda ((D.core.F a).obj X) ⋯

The representable-shift comparison restricted to finite-dimensional modules.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalLinearCoyoneda_trivialStabilizer {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)] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hfree : IsFreeOnIsomorphismClasses) (X : C) (a : Additive G) : Nonempty (finiteDimensionalLinearCoyoneda X ⋯ ≅ (CategoryTheory.shiftFunctor (FiniteDimensionalModuleCategory k) a).obj (finiteDimensionalLinearCoyoneda X ⋯)) → a = 0

Freeness on isomorphism classes of representing objects implies trivial deck stabilizers for finite-dimensional representables.