names of inclusion maps

Stream: general

[Johan Commelin]

Given a bundled structure (say submodules) there are two types of inclusion maps:
If N : submodule M, then there is a natural inclusion N →l M (where N is coerced to a type).
If N₁ < N₂, then there is a natural inclusion N₁ →l N₂ (where both are coerced to a type).

How should we call these two types of maps?

This also shows up for subgroups, sub-lie-algebra, sub-algebras, subrings, sub-whatevers. So it's useful to fix some sort of convention now.