Minimal model of ZF with $0\sharp$ We know that the constructible universe $L$ is an absolute and minimal model of ZF (every standard model of ZF contains "an" $L$, and it is actually the same $L$ for all of them).
It is also my understanding that the existence of $0\sharp$ informally means that $V$ is much "bigger" than $L$ (meaning that if $0\sharp$ exists then even $\aleph_1$ is already an inaccessible cardinal in $L$) and that a sort of converse is true (see: https://en.wikipedia.org/wiki/Jensen%27s_covering_theorem).
Therefore my question is: Is there an absolute minimal model of ZF + $\exists0\sharp$ ?
A sort of "$L\sharp$" if we really want to abuse notation?
 A: Yes, the minimal such model is $L[0^\sharp]$. This model can be built by stages, just as $L$, starting with the empty set, taking unions at limit stages, and at each successor stage $\alpha+1$ taking the collection of subsets of $L_\alpha[0^\sharp]$ definable in $(L_\alpha[0^\sharp],\in,0^\sharp)$ from parameters. Here, $0^\sharp$ can be thought of as a set of natural numbers, and definability is in the language of set theory with one additional predicate.
Note that for each finite $n$, $L_n[0^\sharp]=L_n$ (that is, the universes of both structures coincide) and so $L_\omega[0^\sharp]=L_\omega$. However, $0^\sharp$ is now definable at this stage (as the set of numbers satisfying the new predicate), so $0^\sharp\in L[0^\sharp]$. 
This is not quite enough. Let $\varphi(x)$ be the formula in the language of set theory stating that $x$ is $0^\sharp$, i.e., stating that $x$ is the unique EM blueprint satisfying the three indiscernibility conditions listed in section 9 of 

MR1994835 (2004f:03092) Kanamori, Akihiro. The higher infinite. Large cardinals in set theory from their beginnings. Second edition. Springer Monographs in Mathematics. Springer-Verlag, Berlin, 2003. xxii+536 pp. ISBN: 3-540-00384-3.

One should also check that $L[0^\sharp]\models \varphi(0^\sharp)$, and that whenever $M$ is an inner model and $M\models\varphi(a)$ for some $a$, then $0^\sharp$ exists in $V$ and $a=0^\sharp$, so that $L[0^\sharp]\subseteq M$. This is essentially an absoluteness argument, but it is a bit technical so I will skip the details here. The point of proving this is that not only is $L[0^\sharp]$ the smallest such model, but it knows it, in the sense that it satisfies $L[0^\sharp]\models V=L[0^\sharp]$, and is contained in any inner model that believes in the existence of $0^\sharp$. 
One can prove more as well, for instance, $L[0^\sharp]$ satisfies appropriate analogues of the fine structural properties of $L$, so it is not just the least model containing $0^\sharp$, it is also a very well-behaved model. Naturally, the construction generalizes to more general sharps and other inner-model theoretic objects, although the absoluteness requirements become more involved.
