Solution (source code)

= Solution

An <uncountable> cardinal $\kappa$ is a <measurable cardinal> if there is a nonprincipal $\kappa$-complete <ultrafilter> $U$ on $\kappa$: <intersections> of fewer than $\kappa$ members of $U$ remain in $U$. Such an <ultrafilter> is uniform. No <singleton> belongs to it, and intersecting the complements of fewer than $\kappa$ <singletons> shows that no <set> of <cardinality> below $\kappa$ belongs to it.

Form the <ultrapower> of the universe by $U$, with classes $[f]$ of <functions> $f:\kappa\to V$, and $[f]\in_U[g]$ exactly when $\{\xi:f(\xi)\in g(\xi)\}\in U$. The <Łoś theorem> proves that the map taking $x$ to the constant <function> with value $x$ is elementary. The <ultrapower> relation is well-founded: from an infinite descending <sequence> $[f_0]\ni_U[f_1]\ni_U\cdots$, <countable> completeness gives a coordinate satisfying all the membership relations, producing an actual infinite descending membership <sequence> and contradicting <foundation>. It is also set-like. Predecessors of $[g]$ can be represented by <functions> whose value at $\xi$ lies in $g(\xi)\cup\{\varnothing\}$; these <functions> form a <set>. The <Mostowski collapse theorem> therefore gives a <transitive class> $N$ and an <elementary embedding>
$$
j:V\longrightarrow N.
$$
The usual class-ultrapower notation is understood via set-sized representatives and this set-like collapse.

For $\alpha<\kappa$, any <function> into $\alpha$ is constant on a $U$-large <set>: if none of its fewer-than-$\kappa$ fibers belonged to $U$, intersect their complements to get the <empty set> in $U$. Consequently every member of the <ultrapower> <ordinal> represented by the constant $\alpha$ is represented by a constant <ordinal> below $\alpha$. Induction on $\alpha$ now gives $j(\alpha)=\alpha$.

On the other hand the identity <function> $d(\xi)=\xi$ represents an <ordinal> below $j(\kappa)$. For every $\alpha<\kappa$, the tail $\{\xi:\xi>\alpha\}$ belongs to $U$, so the collapsed <ordinal> $[d]$ is above $j(\alpha)=\alpha$. Hence
$$
\boxed{\operatorname{crit}(j)=\kappa,\qquad j(\kappa)>\kappa.}
$$
This proves nonidentity explicitly. The collapsed identity class is at least $\kappa$; it need not equal $\kappa$ unless an additional normality convention is imposed on $U$.

Conversely, an <elementary embedding> $j:V\to N$ into a <transitive class> with critical point $\kappa$ yields
$$
U=\{X\subseteq\kappa:\kappa\in j(X)\}.
$$
For the converse use the usual amenability assumption on the class embedding, so this collection is a <set>. Since $j(\kappa)>\kappa$, exactly one of $j(X)$ and $j(\kappa\setminus X)$ contains $\kappa$, proving the <ultrafilter> condition. <Singletons> are excluded because $j(\alpha)=\alpha<\kappa$. If $\lambda<\kappa$ and $X_i\in U$ for $i<\lambda$, then $j$ fixes $\lambda$ and every index below it, giving $j(\bigcap_{i<\lambda}X_i)=\bigcap_{i<\lambda}j(X_i)$; the <intersection> still contains $\kappa$. Thus $U$ is $\kappa$-complete and $\kappa$ is measurable.

In particular the first moved <ordinal> is a <strongly inaccessible cardinal>. If $\operatorname{cf}(\kappa)<\kappa$, partition $\kappa$ into fewer than $\kappa$ bounded intervals. Each is too small to lie in $U$, contradicting completeness. Thus $\kappa$ is regular. If $2^\lambda\ge\kappa$ for some $\lambda<\kappa$, choose distinct <subsets> $A_\xi\subseteq\lambda$ for $\xi<\kappa$. For each $\eta<\lambda$, choose the $U$-large side of the question $\eta\in A_\xi$. Intersect these fewer-than-$\kappa$ large sides. The <intersection> belongs to $U$, but all its indices have identical $A_\xi$, so it contains at most one index, contradicting nonprincipality. Therefore $2^\lambda<\kappa$ for every $\lambda<\kappa$, as required.