Basic theorem on induction for representations of $p$-adic groups I know a lot of places where the following is sparsely proved, but I remember there was some paper where I read it in basically the same form I write it, but unfortunately I can't remember where it was.
Let $\mathcal{H}$ be the Hecke algebra of a reductive $p$-adic group, and $K$ be a compact open subgroup of $G$. There is a restriction functor $r : \mathcal{M}(\mathcal{H})\rightarrow \mathcal{M}(\mathcal{H}_K)$ defined by $r(V)=e_K V=V^K$  having the following properties.


*

*$r$ has a left adjoint, the induction functor $i: \mathcal{M}(\mathcal{H}_K)\rightarrow \mathcal{M}(\mathcal{H})$ (Frobenius reciprocity).

*$i$ carries admissible representations to admissible representations.

*The pair $(r,i)$ gives a bijection between $\mathcal{M}(\mathcal{H}_K)$ and the subcategory of $\mathcal{M}(\mathcal{H})$ of representations that are generated by $K$-fixed vectors.
 A: The general setting for your question is the theory of types as developped by Bushnell and Kutzko:
Smooth representations of reductive p-adic groups: structure theory via types. Proc. London Math. Soc. (3) 77 (1998), no. 3, 582–634.
First in order that your question make sense, let us clarify a few things.
$\bullet$ The good "induction functor" here is 
$$
i(M) = {\mathcal H}(G)\otimes_{{\mathcal  H}(K)} M
$$
where $M$ is a left ${\mathcal H}(K)$-module. Here you consider ${\mathcal H}(G)$ as a right ${\mathcal H}(K)$-module and left $G$-module. 
$\bullet$ It is false that $i$ takes "admissible modules" to "admissible modules". For instance if $M={\mathbb C}$ is the "trivial" character of ${\mathcal H}(K)$, then $i(M)$ is not admissible! Indeed if $L$ is a compact open subgroup of $G$, $i(M)^L$ is the space of $(L,K)$⁻bi-invariant functions on $G$ with finite support modulo $(L,K)$, an infinite dimensional space.
$\bullet$ You refer the pair $(r,i)$ as a "bijection". Of course you mean an equivalence of categories. This is false in general!
In order to get an equivalence of categories you need strong assumptions on $K$. As Peter McNamara writes, you need that $K$ have some nice "Iwahori decompositions". Typically a maximal compact subgroup of $G$ does not fulfill this condition. However this is true for a general reductive group $G$ and:
$\bullet$ $K=I$ an Iwahori subgroup of $G$ (Borel, Admissible representations of a semi-simple group over a local field with vectors fixed under an Iwahori subgroup. Invent. Math. 35 (1976), 233–259). 
$\bullet$ $K$ is a certain "congruence subgroup" ("le centre de Bernstein" in  Deligne, P.; Kazhdan, D.; Vignéras, M.-F. Représentations des algèbres centrales simples p-adiques. (French) [Representations of central simple p-adic algebras] Representations of reductive groups over a local field, 33–117, Travaux en Cours, Hermann, Paris, 1984. 
The aim of Bushnell and Kutzko's theory is to generalize this as follows. Instead of taking the trivial character of $K$, you fix an irreducible smooth representation $\rho$. You define an idempotent $e_\rho$ in ${\mathcal H}(G)$ such that $e_\rho V$ is the $\rho$-isotypic component $V^\rho$ of $V$, for all smooth $G$-modules $V$. You define the Hecke algebra of the pair $(K,\rho )$ by 
${\mathcal H}_\rho = e_\rho \star {\mathcal H}(G)\star e_\rho$. You have two functors between the category of $G$-modules $V$ generated by $V^\rho$ and the category of left ${\mathcal H}_\rho$-modules: $r(V)=V^\rho$, and $i(M) = {\mathcal H}(G)\otimes_{{\mathcal H}_\rho} M$. Then by definition $(K,\rho )$ is a type in $G$ if these functors define an equivalence of categories. 
Given an irreducible  representation $\pi$ of $G$, exhibiting a nice type $(K,\rho )$ such that $\pi_{\mid K}$ contains $\rho$ gives a lot of informations on $\pi$. 
A: The existence of the induction functor is general nonsense (tensor-hom adjunction).
When K is the Iwahori subgroup, Borel gives a direct proof in his paper on representations with Iwahori-fixed vectors. For general K, I see no easy way to prove this, but if you have the equivalence of categories from your third point (which is not true for all K), then this property follows since finite length is equivalent to admissible and finitely generated.
In general there is a bijection between irreps of HK and irreps of G with K-fixed vectors. In general there is not an equivalence of categories. e.g. Let K be hyperspecial and look at the reducible principal series.
If you assume K has an Iwahori factorisation w.r.t. a minimal parabolic, then there is an equivalence between HK-mod and the full subcategory of G-mod generated by K-fixed vectors. I don't know a reference in this generality. In the aforementioned paper of Borel, it is proved for the Iwahori. In Renard's book, there is a proof with the extra assumption that K is distinguished in a special maximal compact. In general, you can follow Borel's argument, using the version of Jacquet's lemma that doesn't require admissibility. I have some very rough notes on this on my hard drive that if I find the time or energy to polish, I can put online.
