Retracts of injective modules

A retract of an injective module in the same universe is injective, straight from the class Module.Injective.

Main results

• Module.Injective.of_leftInverse: a retract of an injective module of the same universe is injective.

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

Injective modules are closed under retracts. If M admits a split inclusion into an injective module Q of the same universe, then M is injective.