linear_map.ker_eq_bot semiring?

Stream: maths

[Winston Yin]

Any reason why linear_map.ker_eq_bot uses ring R and add_comm_group M instead of semiring R and add_comm_monoid M like many of the other linear_map theorems? I only need the -> direction of this.

[Adam Topaz]

Just for the link since I'm on mobile: docs#linear_map.ker_eq_bot

[Adam Topaz]

Right, this is not true for semimodules over semirings

[Adam Topaz]

Take e.g. the semiring B = {0,1} where 1+1=1, and consider the projection from N to B sending every positive natural to 1

[Adam Topaz]

The kernel, i.e. the set of elements mapping to 0, is indeed 0, but the map is not injective