[proofplan] Starting from a $\lambda$-supercompactness embedding $j:V \to M$, we define the ultrafilter by testing whether the seed $j``\lambda$ belongs to $j(A)$. Elementarity gives ultrafilterhood and $\kappa$-completeness, while fineness and normality are exactly the consequences of evaluating at the seed. Conversely, from a fine normal $\kappa$-complete ultrafilter $U$ on $P_\kappa(\lambda)$, we form the ultrapower of $V$ by $U$, collapse it to a transitive class, and analyze the canonical seed $[\operatorname{id}]_U$. Fineness gives $j``\lambda \subset [\operatorname{id}]_U$, normality gives the reverse inclusion, and this seed representation yields both $j(\kappa)>\lambda$ and closure of the ultrapower under $\lambda$-sequences. [/proofplan] [step:Construct the fine normal measure from a supercompactness embedding] Assume $\kappa$ is $\lambda$-supercompact. Fix an elementary embedding $j:V \to M$ into a transitive class $M$ such that $\operatorname{crit}(j)=\kappa$, $j(\kappa)>\lambda$, and $M^\lambda \subset M$. Define the seed $s := j``\lambda = \{j(\alpha):\alpha<\lambda\}$. Since the map $\alpha \mapsto j(\alpha)$ for $\alpha<\lambda$ is a $\lambda$-sequence of elements of $M$, the closure hypothesis $M^\lambda \subset M$ gives $s \in M$. Also $s \subset j(\lambda)$ and, in $M$, the set $s$ has cardinality $\lambda < j(\kappa)$. Hence \begin{align*} s \in P_{j(\kappa)}(j(\lambda)). \end{align*} Define $U \subset \mathcal{P}(P_\kappa(\lambda))$ by \begin{align*} U := \{A \subset P_\kappa(\lambda): s \in j(A)\}. \end{align*} For every $A \subset P_\kappa(\lambda)$, elementarity gives \begin{align*} j(P_\kappa(\lambda) \setminus A)=P_{j(\kappa)}(j(\lambda)) \setminus j(A). \end{align*} Since $s \in P_{j(\kappa)}(j(\lambda))$, exactly one of $s \in j(A)$ and $s \in j(P_\kappa(\lambda)\setminus A)$ holds. Therefore $U$ is an ultrafilter on $P_\kappa(\lambda)$. To prove $\kappa$-completeness, let $\delta<\kappa$ be an ordinal and let $(A_i)_{i<\delta}$ be a family of members of $U$. Since $\delta<\operatorname{crit}(j)$, we have $j(\delta)=\delta$ and \begin{align*} j\left(\bigcap_{i<\delta} A_i\right)=\bigcap_{i<\delta}j(A_i). \end{align*} For each $i<\delta$, $A_i \in U$, so $s \in j(A_i)$. Hence $s$ belongs to the displayed intersection, and therefore $\bigcap_{i<\delta}A_i \in U$. For fineness, fix $\alpha<\lambda$ and define \begin{align*} X_\alpha := \{x \in P_\kappa(\lambda): \alpha \in x\}. \end{align*} Then \begin{align*} j(X_\alpha)=\{y \in P_{j(\kappa)}(j(\lambda)): j(\alpha)\in y\}. \end{align*} Since $j(\alpha)\in s$, we have $s\in j(X_\alpha)$, so $X_\alpha\in U$. For normality, let $S \in U$ and let $f:S \to \lambda$ be a regressive map in the sense that $f(x)\in x$ for every $x\in S$. Since $s\in j(S)$, elementarity gives \begin{align*} j(f)(s)\in s. \end{align*} Thus there is an $\alpha<\lambda$ such that $j(f)(s)=j(\alpha)$. Define \begin{align*} S_\alpha := \{x\in S:f(x)=\alpha\}. \end{align*} Then $s\in j(S_\alpha)$, so $S_\alpha\in U$. This is normality. Finally, $U$ is nonprincipal. If $x_0\in P_\kappa(\lambda)$, choose $\alpha\in\lambda\setminus x_0$, possible because $|x_0|<\kappa\leq\lambda$. The fine set $X_\alpha=\{x\in P_\kappa(\lambda):\alpha\in x\}$ belongs to $U$ and is disjoint from $\{x_0\}$. Hence $\{x_0\}\notin U$. [/step] [step:Form the well founded ultrapower from the measure] Conversely, assume $U$ is a nonprincipal fine normal $\kappa$-complete ultrafilter on $P_\kappa(\lambda)$. Put $X:=P_\kappa(\lambda)$. Let $\operatorname{Ult}(V,U)$ be the ultrapower whose elements are equivalence classes $[f]_U$ of functions $f:X\to V$, where $f\sim_U g$ means $\{x\in X:f(x)=g(x)\}\in U$. Let \begin{align*} j_U:V\to \operatorname{Ult}(V,U) \end{align*} be the ultrapower map defined by $j_U(a)=[c_a]_U$, where $c_a:X\to V$ is the constant map $c_a(x)=a$. By Los theorem for ultrapowers, applied to the ultrafilter $U$, the map $j_U$ is elementary. Since $\kappa$ is uncountable and $U$ is $\kappa$-complete, $U$ is countably complete. By the well-foundedness theorem for countably complete ultrapowers, $\operatorname{Ult}(V,U)$ is well founded. Applying the Mostowski collapse theorem, we identify the ultrapower with its transitive collapse $M$ and write \begin{align*} j:V\to M \end{align*} for the corresponding elementary embedding. The three external results used in this paragraph are standard ultrapower facts not yet resolved to wiki theorem IDs: Los theorem for ultrapowers, well-foundedness of countably complete ultrapowers, and the Mostowski collapse theorem. [/step] [step:Verify that the critical point of the ultrapower embedding is $\kappa$] We first show that $j$ fixes every ordinal below $\kappa$. Let $\alpha<\kappa$, and let $f:X\to \alpha$ be any function. The family \begin{align*} \{f^{-1}(\{\beta\}):\beta<\alpha\} \end{align*} has size $|\alpha|<\kappa$ and has union $X$. Since $U$ is a $\kappa$-complete ultrafilter, one of these fibers belongs to $U$. Hence there is a $\beta<\alpha$ such that $[f]_U=[c_\beta]_U$. It follows by induction on $\alpha<\kappa$ that $j(\alpha)=\alpha$. Next we show that $j(\kappa)\neq\kappa$. Define the cardinality map \begin{align*} r:X\to \kappa \end{align*} by $r(x)=|x|$. For every $\gamma<\kappa$, the set $\{x\in X:\gamma<|x|\}$ belongs to $U$: indeed, choose distinct ordinals $\alpha_\xi<\lambda$ for $\xi\leq\gamma$, and use fineness together with $\kappa$-completeness to see that \begin{align*} \{x\in X:\{\alpha_\xi:\xi\leq\gamma\}\subset x\}\in U. \end{align*} On this set, $r(x)>\gamma$. Therefore $[r]_U$ is an ordinal of $M$ below $j(\kappa)$ but above every $\gamma<\kappa$. Thus $j(\kappa)>\kappa$, and since all ordinals below $\kappa$ are fixed, $\operatorname{crit}(j)=\kappa$. [/step] [step:Identify the ultrapower seed with $j``\lambda$] Let \begin{align*} \operatorname{id}:X\to X \end{align*} be the identity map $\operatorname{id}(x)=x$, and let $s:=[\operatorname{id}]_U\in M$ be the ultrapower seed. We prove \begin{align*} s=j``\lambda. \end{align*} First fix $\alpha<\lambda$. By Los theorem, applied to the membership relation, \begin{align*} j(\alpha)\in s \iff \{x\in X:\alpha\in x\}\in U. \end{align*} The right-hand side holds by fineness. Hence $j``\lambda\subset s$. Conversely, suppose $a\in s$. Choose a function $f:X\to V$ such that $a=[f]_U$. By Los theorem, \begin{align*} a\in s \iff \{x\in X:f(x)\in x\}\in U. \end{align*} Let \begin{align*} S:=\{x\in X:f(x)\in x\}. \end{align*} Then $S\in U$. On $S$, the map $f|_S:S\to\lambda$ is regressive in the $P_\kappa(\lambda)$ sense, because $f(x)\in x\subset\lambda$. By normality, there is an $\alpha<\lambda$ such that \begin{align*} \{x\in S:f(x)=\alpha\}\in U. \end{align*} Thus $[f]_U=[c_\alpha]_U=j(\alpha)$, so $a\in j``\lambda$. Therefore $s\subset j``\lambda$, and the seed identity follows. [/step] [step:Derive $j(\kappa)>\lambda$ from the seed identity] Since $s=[\operatorname{id}]_U$, Los theorem gives \begin{align*} M\models s\in P_{j(\kappa)}(j(\lambda)). \end{align*} Thus, in $M$, the set $s$ has cardinality less than $j(\kappa)$. By the previous step, $s=j``\lambda$. The set $s$ is a set of ordinals, and its increasing enumeration has order type $\lambda$. Since $M$ is transitive and contains $s$, the order type of $s$ is computed correctly in $M$. Hence $M$ sees a bijection between $\lambda$ and $s$, so \begin{align*} \lambda<j(\kappa). \end{align*} [/step] [step:Use the seed representation to prove closure under $\lambda$-sequences] Let $(a_\alpha)_{\alpha<\lambda}$ be a $V$-sequence of elements of $M$. We prove that this sequence belongs to $M$. For each $\alpha<\lambda$, choose a representing function \begin{align*} f_\alpha:X\to V \end{align*} such that $a_\alpha=[f_\alpha]_U$. Define a function \begin{align*} F:X\to V \end{align*} as follows: for $x\in X$, $F(x)$ is the function with domain $x$ given by \begin{align*} F(x)(\alpha)=f_\alpha(x) \end{align*} for each $\alpha\in x$. Now evaluate $j(F)$ at the seed $s=[\operatorname{id}]_U$. By Los theorem, $j(F)(s)$ is the function in $M$ with domain $s$ satisfying \begin{align*} j(F)(s)(j(\alpha))=[f_\alpha]_U=a_\alpha \end{align*} for every $\alpha<\lambda$. Since $s=j``\lambda$, the increasing enumeration \begin{align*} e:\lambda\to s \end{align*} belongs to $M$ and satisfies $e(\alpha)=j(\alpha)$ for each $\alpha<\lambda$. Therefore \begin{align*} j(F)(s)\circ e:\lambda\to M \end{align*} is an element of $M$, and for every $\alpha<\lambda$, \begin{align*} (j(F)(s)\circ e)(\alpha)=j(F)(s)(j(\alpha))=a_\alpha. \end{align*} Thus $(a_\alpha)_{\alpha<\lambda}\in M$. [guided] We want to prove the closure condition $M^\lambda\subset M$. This means the following precise statement: whenever $(a_\alpha)_{\alpha<\lambda}$ is a sequence in $V$ and each $a_\alpha$ is an element of the ultrapower model $M$, the whole sequence must itself be an element of $M$. The seed $s=[\operatorname{id}]_U$ is the mechanism that lets the ultrapower see all $\lambda$ many coordinates at once. For each $\alpha<\lambda$, choose a function \begin{align*} f_\alpha:X\to V \end{align*} with $a_\alpha=[f_\alpha]_U$. This is possible because every element of the ultrapower is represented by some function from $X=P_\kappa(\lambda)$ to $V$. The problem is that a point $x\in X$ has size less than $\kappa$, so it cannot necessarily store all $\lambda$ many values $f_\alpha(x)$. But it can store the values indexed by the elements of $x$. Define \begin{align*} F:X\to V \end{align*} by declaring that $F(x)$ is the function with domain $x$ and value \begin{align*} F(x)(\alpha)=f_\alpha(x) \end{align*} for each $\alpha\in x$. Thus $F(x)$ is the local fragment of the desired sequence visible from the small set $x$. Now pass to the ultrapower. The object $j(F)(s)$ belongs to $M$, because $j(F)\in M$ and $s\in M$. Its domain is $s$: Los theorem says that the domain of $j(F)(s)$ is obtained by applying the same construction to the seed $s=[\operatorname{id}]_U$. For each $\alpha<\lambda$, the value of $j(F)(s)$ at $j(\alpha)$ is computed by Los theorem as \begin{align*} j(F)(s)(j(\alpha))=[x\mapsto F(x)(\alpha)]_U. \end{align*} On the fine set $\{x\in X:\alpha\in x\}\in U$, the expression $F(x)(\alpha)$ is defined and equals $f_\alpha(x)$. Therefore \begin{align*} [x\mapsto F(x)(\alpha)]_U=[f_\alpha]_U=a_\alpha. \end{align*} It remains to convert the domain from $s$ back to $\lambda$. By the seed computation already proved, $s=j``\lambda$. Since $s$ is a set of ordinals in the transitive model $M$, its increasing enumeration \begin{align*} e:\lambda\to s \end{align*} belongs to $M$ and satisfies $e(\alpha)=j(\alpha)$ for every $\alpha<\lambda$. Therefore the composition \begin{align*} j(F)(s)\circ e:\lambda\to M \end{align*} belongs to $M$. For each $\alpha<\lambda$, \begin{align*} (j(F)(s)\circ e)(\alpha)=j(F)(s)(j(\alpha))=a_\alpha. \end{align*} So the original sequence $(a_\alpha)_{\alpha<\lambda}$ is exactly the function $j(F)(s)\circ e$, and hence it is an element of $M$. [/guided] [/step] [step:Conclude the equivalence] From the ultrapower construction we have obtained an elementary embedding $j:V\to M$ into a transitive class $M$ such that $\operatorname{crit}(j)=\kappa$, $j(\kappa)>\lambda$, and $M^\lambda\subset M$. Hence $\kappa$ is $\lambda$-supercompact. The first direction constructed a nonprincipal fine normal $\kappa$-complete ultrafilter from any $\lambda$-supercompactness embedding, and the second direction constructed a $\lambda$-supercompactness embedding from any such ultrafilter. Therefore the two conditions are equivalent. [/step]