Solution (source code)

= Solution

The <critical point of an elementary embedding> $j$ is the least <ordinal> $\alpha$ for which $j(\alpha)\ne\alpha$.

We first prove by <transfinite induction> that $j(\alpha)=\alpha$ for every $\alpha<\kappa$. Suppose this is known below $\alpha<\kappa$. If $[f]\mathrel E[\operatorname{const}_\alpha]$, then
$$
A=\{\xi<\kappa:f(\xi)<\alpha\}\in U.
$$
The sets $A_\beta=\{\xi\in A:f(\xi)=\beta\}$ for $\beta<\alpha$ partition $A$ into fewer than $\kappa$ pieces. A <kappa-complete filter> that is an <ultrafilter> must contain one cell $A_\beta$: otherwise all their complements would belong to $U$, and their intersection would contradict $A\in U$. Hence $[f]=[\operatorname{const}_\beta]$. The predecessors of $j(\alpha)$ are consequently exactly the already-fixed ordinals below $\alpha$, so $j(\alpha)=\alpha$.

Now let $\operatorname{id}(\xi)=\xi$. An identical argument shows that the predecessors of $[\operatorname{id}]$ in the ultrapower are exactly $[\operatorname{const}_\beta]$ for $\beta<\kappa$, so
$$
\pi([\operatorname{id}])=\kappa.
$$
Since $\{\xi<\kappa:\xi<\kappa\}=\kappa\in U$, one has $[\operatorname{id}]\mathrel E[\operatorname{const}_\kappa]$. After collapsing, $\kappa\in j(\kappa)$, and therefore $j(\kappa)>\kappa$. Thus $\operatorname{crit}(j)=\kappa$.