Induced representation: which adjoint is it? I'm having trouble understanding on which side the induced representation functor is adjoint to the restriction functor.
For simplicity I'm assuming $H$ is a subgroup of $G$ (we could also see it as a morphism $H\to G$). Let me denote $\mathbf{Rep}_H$ the category of representations of $H$ over a fixed field $K$ (similarly for $G$), let $\mathbf{Res}_H^G: \mathbf{Rep}_G \to \mathbf{Rep}_H$ be the restriction functor.
One usual description of the induced representation is the following: given $(\rho,V)$ a representation of $H$, let $\mathbf{Ind}_H^G\rho = \{f: G\to V \mid \forall h\in H, \forall x\in G, f(hx)=h\cdot f(x)\}$ with $g\cdot f(x) =f(xg)$.
With this definition it's easy to prove $\operatorname{Hom}_G(\pi, \mathbf{Ind}_H^G\rho)\simeq \operatorname{Hom}_H(\mathbf{Res}_H^G\pi, \rho)$, which makes $\mathbf{Ind}_H^G$ right-adjoint to $\mathbf{Res}_H^G$. If I'm not mistaken, the explicit arrows are $\lambda\mapsto (v\mapsto \lambda(v)(1))$ and in the reverse direction $f\mapsto (v\mapsto (g\mapsto f(g\cdot v)))$.
First of all this is a bit surprising as $\mathbf{Res}_H^G$ is more of a forgetful-type functor so we'd expect the "obvious functor in the other direction" to be its left adjoint, but as the proof goes through so simply we can let this surprise on the side.
However, Wiki states the following : "In the case of finite groups, they are actually both left- and right-adjoint to one another" (from the article on Frobenius Reciprocity)
Moreover in the same article they state that there is a natural isomorphism $\operatorname{Hom}_{K[G]}(K[G]\otimes_{K[H]}V, W) \simeq \operatorname{Hom}_{K[H]}(V,W)$ where a representation is simply seen as a $K[G]$(resp. $K[H]$-)module  (and $K[G]$ is a $(K[G],K[H])$-bimodule to make sense of the tensor product and the $K[G]$-module structure on it). Once again, this isomorphism seems easy to establish : one direction is $\lambda\mapsto (v\mapsto \lambda(1\otimes v))$ and the other $f\mapsto (g\otimes v\mapsto g\cdot f(v))$.
This seems to work for arbitrary groups, not just finite ones. So I assume the sentence in the wikipedia article means that $K[G]\otimes_{K[H]}V \simeq \mathbf{Ind}_H^GV$ only if $G$ is finite (the "only" being in the sense "in general").

If that's not the case, what does this sentence mean ? If it is, is this isomorphism natural (in $V$ ? and in $(H,G)\in \mathbf{FinGrp}^\to$ ?) ? What is the isomorphism? If my interpretation is correct, can anything be said on the relationship between $K[G]\otimes_{K[H]}V$ and $\mathbf{Ind}_H^GV$ when $G$ is infinite ?


If my interpretation is not correct and the "$K[G]\otimes_{K[H]}V$" construction does not work for infinite $G$ (because of some mistake I made), then does $\mathbf{Res}_H^G$ have a left adjoint in general ?

It seems as though one can apply the general adjoint functor theorem to prove that it does, the only bit I'm not sure about being the fact that it preserves limits... But I think it preserves products and equalizers so it should suffice, right ?

If this is correct, and still working under the assumption that my interpretation isn't correct, can the aforementioned left adjoint be explicited? Does it have anything to do with $\mathbf{Ind}_H^G$ ? with $K[G]\otimes_{K[H]}-$ ?

Any correction of anything I said, besides the explicit questions, is very welcome as well as an answer to the questions !
 A: Let $f : R \to S$ be a ring homomorphism, which in this special case is a homomorphism of group rings $k[H] \to k[G]$ induced by a homomorphism of groups. $f$ induces a restriction of scalars functor between categories of left modules
$$f^{\ast} : \text{Mod}(S) \to \text{Mod}(R)$$
which has both a left and a right adjoint. The left adjoint is called extension of scalars and looks like
$$f_L : \text{Mod}(R) \ni M \mapsto S \otimes_R M \in \text{Mod}(S)$$
and the right adjoint doesn't have a common name that I'm aware of, but we could call it coextension of scalars, and it looks like
$$f_R : \text{Mod}(R) \ni M \mapsto \text{Hom}_R(S, M) \in \text{Mod}(S).$$
Now, I claim that if $G$ and $H$ are finite groups, then these functors are naturally isomorphic, meaning induction is both left and right adjoint to restriction in this case. But in general they're not. Which one deserves to be called "induction" and which one deserves to be called "coinduction" is a question I haven't settled to my own satisfaction. The second one seems to generalize more cleanly to the setting where $G$ and $H$ are groups with extra structure, e.g. algebraic groups; IIRC it can be interpreted as computing the space of sections of a $G$-equivariant vector bundle on the quotient $G/H$. 
