Finite-dimensional injective envelopes

Every finite-dimensional module over a finite-dimensional algebra has a finite-dimensional injective envelope. No algebraic closedness or self-injectivity is required. The result also applies to finitely generated modules, with their base-field action induced from the algebra.

Finite powers of the dual of the right regular module provide finite-dimensional injective ambient modules. Restricting an embedding into one of these yields an envelope, so its uniqueness follows from the general injective-envelope API.

References

• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.5.

theorem TauCeti.exists_isInjectiveEnvelope_finiteDimensional {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (M : Type w) [AddCommGroup M] [Module A M] [Module k M] [IsScalarTower k A M] [FiniteDimensional k M] : ∃ (Q : Type (max u v)) (x : AddCommGroup Q) (x_1 : Module A Q) (x_2 : Module k Q) (_ : IsScalarTower k A Q) (_ : FiniteDimensional k Q) (i : M →ₗ[A] Q), IsInjectiveEnvelope i

Every finite-dimensional module over a finite-dimensional algebra has an injective envelope which is finite-dimensional over the same field. The envelope can be taken in the universe of the field and algebra, independently of the universe of the original module.

theorem TauCeti.exists_isInjectiveEnvelope_of_finite {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (M : Type w) [AddCommGroup M] [Module A M] [Module.Finite A M] : ∃ (Q : Type (max u v)) (x : AddCommGroup Q) (x_1 : Module A Q) (x_2 : Module k Q) (_ : IsScalarTower k A Q) (_ : FiniteDimensional k Q) (i : M →ₗ[A] Q), IsInjectiveEnvelope i

Every finitely generated module over a finite-dimensional algebra has a finite-dimensional injective envelope. The field action on the source is induced through the algebra map.