$A^\#$ and inner models For a set of ordinals $A$ we say that $A^\#$ exists if there exists a closed and unbounded class of indiscernibles, $I\subseteq\operatorname{Ord}$, for $L[A]$. Formally, if such class exists we define $A^\#=\{\varphi\mid L_{i_\omega}[A]\models\varphi(i_1,\ldots,i_n)\}$, where $\varphi$ is a formula in the language $\{\in,A\}$. If we consider the Godel encoding of $\varphi$ we can think of $A^\#$ as a subset of $\omega$ or as a real number.
Suppose $V$ is a model of $ZFC$, $A$ a set of ordinals and $M$ is a transitive inner model such that $A\in M$ and $M\models A^\#\text{ exists}$.
Does that imply $V\models A^\#\text{ exists}$? What about the other direction (i.e. $A^\#$ exists in $V$, and $A\in M$)?
My intuition says the answer is yes in both cases, but my intuition was completely obliterated and needs to be rebuilt.
 A: One can use the class of indiscernibles to generate elementary embeddings of $L[A]$ to itself with critical point above the supremum of $A$, in much the same way as the indiscernibles of $L$ give us embeddings of $L$ into itself. 
By results of Kunen (for $L$, but they generalize straightforwardly), the existence of an embedding $j:L[A]\to L[A]$ that has critical point above the supremum of $A$ implies the existence of $A^\sharp$, so both statements are equivalent.
So, suppose $M$ is an inner model and $M$ thinks that $A^\sharp$ exists. Then $M$ sees an elementary embedding of $L[A]$ into itself. This is clearly seen in $V$ as well. So $A^\sharp$ exists in $V$. The converse does not hold. After all, $L[A]$ sees $A$ but never $A^\sharp$. (However, if $M$ is an inner model that thinks that $A^\sharp$ exists, then $A^\sharp$ exists and coincides with $M$'s idea of it. This can be seen descriptive set theoretically (see below), or using the Kunen characterization. Also, if $A^\sharp$ belongs to $M$, then $M$ thinks that $A^\sharp$ exists, because from the sharp one can easily produce an $L[A]$-normal measure on the indiscernible $i_0$, and one can use this to recover the elementary embeddings.)
There is a better way of thinking about sharps, though, namely in terms of mice. This is probably folklore by now, but a nice reference is Schimmerling's "The ABC's of mice", Bulletin of Symbolic Logic 7 (2001) 485-503.
A sharp is then a model of the form $M=(L_\alpha[A],\in,A,U)$ where $U$ is an (external) measure on some $L_\alpha[A]$ cardinal $\kappa$. We add certain requirements that depend on your fine structural taste (say, $\alpha=\kappa^{++}$ in the sense of $L_\alpha[A]$), $M$ has the same size as $A$ and is sound and iterable. Soundness is a technical condition which essentially ensures $M$ is as small as possible. 
Iterability is more complicated but it means that (as you imagine) iterating the process of forming ultrapowers by $U$ and its images only produces well-founded models. All the conditions describing the mouse $A^\sharp$ except for iterability are clearly absolute between inner models and $V$. 
Iterability is as well, but this requires an argument. But then absoluteness gives us a positive answer to your question. (This means that if an inner model thinks that the mouse $A^\sharp$ exists, then it does in $V$, and if $A^\sharp$ exists and belongs to an inner model, then the inner model knows that it is $A^\sharp$.)
Consider first the case where $A$ is a subset of $\omega$. Then if one iterates $M$ some countable ordinal number of times, the whole iteration is codable by reals, and we can see that the statement that a real $x$ coding a model is iterable is $\Pi^1_2(x)$ (you basically have to say: every real coding an iteration of $x$ gives a well-founded model). The point is that if some iterate of $x$ is ill-founded, then some countable iterate is ill-founded, so you only need to describe iterations "accessible" by reals. 
Finally, if $A$ is not a real, we can pretend that it is by working on a collapse of a sufficiently large initial segment of the universe to verify absoluteness. Or we can form the tree of attempts to build $A^\sharp$ and check that if $M$ thinks that $A^\sharp$ exists, then the tree is ill-founded, so $A^\sharp$ exists in $V$, and if $A^\sharp$ is in $M$, hen $M$ has a witness to the ill-foundedness of the tree. You can see a more detailed sketch of that idea in my paper with Schindler, "Projective well-orderings of the reals", Archive for Mathematical Logic 45 (7) (2006), 783-793, available at my page.
(Of course, one can also go as Jech does and verify the absoluteness of sharps in terms of blueprints, but I prefer the two other approaches I sketched.)
