Endomorphisms under left–right linear duality

Let N be a right module and identify a left module Q with its scalar dual, with the action given by precomposition. Transposition gives a ring homomorphism from the opposite endomorphism ring of N to the endomorphism ring of Q. When N is reflexive over the base, this is a ring equivalence. In particular, finite-dimensional linear duality preserves the idempotents that detect decompositions of modules.

The action is specified through an equivariant linear identification, so these constructions apply to a dual carrying a chosen action without introducing competing global instances. The inverse equivalence is characterized by the same evaluation pairing as transposition.

References

• M. Auslander, I. Reiten, S. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Section I.3.

def LinearEquiv.dualEndRingHom {k : Type u} [CommSemiring k] {A : Type v} [Semiring A] [Algebra k A] {N : Type w} [AddCommMonoid N] [Module Aᵐᵒᵖ N] [Module k N] [IsScalarTower k Aᵐᵒᵖ N] {Q : Type z} [AddCommMonoid 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.End Aᵐᵒᵖ N)ᵐᵒᵖ →+* Module.End A Q

Transposition along an equivariant identification with the scalar dual reverses multiplication of endomorphisms. No reflexivity assumption is needed for this map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearEquiv.dualEndRingHom_apply_apply {k : Type u} [CommSemiring k] {A : Type v} [Semiring A] [Algebra k A] {N : Type w} [AddCommMonoid N] [Module Aᵐᵒᵖ N] [Module k N] [IsScalarTower k Aᵐᵒᵖ N] {Q : Type z} [AddCommMonoid 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)) (f : (Module.End Aᵐᵒᵖ N)ᵐᵒᵖ) (q : Q) (x : N) : (e (((e.dualEndRingHom he) f) q)) x = (e q) ((MulOpposite.unop f) x)

Transposition is precomposition, expressed through the identifying pairing.

theorem LinearEquiv.dualEndRingHom_bijective {k : Type u} [CommSemiring k] {A : Type v} [Semiring A] [Algebra k A] {N : Type w} [AddCommMonoid N] [Module Aᵐᵒᵖ N] [Module k N] [IsScalarTower k Aᵐᵒᵖ N] {Q : Type z} [AddCommMonoid Q] [Module A Q] [Module k Q] [Module.IsReflexive k 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)) : Function.Bijective ⇑(e.dualEndRingHom he)

Over a reflexive scalar module, every endomorphism of the left dual is the transpose of a unique right-module endomorphism.

noncomputable def LinearEquiv.dualEndRingEquiv {k : Type u} [CommSemiring k] {A : Type v} [Semiring A] [Algebra k A] {N : Type w} [AddCommMonoid N] [Module Aᵐᵒᵖ N] [Module k N] [IsScalarTower k Aᵐᵒᵖ N] {Q : Type z} [AddCommMonoid Q] [Module A Q] [Module k Q] [Module.IsReflexive k 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.End Aᵐᵒᵖ N)ᵐᵒᵖ ≃+* Module.End A Q

Linear duality identifies the endomorphism ring of a reflexive right module, with multiplication reversed, with the endomorphism ring of its left dual.

Equations

• e.dualEndRingEquiv he = RingEquiv.ofBijective (e.dualEndRingHom he) ⋯

@[simp]

theorem LinearEquiv.dualEndRingEquiv_apply_apply {k : Type u} [CommSemiring k] {A : Type v} [Semiring A] [Algebra k A] {N : Type w} [AddCommMonoid N] [Module Aᵐᵒᵖ N] [Module k N] [IsScalarTower k Aᵐᵒᵖ N] {Q : Type z} [AddCommMonoid Q] [Module A Q] [Module k Q] [Module.IsReflexive k 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)) (f : (Module.End Aᵐᵒᵖ N)ᵐᵒᵖ) (q : Q) (x : N) : (e (((e.dualEndRingEquiv he) f) q)) x = (e q) ((MulOpposite.unop f) x)

The endomorphism-ring equivalence acts by precomposition on the pairing.

@[simp]

theorem LinearEquiv.dualEndRingEquiv_symm_apply_apply {k : Type u} [CommSemiring k] {A : Type v} [Semiring A] [Algebra k A] {N : Type w} [AddCommMonoid N] [Module Aᵐᵒᵖ N] [Module k N] [IsScalarTower k Aᵐᵒᵖ N] {Q : Type z} [AddCommMonoid Q] [Module A Q] [Module k Q] [Module.IsReflexive k 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)) (g : Module.End A Q) (q : Q) (x : N) : (e q) ((MulOpposite.unop ((e.dualEndRingEquiv he).symm g)) x) = (e (g q)) x

The inverse transposition is characterized by moving the endomorphism across the evaluation pairing.