Projective and injective boundaries of finite orbit push-down

Gabriel's component argument also uses the boundary vertices of the Auslander--Reiten quiver. This file begins the boundary comparison by showing that the chosen deck-orbit skeleton again has local vertex endomorphism rings and that every indecomposable projective downstairs is the push-down of an indecomposable projective upstairs.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeleton_end_isLocalRing {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [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)] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (hfree : IsFreeOnIsomorphismClasses) (q : DeckOrbitSkeleton C G) : IsLocalRing (CategoryTheory.End q)

The endomorphism ring of every object of the chosen deck-orbit skeleton is local. This is inherited from an upstairs representative by passing to its finite representable, using Gabriel 3.5 for the pushed module, and then reflecting through fully faithful linear co-Yoneda.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.exists_projectiveIndecomposable_preimage {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [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)] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (hfree : IsFreeOnIsomorphismClasses) {Y : FiniteDimensionalModuleCategory k} [CategoryTheory.Projective Y] : CategoryTheory.Indecomposable Y → ∃ (M : FiniteDimensionalModuleCategory k), CategoryTheory.Projective M ∧ CategoryTheory.Indecomposable M ∧ Nonempty (D.finiteDimensionalModuleOrbitSkeletonPushdown.obj M ≅ Y)

Gabriel 3.6(b), projective boundary: every indecomposable projective on the deck-orbit skeleton is the push-down of an indecomposable projective finite module upstairs.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.exists_injectiveIndecomposable_preimage {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] {G : Type v} [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)] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (hfree : IsFreeOnIsomorphismClasses) {Y : FiniteDimensionalModuleCategory k} [CategoryTheory.Injective Y] : CategoryTheory.Indecomposable Y → ∃ (M : FiniteDimensionalModuleCategory k), CategoryTheory.Injective M ∧ CategoryTheory.Indecomposable M ∧ Nonempty (D.finiteDimensionalModuleOrbitSkeletonPushdown.obj M ≅ Y)

Gabriel 3.6(b), injective boundary: every indecomposable injective on the deck-orbit skeleton is the push-down of an indecomposable injective finite module upstairs.