Preimage/inverse image of finite maps

It would be nice to have some theory for taking inverse images of finite maps. For example, if I have a map m : gmap nat string, then I want to obtain an inverse m^-1 : gmap string (gset nat) such that

m^-1 !! s = Some X ↔ (∀ x, x ∈ X ↔ m !! x = Some s)