Exactness of finite skeletal Gabriel push-down

The map induced by orbit push-down at a fixed downstairs object is the direct sum of the corresponding upstairs component maps. Direct sums of modules preserve exactness componentwise. Detecting exactness pointwise in the ambient functor category therefore proves that skeletal push-down is an exact functor.

The result descends through the full subcategories of additive linear modules and finite-dimensional finite-support modules. In particular, Gabriel push-down sends short exact sequences of finite-dimensional modules to short exact sequences on the chosen orbit skeleton.

theorem MagnitudeConjecture.CoveringHom.functionExact_directSum_lmap {R : Type uK} [Ring R] {ι : Type w} {V₁ V₂ V₃ : ι → Type uM} [(i : ι) → AddCommGroup (V₁ i)] [(i : ι) → Module R (V₁ i)] [(i : ι) → AddCommGroup (V₂ i)] [(i : ι) → Module R (V₂ i)] [(i : ι) → AddCommGroup (V₃ i)] [(i : ι) → Module R (V₃ i)] (f : (i : ι) → V₁ i →ₗ[R] V₂ i) (g : (i : ι) → V₂ i →ₗ[R] V₃ i) (h : ∀ (i : ι), Function.Exact ⇑(f i) ⇑(g i)) : Function.Exact ⇑(DirectSum.lmap f) ⇑(DirectSum.lmap g)

theorem MagnitudeConjecture.CoveringHom.functorCategory_exact_of_pointwise {J : Type u} [CategoryTheory.Category.{v, u} J] {D : Type uM} [CategoryTheory.Category.{uK, uM} D] [CategoryTheory.Abelian D] (S : CategoryTheory.ShortComplex (CategoryTheory.Functor J D)) (hS : ∀ (X : J), (S.map ((CategoryTheory.evaluation J D).obj X)).Exact) : S.Exact

theorem MagnitudeConjecture.CoveringHom.orbitPushdownNatTransAppLinear_eq_lmap {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] {M N : CategoryTheory.Functor C (ModuleCat k)} (α : M ⟶ N) (X : C) : orbitPushdownNatTransAppLinear α X = DirectSum.lmap fun (b : A) => ModuleCat.Hom.hom (α.app ((CategoryTheory.shiftFunctor C b).obj X))

theorem MagnitudeConjecture.CoveringHom.orbitPushdownNatTransAppLinear_injective {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] {M N : CategoryTheory.Functor C (ModuleCat k)} (α : M ⟶ N) (hα : ∀ (X : C), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (α.app X))) (X : C) : Function.Injective ⇑(orbitPushdownNatTransAppLinear α X)

theorem MagnitudeConjecture.CoveringHom.orbitPushdownNatTransAppLinear_surjective {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type w} [AddGroup A] [CategoryTheory.HasShift C A] {M N : CategoryTheory.Functor C (ModuleCat k)} (α : M ⟶ N) (hα : ∀ (X : C), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (α.app X))) (X : C) : Function.Surjective ⇑(orbitPushdownNatTransAppLinear α X)

instance MagnitudeConjecture.CoveringHom.linearModuleOrbitSkeletonPushdown_preservesMonomorphisms {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.HasShift C (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] : linearModuleOrbitSkeletonPushdown.PreservesMonomorphisms

instance MagnitudeConjecture.CoveringHom.linearModuleOrbitSkeletonPushdown_preservesEpimorphisms {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.HasShift C (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] : linearModuleOrbitSkeletonPushdown.PreservesEpimorphisms

theorem MagnitudeConjecture.CoveringHom.linearModuleOrbitSkeletonPushdown_map_exact {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.HasShift C (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] (S : CategoryTheory.ShortComplex (LinearModuleCategory k)) (hS : S.Exact) : (S.map linearModuleOrbitSkeletonPushdown).Exact

instance MagnitudeConjecture.CoveringHom.linearModuleOrbitSkeletonPushdown_preservesHomology {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.HasShift C (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] : linearModuleOrbitSkeletonPushdown.PreservesHomology

instance MagnitudeConjecture.CoveringHom.linearModuleOrbitSkeletonPushdown_preservesFiniteLimits {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.HasShift C (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] : CategoryTheory.Limits.PreservesFiniteLimits linearModuleOrbitSkeletonPushdown

instance MagnitudeConjecture.CoveringHom.linearModuleOrbitSkeletonPushdown_preservesFiniteColimits {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [CategoryTheory.HasShift C (Additive G)] [∀ (a : Additive G), (CategoryTheory.shiftFunctor C a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C a)] : CategoryTheory.Limits.PreservesFiniteColimits linearModuleOrbitSkeletonPushdown

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_map_exact {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (S : CategoryTheory.ShortComplex (FiniteDimensionalModuleCategory k)) (hS : S.Exact) : (S.map D.finiteDimensionalModuleOrbitSkeletonPushdown).Exact

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_preservesHomology {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G 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.PreservesHomology

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_preservesFiniteLimits {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G 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.Limits.PreservesFiniteLimits D.finiteDimensionalModuleOrbitSkeletonPushdown

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_preservesFiniteColimits {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G 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.Limits.PreservesFiniteColimits D.finiteDimensionalModuleOrbitSkeletonPushdown

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_map_shortExact {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {G : Type w} [Group G] [MulAction G C] [IsCancelSMul G C] (D : CoherentDeckShift C G) [∀ (a : Additive G), (D.core.F a).Additive] [∀ (a : Additive G), CategoryTheory.Functor.Linear k (D.core.F a)] (S : CategoryTheory.ShortComplex (FiniteDimensionalModuleCategory k)) (hS : S.ShortExact) : (S.map D.finiteDimensionalModuleOrbitSkeletonPushdown).ShortExact