Finite-dimensional Gabriel push-down on an orbit skeleton

A finite-support module upstairs has only finitely many nonzero translated values at a fixed object when the deck action is free. The corresponding direct sum is therefore finite-dimensional. After passing to one chosen representative per deck orbit, the object support of push-down is contained in the quotient image of the finite upstairs support.

These two facts restrict the generic skeletal Gabriel push-down functor to the finite-dimensional module categories used by the covering argument.

theorem MagnitudeConjecture.CoveringHom.finiteDimensional_directSum_of_finite_nontrivial {k : Type uK} [Field k] {ι : Type u} (V : ι → Type uM) [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [∀ (i : ι), FiniteDimensional k (V i)] (h : {i : ι | Nontrivial (V i)}.Finite) : FiniteDimensional k (DirectSum ι V)

A direct sum is finite-dimensional when only finitely many of its summands are nontrivial and every summand is finite-dimensional.

theorem MagnitudeConjecture.CoveringHom.exists_nontrivial_of_directSum_nontrivial {ι : Type u} (V : ι → Type uM) [(i : ι) → AddCommGroup (V i)] (h : Nontrivial (DirectSum ι V)) : ∃ (i : ι), Nontrivial (V i)

A nontrivial direct sum has a nontrivial summand.

theorem MagnitudeConjecture.CoveringHom.subsingleton_directSum_iff {ι : Type u} (V : ι → Type uM) [(i : ι) → AddCommGroup (V i)] : Subsingleton (DirectSum ι V) ↔ ∀ (i : ι), Subsingleton (V i)

A direct sum is subsingleton exactly when every summand is subsingleton.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.inverseTranslate_injective {C : Type u} {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G C] (X : C) : Function.Injective fun (b : Additive G) => (Additive.toMul b)⁻¹ • X

Freeness of the strict deck action makes inverse translates of a fixed object injectively indexed by the additive shift group.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.nontrivial_shift_value_iff {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) (M : FiniteDimensionalModuleCategory k) (b : Additive G) (X : C) : Nontrivial ↑(M.obj.obj.obj ((CategoryTheory.shiftFunctor C b).obj X)) ↔ (Additive.toMul b)⁻¹ • X ∈ moduleSupport k M.obj.obj

A shifted value is nonzero exactly when the corresponding inverse deck translate belongs to the upstairs object support.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finite_nontrivial_shift_values {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : CoherentDeckShift C G) (M : FiniteDimensionalModuleCategory k) (X : C) : {b : Additive G | Nontrivial ↑(M.obj.obj.obj ((CategoryTheory.shiftFunctor C b).obj X))}.Finite

At a fixed downstairs orbit, only finitely many translated summands of an upstairs finite-support module are nonzero.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonPushdown_pointwise_finite {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group 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) (q : DeckOrbitSkeleton C G) : FiniteDimensional k ↑((orbitSkeletonPushdown M.obj.obj).obj q)

Restriction to an orbit representative makes every push-down value finite-dimensional.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonPushdown_obj_isZero_iff {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) (q : DeckOrbitSkeleton C G) : CategoryTheory.Limits.IsZero ((orbitSkeletonPushdown M.obj.obj).obj q) ↔ ∀ (b : Additive G), CategoryTheory.Limits.IsZero (M.obj.obj.obj ((CategoryTheory.shiftFunctor C b).obj (deckOrbitRepresentative (have this := q; this))))

A skeletal push-down value is zero exactly when every translated upstairs value over that orbit is zero.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.moduleSupport_orbitSkeletonPushdown_subset {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) : moduleSupport k (orbitSkeletonPushdown M.obj.obj) ⊆ Quotient.mk'' '' moduleSupport k M.obj.obj

The support of skeletal push-down is contained in the quotient image of the finite upstairs support.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonPushdown_finite_support {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) : (moduleSupport k (orbitSkeletonPushdown M.obj.obj)).Finite

Skeletal push-down has finite literal object support.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonPushdown_isFiniteDimensionalModule {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group 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) : IsFiniteDimensionalModule k (linearModuleOrbitSkeletonPushdown.obj M.obj)

Skeletal push-down of a finite-dimensional upstairs module satisfies the downstairs pointwise and finite-support conditions.

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

Gabriel push-down from finite-dimensional upstairs modules to finite-dimensional modules on the one-representative-per-orbit base.

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

View the finite skeletal push-down through an extensionally chosen shift instance known to equal the coherent deck shift. Keeping the equality explicit prevents downstream orbit-category types from forcing Lean to normalize two large but equal shift constructions.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_of_hasShift_eq_obj_obj {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group 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)] (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) : ((D.finiteDimensionalModuleOrbitSkeletonPushdown_of_hasShift_eq H hadd hlinear hH).obj M).obj = linearModuleOrbitSkeletonPushdown.obj M.obj

The transported finite push-down has the expected underlying linear module object for the chosen shift instance.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_of_hasShift_eq_isoMk {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group 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)] (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) {Y : FiniteDimensionalModuleCategory k} : (linearModuleOrbitSkeletonPushdown.obj M.obj ≅ Y.obj) → ((D.finiteDimensionalModuleOrbitSkeletonPushdown_of_hasShift_eq H hadd hlinear hH).obj M ≅ Y)

Lift an isomorphism from the expected underlying push-down module through the transported finite-dimensional full subcategory.

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

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_of_hasShift_eq_additive {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group 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)] (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) : (D.finiteDimensionalModuleOrbitSkeletonPushdown_of_hasShift_eq H hadd hlinear hH).Additive

Additivity of finite push-down transported across an explicit equality of shift instances.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_linear {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type w} [Group 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)] : CategoryTheory.Functor.Linear k D.finiteDimensionalModuleOrbitSkeletonPushdown