Ultrapower embedding (source code)

= Ultrapower embedding
{wiki=Ultraproduct}

An ultrafilter $U$ on $I$ gives an elementary map into the well-founded collapse of an ultrapower by sending $x$ to the class of the constant function with value $x$. For a $\kappa$-complete nonprincipal ultrafilter on $\kappa$, its critical point is $\kappa$.