We really need two kinds of Sym^k distribution modules: exact ones (which are typically over QQ and have no notion of approximation modules, and are the right domain for "lift"); and inexact ones (which must be defined over a p-adic field, have a good notion of approximation modules, and are the right codomain for "specialize").
We really need two kinds of Sym^k distribution modules: exact ones (which are typically over QQ and have no notion of approximation modules, and are the right domain for "lift"); and inexact ones (which must be defined over a p-adic field, have a good notion of approximation modules, and are the right codomain for "specialize").