Projective-stable covariant representables on the finite module skeleton

This is the functor \underline{Hom}(X, -) used in Auslander--Reiten, Proposition 1.3(a)(iii).

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveStableCovariantRepresentable {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : CategoryTheory.Functor S.IndecCategory (ModuleCat k)

The restriction of projective-stable Hom(X, -) to the finite skeleton of indecomposable right modules.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveStableCovariantRepresentable_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : (S.projectiveStableCovariantRepresentable X).Additive

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveStableCovariantRepresentable_linear {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : CategoryTheory.Functor.Linear k (S.projectiveStableCovariantRepresentable X)

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveStableCovariantRepresentableLinearModule {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : CoveringHom.LinearModuleCategory k

The restricted projective-stable covariant representable as a linear module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveStableCovariantRepresentable_isFiniteDimensional {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : CoveringHom.IsFiniteDimensionalModule k (S.projectiveStableCovariantRepresentableLinearModule X)

On the finite skeleton, the projective-stable covariant representable is pointwise finite-dimensional with finite support.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableCovariantRepresentable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : CoveringHom.FiniteDimensionalModuleCategory k

The projective-stable covariant representable as an object of the finite functor category.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveStableCovariantQuotientLinearModule {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : (S.finiteRestrictedCovariantRepresentable X).obj ⟶ (S.finiteProjectiveStableCovariantRepresentable X).obj

The objectwise quotient from ordinary Hom to projective-stable Hom.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableCovariantQuotient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : S.finiteRestrictedCovariantRepresentable X ⟶ S.finiteProjectiveStableCovariantRepresentable X

The quotient from ordinary Hom to projective-stable Hom in the finite functor category.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteProjectiveStableCovariantQuotient_epi {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : FinitelyGeneratedCategory A) : CategoryTheory.Epi (S.finiteProjectiveStableCovariantQuotient X)