noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownWindow {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)] (W : Set (FiniteDimensionalModuleCategory k)) : CategoryTheory.Functor (CoveringSeparation.WindowCategory W) (FiniteDimensionalModuleCategory k)

The finite-dimensional skeletal push-down restricted to a full control window of upstairs modules.

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

The finite push-down's orbit Hom decomposition restricted to a full control window.

def MagnitudeConjecture.CoveringHom.CoherentDeckShift.FiniteModuleWindowShiftHomOrthogonal {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)] (W : Set (FiniteDimensionalModuleCategory k)) : Prop

Nonidentity shifted Homs vanish between every ordered pair of modules in the control window.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteModuleWindowTranslateHomOrthogonal_of_shiftHomOrthogonal {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)] (W : Set (FiniteDimensionalModuleCategory k)) : D.FiniteModuleWindowShiftHomOrthogonal W → TranslateHomOrthogonal fun (M N : CoveringSeparation.WindowCategory W) (g : Multiplicative (Additive G)) => multiplicativeShiftHom M.obj.obj N.obj.obj g

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownWindow_full {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)] (W : Set (FiniteDimensionalModuleCategory k)) : D.FiniteModuleWindowShiftHomOrthogonal W → (D.finiteDimensionalModuleOrbitSkeletonPushdownWindow W).Full

A translate-orthogonal module window makes finite skeletal push-down full on that window.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownWindow_faithful {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)] (W : Set (FiniteDimensionalModuleCategory k)) : (D.finiteDimensionalModuleOrbitSkeletonPushdownWindow W).Faithful

Finite skeletal push-down is faithful on every full control window.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownWindow_obj_indecomposable {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)] (W : Set (FiniteDimensionalModuleCategory k)) : D.FiniteModuleWindowShiftHomOrthogonal W → ∀ (M : CoveringSeparation.WindowCategory W), CategoryTheory.Indecomposable M.obj → CategoryTheory.Indecomposable ((D.finiteDimensionalModuleOrbitSkeletonPushdownWindow W).obj M)

Every indecomposable object in a translate-orthogonal window has indecomposable finite skeletal push-down. In particular, the finite-cover separation used by the campaign preserves the selected indecomposable vertices without invoking global density.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.isIrreducibleMorphism_finiteOrbitPushdownWindowMap_iff {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)] (W : Set (FiniteDimensionalModuleCategory k)) : D.FiniteModuleWindowShiftHomOrthogonal W → ∀ {X Y : CoveringSeparation.WindowCategory W} {f : X ⟶ Y}, IsLocallyFactorizationClosedAt (D.finiteDimensionalModuleOrbitSkeletonPushdownWindow W) f → (QuotientSubmoduleEquidistribution.IsIrreducibleMorphism ((D.finiteDimensionalModuleOrbitSkeletonPushdownWindow W).map f) ↔ QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f)

On a translate-orthogonal window, finite skeletal push-down identifies irreducibility once the relevant downstairs factorizations stay in the local essential image.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.rightAlmostSplit_finiteOrbitPushdownWindowMap {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)] (W : Set (FiniteDimensionalModuleCategory k)) : D.FiniteModuleWindowShiftHomOrthogonal W → ∀ {X Y : CoveringSeparation.WindowCategory W} {f : X ⟶ Y}, QuotientSubmoduleEquidistribution.IsRightAlmostSplit f → IsLocallyRightObjectClosedAt (D.finiteDimensionalModuleOrbitSkeletonPushdownWindow W) Y → QuotientSubmoduleEquidistribution.IsRightAlmostSplit ((D.finiteDimensionalModuleOrbitSkeletonPushdownWindow W).map f)

The same local interface transports right almost-split maps.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.leftAlmostSplit_finiteOrbitPushdownWindowMap {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)] (W : Set (FiniteDimensionalModuleCategory k)) : D.FiniteModuleWindowShiftHomOrthogonal W → ∀ {X Y : CoveringSeparation.WindowCategory W} {f : X ⟶ Y}, QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f → IsLocallyLeftObjectClosedAt (D.finiteDimensionalModuleOrbitSkeletonPushdownWindow W) X → QuotientSubmoduleEquidistribution.IsLeftAlmostSplit ((D.finiteDimensionalModuleOrbitSkeletonPushdownWindow W).map f)

The dual local interface transports left almost-split maps.