Orbit push-down and finite projective Nakayama data

The matrix category Mat_ Cᵒᵖ is the finite additive envelope of the representing objects. Its linear-coyoneda lift consists of finite sums of projective representables, while the corresponding dual-Yoneda lift consists of their Nakayama images. This file extends the objectwise orbit push-down comparisons to those additive envelopes.

noncomputable def MagnitudeConjecture.CoveringHom.linearCoyonedaLinearModuleFunctor {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.Functor Cᵒᵖ (LinearModuleCategory k)

The linear coyoneda functor with codomain restricted to additive linear modules.

instance MagnitudeConjecture.CoveringHom.linearCoyonedaLinearModuleFunctor_additive {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : linearCoyonedaLinearModuleFunctor.Additive

instance MagnitudeConjecture.CoveringHom.linearCoyonedaLinearModuleFunctor_full {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : linearCoyonedaLinearModuleFunctor.Full

noncomputable def MagnitudeConjecture.CoveringHom.dualLinearYonedaFunctor {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C (ModuleCat k))

The coefficient-dual corepresentables as a functor on the opposite category of representing objects.

instance MagnitudeConjecture.CoveringHom.dualLinearYonedaFunctor_additive {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : dualLinearYonedaFunctor.Additive

noncomputable def MagnitudeConjecture.CoveringHom.dualLinearYonedaLinearModuleFunctor {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.Functor Cᵒᵖ (LinearModuleCategory k)

The dual corepresentable functor with codomain restricted to additive linear modules.

instance MagnitudeConjecture.CoveringHom.dualLinearYonedaLinearModuleFunctor_additive {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : dualLinearYonedaLinearModuleFunctor.Additive

noncomputable def MagnitudeConjecture.CoveringHom.finiteDimensionalLinearCoyonedaFunctor {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : CategoryTheory.Functor Cᵒᵖ (FiniteDimensionalModuleCategory k)

Finite projective representables, functorially bundled in the literal finite-dimensional module category.

instance MagnitudeConjecture.CoveringHom.finiteDimensionalLinearCoyonedaFunctor_additive {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : (finiteDimensionalLinearCoyonedaFunctor hP).Additive

instance MagnitudeConjecture.CoveringHom.finiteDimensionalLinearCoyonedaFunctor_faithful {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : (finiteDimensionalLinearCoyonedaFunctor hP).Faithful

instance MagnitudeConjecture.CoveringHom.finiteDimensionalLinearCoyonedaFunctor_full {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : (finiteDimensionalLinearCoyonedaFunctor hP).Full

noncomputable def MagnitudeConjecture.CoveringHom.finiteDimensionalDualLinearYonedaFunctor {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : CategoryTheory.Functor Cᵒᵖ (FiniteDimensionalModuleCategory k)

Finite dual corepresentables, functorially bundled in the literal finite-dimensional module category.

instance MagnitudeConjecture.CoveringHom.finiteDimensionalDualLinearYonedaFunctor_additive {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : (finiteDimensionalDualLinearYonedaFunctor hI).Additive

noncomputable def MagnitudeConjecture.CoveringHom.finiteMatrixLift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] : CategoryTheory.Functor (CategoryTheory.Mat_ C) D

Universe-polymorphic finite additive-envelope lift. This is the same matrix construction as Mat_.lift, without its same-universe restriction on the target category.

@[simp]

theorem MagnitudeConjecture.CoveringHom.finiteMatrixLift_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] (X : CategoryTheory.Mat_ C) : (finiteMatrixLift F).obj X = ⨁ fun (i : X.ι) => F.obj (X.X i)

@[simp]

theorem MagnitudeConjecture.CoveringHom.finiteMatrixLift_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] {X✝ Y✝ : CategoryTheory.Mat_ C} (f : X✝ ⟶ Y✝) : (finiteMatrixLift F).map f = CategoryTheory.Limits.biproduct.matrix fun (i : X✝.ι) (j : Y✝.ι) => F.map (f i j)

instance MagnitudeConjecture.CoveringHom.finiteMatrixLift_additive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] : (finiteMatrixLift F).Additive

instance MagnitudeConjecture.CoveringHom.finiteMatrixLift_faithful {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] [F.Faithful] : (finiteMatrixLift F).Faithful

instance MagnitudeConjecture.CoveringHom.finiteMatrixLift_full {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] [F.Full] : (finiteMatrixLift F).Full

noncomputable def MagnitudeConjecture.CoveringHom.finiteMatrixPushforwardIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type uD} [CategoryTheory.Category.{vD, uD} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] {E : Type uE} [CategoryTheory.Category.{vE, uE} E] [CategoryTheory.Preadditive E] [CategoryTheory.Limits.HasFiniteBiproducts E] (F : CategoryTheory.Functor C D) [F.Additive] (P : CategoryTheory.Functor D E) [P.Additive] (H : CategoryTheory.Functor C E) [H.Additive] (e : F.comp P ≅ H) : (finiteMatrixLift F).comp P ≅ finiteMatrixLift H

A natural isomorphism after an additive functor extends componentwise to finite matrices, with the additive functor's canonical biproduct comparison on the source.

noncomputable def MagnitudeConjecture.CoveringHom.finiteProjectiveRepresentableSumFunctor {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : CategoryTheory.Functor (CategoryTheory.Mat_ Cᵒᵖ) (FiniteDimensionalModuleCategory k)

Finite sums of finite-dimensional projective representables, with maps encoded as matrices between the representing objects.

instance MagnitudeConjecture.CoveringHom.finiteProjectiveRepresentableSumFunctor_faithful {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : (finiteProjectiveRepresentableSumFunctor hP).Faithful

noncomputable def MagnitudeConjecture.CoveringHom.finiteNakayamaRepresentableSumFunctor {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : CategoryTheory.Functor (CategoryTheory.Mat_ Cᵒᵖ) (FiniteDimensionalModuleCategory k)

Finite sums of finite dual corepresentables, the Nakayama images of the corresponding finite sums of projective representables.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonFiniteDimensionalLinearCoyonedaFunctor {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)] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : CategoryTheory.Functor Cᵒᵖ (FiniteDimensionalModuleCategory k)

The finite projective representables on chosen strict orbits, indexed by their upstairs representing objects.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonFiniteDimensionalLinearCoyonedaFunctor_additive {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)] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : (D.orbitSkeletonFiniteDimensionalLinearCoyonedaFunctor hP).Additive

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonFiniteDimensionalDualLinearYonedaFunctor {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)] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : CategoryTheory.Functor Cᵒᵖ (FiniteDimensionalModuleCategory k)

The finite dual corepresentables on chosen strict orbits, indexed by their upstairs representing objects.

instance MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonFiniteDimensionalDualLinearYonedaFunctor_additive {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)] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : (D.orbitSkeletonFiniteDimensionalDualLinearYonedaFunctor hI).Additive

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownLinearCoyonedaNatIso {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)] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : (finiteDimensionalLinearCoyonedaFunctor hP).comp D.finiteDimensionalModuleOrbitSkeletonPushdown ≅ D.orbitSkeletonFiniteDimensionalLinearCoyonedaFunctor hP

The finite projective-representable comparison, bundled as a natural isomorphism in the upstairs representing object.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteDimensionalModuleOrbitSkeletonPushdownDualLinearYonedaNatIso {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)] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : (finiteDimensionalDualLinearYonedaFunctor hI).comp D.finiteDimensionalModuleOrbitSkeletonPushdown ≅ D.orbitSkeletonFiniteDimensionalDualLinearYonedaFunctor hI

The finite dual-corepresentable comparison, bundled as a natural isomorphism in the upstairs representing object.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonFiniteProjectiveRepresentableSumFunctor {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)] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : CategoryTheory.Functor (CategoryTheory.Mat_ Cᵒᵖ) (FiniteDimensionalModuleCategory k)

Finite sums of projective representables on the chosen strict orbit skeleton, still indexed by their upstairs representing objects.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.orbitSkeletonFiniteNakayamaRepresentableSumFunctor {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)] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : CategoryTheory.Functor (CategoryTheory.Mat_ Cᵒᵖ) (FiniteDimensionalModuleCategory k)

Finite sums of dual corepresentables on the chosen strict orbit skeleton, still indexed by their upstairs representing objects.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteProjectiveRepresentableSumOrbitSkeletonPushdownIso {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)] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : (finiteProjectiveRepresentableSumFunctor hP).comp D.finiteDimensionalModuleOrbitSkeletonPushdown ≅ D.orbitSkeletonFiniteProjectiveRepresentableSumFunctor hP

Orbit push-down commutes with finite sums and matrices of projective representables.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteNakayamaRepresentableSumOrbitSkeletonPushdownIso {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)] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) : (finiteNakayamaRepresentableSumFunctor hI).comp D.finiteDimensionalModuleOrbitSkeletonPushdown ≅ D.orbitSkeletonFiniteNakayamaRepresentableSumFunctor hI

Orbit push-down commutes with the finite sums and matrices of dual corepresentables that occur after applying Nakayama.

noncomputable def MagnitudeConjecture.CoveringHom.CoherentDeckShift.finiteNakayamaKernelOrbitSkeletonPushdownIso {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)] (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {P₁ P₀ : CategoryTheory.Mat_ Cᵒᵖ} (d : P₁ ⟶ P₀) : D.finiteDimensionalModuleOrbitSkeletonPushdown.obj (CategoryTheory.Limits.kernel ((finiteNakayamaRepresentableSumFunctor hI).map d)) ≅ CategoryTheory.Limits.kernel ((D.orbitSkeletonFiniteNakayamaRepresentableSumFunctor hI).map d)

Exact orbit push-down transports the kernel of a matrix between finite Nakayama sums to the kernel of the pushed matrix. For a minimal projective presentation, this is the categorical kernel that defines the Auslander--Reiten translate.