The dual regular module is injective #
For an algebra A over a field k, the dual of the right regular module is an injective
left A-module. Together with its cogenerator property, this provides injective modules
containing finite-dimensional modules, without a self-injectivity assumption on the algebra.
The action on the dual is specified through an equivariant linear equivalence, rather than
installed as a global instance on all duals. This follows the convention of
TauCeti.LinearAlgebra.Dual.RightAction.
References #
- I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.5.
theorem
TauCeti.moduleInjective_of_equiv_dual_regular
(k : Type u_1)
{A : Type u_2}
{Q : Type u_3}
[Field k]
[Ring A]
[Algebra k A]
[AddCommGroup Q]
[Module A Q]
[Module k Q]
(e : Q ≃ₗ[k] Module.Dual k A)
(he : ∀ (a : A) (q : Q) (x : A), (e (a • q)) x = (e q) (x * a))
:
Module.Injective A Q
The dual of the right regular module, with action (a • φ) x = φ (x * a), is an
injective left module over any algebra over a field.