Injective-stable covariant representables on the finite module skeleton

This file packages the costable functor Hom(X, -) modulo maps factoring through injectives. It is the functor-category target in the Auslander–Reiten Proposition 1.3 passage from a uniserial stable contravariant representable to a uniserial syzygy.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.injectiveStableCovariantRepresentable {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 injective-stable Hom(X, -) to the finite skeleton of indecomposable right modules.

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

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

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

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

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.injectiveStableCovariantRepresentable_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.injectiveStableCovariantRepresentableLinearModule X)

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

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteInjectiveStableCovariantRepresentable {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 restricted injective-stable covariant representable as an object of the finite functor category.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedCovariantRepresentable {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 ordinary covariant representable Hom(X, -) restricted to the finite indecomposable skeleton.

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

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

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

The ordinary restricted covariant representable as a linear module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.restrictedCovariantRepresentable_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.restrictedCovariantRepresentableLinearModule X)

The ordinary restricted covariant representable is finite-dimensional on the finite indecomposable skeleton.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteRestrictedCovariantRepresentable {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 ordinary restricted covariant representable in the finite functor category.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.injectiveStableCovariantQuotientLinearModule {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.finiteInjectiveStableCovariantRepresentable X).obj

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

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteInjectiveStableCovariantQuotient {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.finiteInjectiveStableCovariantRepresentable X

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

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteInjectiveStableCovariantQuotient_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.finiteInjectiveStableCovariantQuotient X)