Finitely generated morphism modules over a finite algebra

For an algebra A over a commutative ring R, Mathlib's scoped ModuleCat.Algebra.instLinear makes ModuleCat A an R-linear category. When R is Noetherian and A is finitely generated as an R-module (for instance an Artin algebra, or a finite-dimensional algebra over a field), the morphisms between two finitely generated A-modules form a finitely generated R-module (the instance ModuleCat.finite_hom_of_finite, and FGModuleCat.finite_hom in FGModuleCat A). This is the Hom-finiteness that dimension and length counts in the module category of such an algebra rest on.

The morphism space is identified with the A-linear maps by ModuleCat.homLinearEquiv, and those embed in maps into a power of the target by TauCeti.isNoetherian_linearMap_of_finite.

A module bundled in ModuleCat A remembers only the action of A. ModuleCat.moduleOfAlgebra recovers its R-action through the algebra map, for any commutative base ring R; Mathlib records this for algebras over a field in ModuleCat.moduleOfAlgebraModule.

@[reducible, inline]

abbrev ModuleCat.moduleOfAlgebra (R : Type u) [CommRing R] {B : Type v} [Ring B] [Algebra R B] (M : ModuleCat B) : Module R ↑M

A module over an R-algebra, as a module over R. Mathlib records this for algebras over a field in ModuleCat.moduleOfAlgebraModule.

theorem ModuleCat.isScalarTower_moduleOfAlgebra (R : Type u) [CommRing R] {B : Type v} [Ring B] [Algebra R B] (M : ModuleCat B) : IsScalarTower R B ↑M

The action of R given by ModuleCat.moduleOfAlgebra is the action through the algebra map.

instance ModuleCat.finite_hom_of_finite {R : Type u} {A : Type v} [CommRing R] [IsNoetherianRing R] [Ring A] [Algebra R A] [Module.Finite R A] (M N : ModuleCat A) [Module.Finite A ↑M] [Module.Finite A ↑N] : Module.Finite R (M ⟶ N)

Morphisms between finitely generated modules over a finite algebra over a Noetherian ring form a finitely generated module over the base ring.

instance FGModuleCat.finite_hom {R : Type u} {A : Type v} [CommRing R] [IsNoetherianRing R] [Ring A] [Algebra R A] [Module.Finite R A] (X Y : FGModuleCat A) : Module.Finite R (X ⟶ Y)

Morphisms in FGModuleCat A, for a finite algebra A over a Noetherian ring, form a finitely generated module over the base ring.