The dual of the regular module as a cogenerator #
For a finite-dimensional module M over an algebra A, its linear dual has a finite basis.
Evaluating the action of A against the coordinate functionals of that basis embeds M into a
finite power of the dual D(A_A) of the right regular module.
Main results #
LinearEquiv.exists_injective_linearMap_pi_of_dual: if a leftA-module is identified withD(A_A), every finite-dimensional leftA-module embeds into a finite power of it.
theorem
LinearEquiv.exists_injective_linearMap_pi_of_dual
{k : Type w}
[Field k]
{A : Type u}
[Ring A]
[Algebra k A]
{Q : Type u_1}
[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))
(M : Type u_2)
[AddCommGroup M]
[Module A M]
[Module k M]
[IsScalarTower k A M]
[FiniteDimensional k M]
:
∃ (n : ℕ) (f : M →ₗ[A] Fin n → Q), Function.Injective ⇑f
The dual of the right regular module is a cogenerator. Let A be an algebra over a field
k and Q a left A-module identified with Module.Dual k A by a k-linear equivalence carrying
the action of a to precomposition with right multiplication by a. Every finite-dimensional left
A-module embeds A-linearly into a finite power of Q.