Self-injective algebras

A ring is self-injective when its regular left module is injective, Module.Injective A A. This file proves the criterion producing the examples which come from a Frobenius structure: an algebra over a field carrying an associative perfect bilinear form is self-injective.

The form is a k-bilinear B : A →ₗ[k] A →ₗ[k] k which is associative, B (x * y) z = B x (y * z), and perfect in the sense of LinearMap.IsPerfPair. Associativity already forces B x y = B 1 (x * y), so the form is multiplication followed by the linear functional B 1, the Frobenius trace; perfectness is nondegeneracy in the strong form which also makes every functional on A of the shape B · a.

Two general facts about Baer modules are proved along the way and stated in Mathlib's Module.Baer namespace, which has neither. A retract of a Baer module is Baer (Module.Baer.of_leftInverse), and consequently the left ideal cut out by an idempotent is Baer over a self-injective ring (Module.Baer.of_isIdempotentElem): over a self-injective ring the principal projective modules are injective. More generally, every finitely generated projective module over a self-injective ring is injective (Module.Injective.of_finite_projective). The two Baer facts are stated for Module.Baer rather than Module.Injective because the two convert freely in one direction only, Module.Baer.of_injective costing a smallness hypothesis on the ring.

Main results

• Function.Bijective.moduleBaer_self and Function.Bijective.moduleInjective_self: an algebra over a field carrying an associative bilinear form whose flip is bijective is self-injective.
• Module.Baer.of_leftInverse: a retract of a Baer module is Baer.
• Module.Baer.of_isIdempotentElem: over a self-injective ring, a left ideal consisting of the elements fixed by right multiplication by an idempotent is Baer.
• Module.Injective.of_finite_projective: every finitely generated projective module over a self-injective ring is injective.

References

See Curtis--Reiner, Methods of representation theory I, Section 9, and Lam, Lectures on modules and rings, Sections 3 and 16, for Frobenius algebras and self-injectivity.

Retracts and idempotent corners of a Baer module

theorem Module.Baer.of_leftInverse {R : Type u} [Ring R] {Q : Type v} [AddCommGroup Q] [Module R Q] {M : Type w} [AddCommGroup M] [Module R M] (hQ : Baer R Q) (s : M →ₗ[R] Q) (r : Q →ₗ[R] M) (hrs : ∀ (m : M), r (s m) = m) : Baer R M

Baer modules are closed under retracts. If M admits a split inclusion into a Baer module Q, then M is Baer. In particular, this criterion applies to projective summands of a self-injective regular module.

theorem Module.Baer.of_isIdempotentElem {A : Type u} [Ring A] (hA : Baer A A) {e : A} (he : IsIdempotentElem e) {p : Ideal A} (hp : ∀ (x : A), x ∈ p ↔ x * e = x) : Baer A ↥p

Over a self-injective ring the principal projective modules are injective, in Baer's form: if the regular module is Baer then so is a left ideal p consisting of the elements fixed by right multiplication by an idempotent e, such a p being a retract of the regular module by right multiplication by e. For p = Ideal.span {e} the hypothesis hp is TauCeti.mem_span_singleton_iff_mul_eq_self.

Finite projective modules over a self-injective ring

theorem Module.Injective.of_finite_projective {R : Type u} [Ring R] {P : Type v} [AddCommGroup P] [Module R P] (hR : Injective R R) [Module.Finite R P] [Projective R P] : Injective R P

A finitely generated projective module over a self-injective ring is injective.

Self-injectivity from an associative perfect form

theorem Function.Bijective.moduleBaer_self {k : Type w} [Field k] {A : Type u} [Ring A] [Algebra k A] {B : A →ₗ[k] A →ₗ[k] k} (hB : Bijective ⇑B.flip) (hassoc : ∀ (x y z : A), (B (x * y)) z = (B x) (y * z)) : Module.Baer A A

An algebra over a field carrying an associative bilinear form whose flip is bijective is self-injective, in Baer's form: every linear map from a left ideal to the regular module extends to the algebra.

theorem Function.Bijective.moduleInjective_self {k : Type w} [Field k] {A : Type u} [Ring A] [Algebra k A] {B : A →ₗ[k] A →ₗ[k] k} (hB : Bijective ⇑B.flip) (hassoc : ∀ (x y z : A), (B (x * y)) z = (B x) (y * z)) : Module.Injective A A

An algebra over a field carrying an associative bilinear form whose flip is bijective is self-injective: its regular left module is an injective module.