Linear duality exchanges projective and injective modules

For an algebra A over a field k, linear duality sends projective right modules to injective left modules. Over a finite-dimensional algebra it also sends finite-dimensional injective right modules to projective left modules. These are the projective and injective terms used when dualizing finite module presentations.

For finite-dimensional right modules the converse also holds: the left dual is injective exactly when the original module is projective.

The left action on a dual is specified by a linear equivalence and the identity e (a • q) x = e q (op a • x). This follows the convention of TauCeti.LinearAlgebra.Dual.RightAction, avoiding a second global action on every linear dual. The statements allow independent universes for the field, algebra, and modules.

References

• M. Auslander, I. Reiten, S. Smalø, Representation Theory of Artin Algebras, Sections I.3 and I.5.

The projective-dual argument uses the existing injectivity of the dual regular module. The injective-dual argument generalizes the transposed free-presentation proof previously in TauCeti.Algebra.Module.Injective.FiniteDimensional.

theorem LinearEquiv.moduleInjective_of_dual_projective {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {N : Type w} [AddCommGroup N] [Module Aᵐᵒᵖ N] [Module k N] [IsScalarTower k Aᵐᵒᵖ N] {Q : Type z} [AddCommGroup Q] [Module A Q] [Module k Q] (e : Q ≃ₗ[k] Module.Dual k N) (he : ∀ (a : A) (q : Q) (x : N), (e (a • q)) x = (e q) (MulOpposite.op a • x)) [Module.Projective Aᵐᵒᵖ N] : Module.Injective A Q

The linear dual of a projective right module is an injective left module, with the action given by precomposition. The algebra need not be finite-dimensional.

theorem LinearEquiv.moduleProjective_of_dual_injective {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {N : Type w} [AddCommGroup N] [Module Aᵐᵒᵖ N] [Module k N] [IsScalarTower k Aᵐᵒᵖ N] {Q : Type z} [AddCommGroup Q] [Module A Q] [Module k Q] [FiniteDimensional k A] [FiniteDimensional k N] [Small.{w, v} Aᵐᵒᵖ] [Module.Injective Aᵐᵒᵖ N] (e : Q ≃ₗ[k] Module.Dual k N) (he : ∀ (a : A) (q : Q) (x : N), (e (a • q)) x = (e q) (MulOpposite.op a • x)) : Module.Projective A Q

Over a finite-dimensional algebra, the linear dual of a finite-dimensional injective right module is a projective left module, with the action given by precomposition.

theorem LinearEquiv.moduleInjective_iff_projective_of_dual {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {N : Type w} [AddCommGroup N] [Module Aᵐᵒᵖ N] [Module k N] [IsScalarTower k Aᵐᵒᵖ N] {Q : Type z} [AddCommGroup Q] [Module A Q] [Module k Q] [FiniteDimensional k A] [FiniteDimensional k N] [Small.{z, v} A] (e : Q ≃ₗ[k] Module.Dual k N) (he : ∀ (a : A) (q : Q) (x : N), (e (a • q)) x = (e q) (MulOpposite.op a • x)) : Module.Injective A Q ↔ Module.Projective Aᵐᵒᵖ N

Over a finite-dimensional algebra, a finite-dimensional right module is projective exactly when its left scalar dual is injective. The dual action is specified by the pairing.