Hom(N,M) is subsingleton iff there exists a smul regular element of M in ann(N)

Let M and N be R-modules. In this section we prove that Hom(N,M) is subsingleton iff there exist r : R, such that IsSMulRegular M r and r ∈ ann(N). This is the case if Depth[I](M) = 0.

Main Results

• IsSMulRegular.subsingleton_linearMap_iff : for R module N M, Hom(N, M) = 0 iff there is a M-regular in Module.annihilator R N.

theorem IsSMulRegular.linearMap_subsingleton_of_mem_annihilator {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {r : R} (reg : IsSMulRegular M r) (mem_ann : r ∈ Module.annihilator R N) : Subsingleton (N →ₗ[R] M)

theorem IsSMulRegular.subsingleton_linearMap_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [IsNoetherianRing R] [Module.Finite R M] [Module.Finite R N] : Subsingleton (N →ₗ[R] M) ↔ ∃ r ∈ Module.annihilator R N, IsSMulRegular M r