Exactness of Hom into an injective module

A map into an injective module factors through f exactly when it vanishes on ker f. In particular, precomposition with f has image the kernel of restriction to ker f. This applies to presenting maps that are not monomorphisms, as occur in projective presentations over non-hereditary algebras. As a further consequence, an annihilator inclusion characterizes the existence of a linear map with one prescribed value.

theorem LinearMap.exists_comp_eq_iff_ker_le {R : Type u} [Ring R] {P : Type v} {Q : Type w} {I : Type t} [AddCommGroup P] [Module R P] [AddCommGroup Q] [Module R Q] [AddCommGroup I] [Module R I] [Small.{t, u} R] [Module.Injective R I] (f : P →ₗ[R] Q) (g : P →ₗ[R] I) : (∃ (h : Q →ₗ[R] I), h ∘ₗ f = g) ↔ f.ker ≤ g.ker

A map into an injective module factors through f exactly when it kills ker f.

theorem LinearMap.range_lcomp_eq_ker_lcomp_ker_subtype {R : Type u} [Ring R] {P : Type v} {Q : Type w} {I : Type t} [AddCommGroup P] [Module R P] [AddCommGroup Q] [Module R Q] [AddCommGroup I] [Module R I] [Small.{t, u} R] [Module.Injective R I] {k : Type s} [Semiring k] [Module k I] [SMulCommClass R k I] (f : P →ₗ[R] Q) : (lcomp k I f).range = (lcomp k I f.ker.subtype).ker

Precomposition into an injective module has image exactly the maps vanishing on the kernel of the original map. The Hom spaces are linear over a semiring whose action commutes with the module action.

theorem LinearMap.comap_range_lcomp_compRight {R : Type u} [Ring R] {P : Type v} {Q : Type w} {I : Type t} [AddCommGroup P] [Module R P] [AddCommGroup Q] [Module R Q] [AddCommGroup I] [Module R I] [Small.{t, u} R] [Module.Injective R I] {k : Type s} [Semiring k] [Module k I] [SMulCommClass R k I] {N : Type u_1} [AddCommGroup N] [Module R N] [Module k N] [SMulCommClass R k N] [CompatibleSMul N I k R] (f : P →ₗ[R] Q) (j : N →ₗ[R] I) (hj : Function.Injective ⇑j) : Submodule.comap (compRight k j) (lcomp k I f).range = (lcomp k N f.ker.subtype).ker

After embedding the coefficient module into an injective module, the inverse image of the precomposition range is exactly the maps vanishing on the original kernel.

theorem TauCeti.exists_linearMap_apply_eq_iff_forall_smul_eq_zero {S : Type u} [Ring S] {M : Type w} [AddCommGroup M] [Module S M] {Q : Type v} [AddCommGroup Q] [Module S Q] [Small.{v, u} S] [Module.Injective S Q] {a : M} {x : Q} : (∃ (f : M →ₗ[S] Q), f a = x) ↔ ∀ (s : S), s • a = 0 → s • x = 0

A linear map into an injective module can send a to x exactly when every scalar killing a also kills x.