Ytukyg

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 $0sharp$ informally means that $V$ is much "bigger" than $L$ (meaning that if $0sharp$ 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 + $exists0sharp$ ?
A sort of "$Lsharp$" if we really want to abuse notation?

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^sharpin 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 $Mmodelsvarphi(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.