I am a little bit confused about the basic theory of overconvergent modular forms, so here are a few questions that I think will be straightforward for those who know the theory but would help me a lot. A lot of my questions are about reconciling various definitions and claims in the classic papers of Coleman, Coleman--Mazur, Katz, and Chenevier. (1) Without any $p$ in the level, the theory is simplest: everyone agrees that for $0 \leq v < \frac{p}{p+1}$, the overconvergent locus $Z_1(N)(v)$ that is relevant for defining $v$-overconvergent modular forms of level $\Gamma_1(N)$ is just the affinoid subdomain of $X_1(N)$ defined by $v(E_{p-1}) \leq v$. What is the full justification for why $M_k^\dagger(N, v) := H^0(Z_1(N)(v), \omega^k)$ is the same as Katz's space of overconvergent forms defined as rules on the usual tuples of data ? It is supposed to be a direct consequence of rigid GAGA ? When you start to increase the power of $p$ in the level, the various sources seem to use different definitions of the overconvergent loci on which the overconvergent modular forms are defined. Question (2) is just asking why the definitions agree (for convenience I will summarize the definitions), and question (3) is asking why it is a reasonable definition: (2) In Coleman's papers (e.g. section B.2 of the "Banach spaces and families of modular forms" paper, which is also what Coleman--Mazur cites), if $0 \leq v < p^{2-m}/(p+1)$, the definition of the $v$-overconvergent locus in $X_1(Np^m)$ is a little bit complicated: you need to enforce the condition $v(E_{p-1}) \leq v$ as usual, but then you also add some conditions related to the level structure, as follows. For a given point $x$ representing the data $(E, \alpha_N, \alpha_p)$ [the level structure at $p$ being $\alpha_p : \mu_{p^m} \to E[p^\infty]$], in order to include $x$ in the $v$-overconvergent locus, Coleman asks that the image of $\alpha_p|_{\mu_p}$ is the canonical subgroup of order $p$, and that the image of $\alpha_p|_{\mu_{p^{m-1}}}$ is the canonical subgroup of order $p^{m-1}$ (at least this is my interpretation of what is going on in section B.2). On the other hand, in Chenevier's paper "une correspondence Jacquet--Langlands p-adique" (see section 3.1 of the arxiv version https://arxiv.org/abs/math/0301032), it is simply defined to be the connected component of $\infty$ in the locus where $v(E_{p-1}) \leq v$. Why are these definitions the same ? Is the point that $X_1(Np^m)$ itself might not be connected, or is the point that removing the too supersingular discs makes it disconnected ? (3) I know that (at least in the parts I have read), Katz in his famous Antwerp paper doesn't really discuss overconvergent modular forms with $p$ in the level. If the answer to (1) is just that it is a direct consequence of rigid GAGA, I would imagine that if you defined the overconvergent forms of high level at $p$ in the same way that Katz does those of level $N$, then you DO NOT get the same thing as with the definitions of Coleman and Coleman--Mazur and Chenevier (due to the extra step of taking connected component of $\infty$). So why is the definition in (2) the correct definition ? Is it just that you need this for the $q$-expansion principle to work ? Is it just because we need the main fact of the next (and final) question (4) to be true ? Finally, one last question about what seems to be one of the main points of the theory: (4) In Chenevier's paper (also in section 3.1 of the arxiv version), there is a claim that (for $v$ in the range where the canonical subgroup of order $p^m$ exists, as usual) $Z_1(Np^m)(v)$ can be canonically identified with the quotient of $Z_1(Np)(v)$ by the relevant diamond operators. This is very important, since it is the reason that in the theory of $p$-adic modular forms we consider all levels at $p$ at a time, compressing all of that information (including the Nebentypus at $p$) into the weight-character. Anyway, is this really 100 percent obvious from the definitions in (2) ? It seems to me that we are slightly off, due to the fact that Coleman's definition in (2) doesn't ask for the image of the level-$p^m$ level structure to be the full canonical subgroup of order $p^m$ (only for $p^{m-1}$) --- so the fibers of the map $Z_1(p^m)(v) \to X_1(p)(v)$ are bigger than claimed, as they include all sorts of ways to extend the level structure from $\mu_{p^{m-1}}$ to $\mu_{p^m}$. Have I just made a silly mistake somewhere here ? Sorry for the long question. I welcome any partial answers to any of the four questions, of course.