noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearModuleOrbitSkeletonRestrictionLinear {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 N : LinearModuleCategory k) : (linearModuleOrbitPushdown.obj M ⟶ linearModuleOrbitPushdown.obj N) →ₗ[k] linearModuleOrbitSkeletonPushdown.obj M ⟶ linearModuleOrbitSkeletonPushdown.obj N

Restriction from the nonskeletal orbit category to its chosen deck-orbit skeleton, on Homs between push-down modules.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearModuleOrbitSkeletonRestrictionLinear_bijective {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 N : LinearModuleCategory k) : Function.Bijective ⇑(D.linearModuleOrbitSkeletonRestrictionLinear M N)

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearModuleOrbitSkeletonRestrictionLinearEquiv {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 N : LinearModuleCategory k) : (linearModuleOrbitPushdown.obj M ⟶ linearModuleOrbitPushdown.obj N) ≃ₗ[k] linearModuleOrbitSkeletonPushdown.obj M ⟶ linearModuleOrbitSkeletonPushdown.obj N

Restriction along the representative equivalence is a linear equivalence on Homs between push-down modules.

@[simp]

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearModuleOrbitSkeletonRestrictionLinearEquiv_apply {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 N : LinearModuleCategory k) (α : linearModuleOrbitPushdown.obj M ⟶ linearModuleOrbitPushdown.obj N) : (D.linearModuleOrbitSkeletonRestrictionLinearEquiv M N) α = CategoryTheory.ObjectProperty.homMk (deckOrbitRepresentativeFunctor.whiskerLeft α.hom)

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearModuleOrbitSkeletonPushdownHomLinearEquiv {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) (N : LinearModuleCategory k) : ShiftOrbitHom (Additive G) M.obj N ≃ₗ[k] linearModuleOrbitSkeletonPushdown.obj M.obj ⟶ linearModuleOrbitSkeletonPushdown.obj N

Gabriel's Hom formula after restricting the base to the chosen deck-orbit skeleton.

@[simp]

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.linearModuleOrbitSkeletonPushdownHomLinearEquiv_apply {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) (N : LinearModuleCategory k) (f : ShiftOrbitHom (Additive G) M.obj N) : (D.linearModuleOrbitSkeletonPushdownHomLinearEquiv M N) f = (D.linearModuleOrbitSkeletonRestrictionLinear M.obj N) ((linearModuleOrbitPushdownSynthesisLinear D.core M.obj N) f)

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownHomLinearEquiv {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 N : FiniteDimensionalModuleCategory k) : ShiftOrbitHom (Additive G) M.obj N.obj ≃ₗ[k] D.finiteDimensionalModuleOrbitSkeletonPushdown.obj M ⟶ D.finiteDimensionalModuleOrbitSkeletonPushdown.obj N

Manuscript-facing Gabriel Hom formula for the literal finite-dimensional push-down on one chosen representative of each deck orbit.

@[simp]

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownHomLinearEquiv_apply_hom {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 N : FiniteDimensionalModuleCategory k) (f : ShiftOrbitHom (Additive G) M.obj N.obj) : ((D.finiteDimensionalModuleOrbitSkeletonPushdownHomLinearEquiv M N) f).hom = (D.linearModuleOrbitSkeletonPushdownHomLinearEquiv M N.obj) f

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownHomLinearEquiv_comp {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 N Z : FiniteDimensionalModuleCategory k) (f : ShiftOrbitHom (Additive G) M.obj N.obj) (g : ShiftOrbitHom (Additive G) N.obj Z.obj) : CategoryTheory.CategoryStruct.comp ((D.finiteDimensionalModuleOrbitSkeletonPushdownHomLinearEquiv M N) f) ((D.finiteDimensionalModuleOrbitSkeletonPushdownHomLinearEquiv N Z) g) = (D.finiteDimensionalModuleOrbitSkeletonPushdownHomLinearEquiv M Z) ((shiftOrbitCompHom f) g)

The finite-dimensional skeletal Gabriel Hom equivalence respects shift-orbit convolution.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownHomLinearEquiv_zero {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 N : FiniteDimensionalModuleCategory k) (f : M ⟶ N) : (D.finiteDimensionalModuleOrbitSkeletonPushdownHomLinearEquiv M N) ((shiftOrbitOf M.obj N.obj 0) (shiftHomZero f.hom)) = D.finiteDimensionalModuleOrbitSkeletonPushdown.map f

The manuscript-facing Hom equivalence sends the degree-zero inclusion of an ordinary finite-dimensional module map to the existing finite push-down functor map.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownHomDecomposition {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 N : FiniteDimensionalModuleCategory k) : OrbitHomDecomposition (D.finiteDimensionalModuleOrbitSkeletonPushdown.obj M ⟶ D.finiteDimensionalModuleOrbitSkeletonPushdown.obj N)

Gabriel's Hom decomposition for one pair of finite-dimensional upstairs modules and their literal skeletal push-downs.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownOrbitHomDecomposition {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] : FunctorOrbitHomDecomposition D.finiteDimensionalModuleOrbitSkeletonPushdown fun (M N : FiniteDimensionalModuleCategory k) (g : Multiplicative (Additive G)) => multiplicativeShiftHom M.obj N.obj g

The finite-dimensional skeletal push-down satisfies the functor-level Gabriel orbit Hom interface.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_faithful {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] : D.finiteDimensionalModuleOrbitSkeletonPushdown.Faithful

Finite-dimensional skeletal Gabriel push-down is faithful, without any translate-orthogonality hypothesis.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_of_hasShift_eq_faithful {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) : (D.finiteDimensionalModuleOrbitSkeletonPushdown_of_hasShift_eq H hadd hlinear hH).Faithful

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

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_indecomposable_of_selfShiftHomOrthogonal {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), a ≠ 0 → Subsingleton (ShiftHom M.obj M.obj a)) → CategoryTheory.Indecomposable (D.finiteDimensionalModuleOrbitSkeletonPushdown.obj M)

If an upstairs indecomposable module has no maps to any of its nontrivial shifts, then its literal finite skeletal push-down is indecomposable. This is the separated-window form of Gabriel's indecomposability argument and does not use density.