Almost-split factorization under finite skeletal push-down

This file formalizes the componentwise adjunction/Hom-formula step in Gabriel's proof that push-down preserves Auslander--Reiten sequences. A downstairs endomorphism is decomposed into finitely many homogeneous maps to deck translates. Once its identity component is known not to be split monic, trivial deck stabilizer gives the same conclusion in every nonidentity degree. The upstairs left almost-split map then factors all components, and finite-support convolution assembles the required downstairs factorization.

The identity-component assertion is proved by comparing the residue maps of the upstairs and downstairs finite-dimensional local endomorphism algebras.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalShiftHom {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 : FiniteDimensionalModuleCategory k) (a : Additive G) : ShiftHom M.obj N.obj a → (M ⟶ (CategoryTheory.shiftFunctor (FiniteDimensionalModuleCategory k) a).obj N)

A homogeneous map between the underlying linear modules, regarded as a map to the corresponding finite-dimensional shifted module.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalShiftHom_map {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 : FiniteDimensionalModuleCategory k) (a : Additive G) (q : ShiftHom M.obj N.obj a) : (IsFiniteDimensionalModule k).ι.map (D.finiteDimensionalShiftHom M N a q) = CategoryTheory.CategoryStruct.comp q (finiteDimensionalModuleShiftUnderlyingIso k D N a).inv

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalShiftHom_roundtrip {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 : FiniteDimensionalModuleCategory k) (a : Additive G) (q : ShiftHom M.obj N.obj a) : CategoryTheory.CategoryStruct.comp ((IsFiniteDimensionalModule k).ι.map (D.finiteDimensionalShiftHom M N a q)) (finiteDimensionalModuleShiftUnderlyingIso k D N a).hom = q

Passing a homogeneous map into the finite shifted category and then back to the underlying shifted linear module recovers the original map.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModule_trivial_linear_stabilizer {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)] (L : FiniteDimensionalModuleCategory k) : (∀ (a : Additive G), Nonempty (L ≅ (CategoryTheory.shiftFunctor (FiniteDimensionalModuleCategory k) a).obj L) → a = 0) → ∀ (a : Additive G), Nonempty (L.obj ≅ (CategoryTheory.shiftFunctor (LinearModuleCategory k) a).obj L.obj) → a = 0

Trivial deck stabilizer passes from a finite-dimensional module to its underlying linear module.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.shiftOrbitComponent_factor {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)] (L E : FiniteDimensionalModuleCategory k) (a : Additive G) (f : L ⟶ E) (q : ShiftHom L.obj L.obj a) (c : E ⟶ (CategoryTheory.shiftFunctor (FiniteDimensionalModuleCategory k) a).obj L) : CategoryTheory.CategoryStruct.comp f c = D.finiteDimensionalShiftHom L L a q → (shiftOrbitCompHom ((shiftOrbitOf L.obj E.obj 0) (shiftHomZero f.hom))) ((shiftOrbitOf E.obj L.obj a) (CategoryTheory.CategoryStruct.comp c.hom (finiteDimensionalModuleShiftUnderlyingIso k D L a).hom)) = (shiftOrbitOf L.obj L.obj a) q

A finite-dimensional factorization of one homogeneous component gives the corresponding singleton factorization in the shift-orbit category.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_reflects_splitMono {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) : CategoryTheory.IsSplitMono (D.finiteDimensionalModuleOrbitSkeletonPushdown.map f) → CategoryTheory.IsSplitMono f

A split monomorphism after finite skeletal push-down was already split upstairs. A downstairs retraction is pulled back through the covering Hom equivalence, and its degree-zero component retracts the original map.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_map_g_not_isSplitEpi {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] (S : CategoryTheory.ShortComplex (FiniteDimensionalModuleCategory k)) (hS : S.ShortExact) (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit S.f) : ¬CategoryTheory.IsSplitEpi (S.map D.finiteDimensionalModuleOrbitSkeletonPushdown).g

The terminal map of a pushed short exact sequence cannot split when the upstairs initial map is left almost split.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_leftEndomorphism_factor {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] (L E : FiniteDimensionalModuleCategory k) (f : L ⟶ E) (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f) (q : D.finiteDimensionalModuleOrbitSkeletonPushdown.obj L ⟶ D.finiteDimensionalModuleOrbitSkeletonPushdown.obj L) : (∀ (a : Additive G), ¬CategoryTheory.IsSplitMono (D.finiteDimensionalShiftHom L L a (((D.finiteDimensionalModuleOrbitSkeletonPushdownHomLinearEquiv L L).symm q) a))) → ∃ (c : D.finiteDimensionalModuleOrbitSkeletonPushdown.obj E ⟶ D.finiteDimensionalModuleOrbitSkeletonPushdown.obj L), CategoryTheory.CategoryStruct.comp (D.finiteDimensionalModuleOrbitSkeletonPushdown.map f) c = q

If every homogeneous component of a downstairs endomorphism is nonsplit monic upstairs, an upstairs left almost-split injection factors the entire endomorphism after finite skeletal push-down.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_allComponents_not_isSplitMono_of_identity {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] (L : FiniteDimensionalModuleCategory k) (hL : CategoryTheory.Indecomposable L) (q : D.finiteDimensionalModuleOrbitSkeletonPushdown.obj L ⟶ D.finiteDimensionalModuleOrbitSkeletonPushdown.obj L) : (∀ (a : Additive G), Nonempty (L ≅ (CategoryTheory.shiftFunctor (FiniteDimensionalModuleCategory k) a).obj L) → a = 0) → ¬CategoryTheory.IsSplitMono (D.finiteDimensionalShiftHom L L 0 (((D.finiteDimensionalModuleOrbitSkeletonPushdownHomLinearEquiv L L).symm q) 0)) → ∀ (a : Additive G), ¬CategoryTheory.IsSplitMono (D.finiteDimensionalShiftHom L L a (((D.finiteDimensionalModuleOrbitSkeletonPushdownHomLinearEquiv L L).symm q) a))

For an indecomposable with trivial deck stabilizer, nonsplitness of the identity component of a downstairs endomorphism forces nonsplitness of every homogeneous component.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_identityComponent_not_isSplitMono {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] [IsAlgClosed k] (L : FiniteDimensionalModuleCategory k) (hL : CategoryTheory.Indecomposable L) : (∀ (a : Additive G), Nonempty (L ≅ (CategoryTheory.shiftFunctor (FiniteDimensionalModuleCategory k) a).obj L) → a = 0) → ∀ (q : D.finiteDimensionalModuleOrbitSkeletonPushdown.obj L ⟶ D.finiteDimensionalModuleOrbitSkeletonPushdown.obj L), ¬CategoryTheory.IsIso q → ¬CategoryTheory.IsSplitMono (D.finiteDimensionalShiftHom L L 0 (((D.finiteDimensionalModuleOrbitSkeletonPushdownHomLinearEquiv L L).symm q) 0))

A noninvertible endomorphism of the pushed indecomposable has nonsplit identity component upstairs. This is Gabriel's identity-component nilpotence/nonunit assertion, proved through the unique residue maps of the two finite-dimensional local endomorphism algebras.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdown_leftEndomorphism_factor_of_trivial_stabilizer {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] [IsAlgClosed k] (L E : FiniteDimensionalModuleCategory k) (hL : CategoryTheory.Indecomposable L) (f : L ⟶ E) (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f) : (∀ (a : Additive G), Nonempty (L ≅ (CategoryTheory.shiftFunctor (FiniteDimensionalModuleCategory k) a).obj L) → a = 0) → ∀ (q : D.finiteDimensionalModuleOrbitSkeletonPushdown.obj L ⟶ D.finiteDimensionalModuleOrbitSkeletonPushdown.obj L), ¬CategoryTheory.IsIso q → ∃ (c : D.finiteDimensionalModuleOrbitSkeletonPushdown.obj E ⟶ D.finiteDimensionalModuleOrbitSkeletonPushdown.obj L), CategoryTheory.CategoryStruct.comp (D.finiteDimensionalModuleOrbitSkeletonPushdown.map f) c = q

Every noninvertible endomorphism of the pushed left term factors through the pushed left almost-split injection.