Literal finite-representable presentations on the deck-orbit skeleton

The orbit-skeleton representables and dual corepresentables are finite at every downstairs object. The recoordinated pushed minimal presentation can therefore be packaged in the generic finite-representable interface used by the presentation-dependent Auslander--Reiten formula.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonLinearCoyonedaFinite {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)) (X : DeckOrbitSkeleton C G) : IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)

Finiteness of every covariant representable on the deck-orbit skeleton, obtained from any upstairs representative of its strict orbit.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonDualLinearYonedaFinite {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)] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) (X : DeckOrbitSkeleton C G) : IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)

Finiteness of every dual corepresentable on the deck-orbit skeleton, obtained from any upstairs representative of its strict orbit.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonTwoStepMinimalFiniteRepresentablePresentation {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) {M : FiniteDimensionalModuleCategory k} (Q : TwoStepMinimalFiniteRepresentablePresentation hP M) : TwoStepMinimalFiniteRepresentablePresentation ⋯ (D.finiteDimensionalModuleOrbitSkeletonPushdown.obj M)

The literal downstream minimal projective presentation, packaged with finite-representable coordinates indexed by the mapped upstairs vertices.

theorem MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonTwoStepMinimalFiniteRepresentablePresentation_representingDifferential {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) {M : FiniteDimensionalModuleCategory k} (Q : TwoStepMinimalFiniteRepresentablePresentation hP M) : (D.orbitSkeletonTwoStepMinimalFiniteRepresentablePresentation hP hlocal hfree Q).toTwoStepFiniteRepresentablePresentation.matrixDifferential = D.orbitSkeletonFunctor.op.mapMat_.map Q.toTwoStepFiniteRepresentablePresentation.matrixDifferential

The representing differential of the downstream finite-representable presentation is the upstairs representing matrix mapped to the orbit skeleton.