Can ultrapowering add choice? I'm supervising a reading course in set theory, and the following question came up (let $\mathsf{LT}$ be Łoś's Theorem; in an earlier version of this question I mistakenly thought $\mathsf{LT}$ was equivalent to $\mathsf{BPI}$):
Suppose $M$ is a (not necessarily transitive) model of $\mathsf{ZF}$, and $I,\mathcal{U}\in M$ with $M\models$ "$\mathcal{U}$ is an ultrafilter on $I$." Let $M^\mathcal{U}$ be the "internal-to-$M$" ultrapower of $M$ by $\mathcal{U}$, that is, the $\{\in\}$-structure whose elements are equivalence classes of elements of $(M^I)^M$ modulo $\mathcal{U}$-equivalence. Note that this structure might fail to be a "true" ultrapower in the sense of the metatheory since we could have $\mathcal{P}(I)^M\not=\mathcal{P}(I)^V$ or $(M^I)^M\not=(M^I)^V$ (or both).
Let $j: M\rightarrow M^\mathcal{U}$ be the obvious embedding; as usual, $M^\mathcal{U}$ and $j$ are appropriately definable in $M$. If $M\models\mathsf{ZFC}$ (or indeed just $\mathsf{ZF+LT}$) then $j$ is elementary. However, if we merely assume $M\models\mathsf{ZF}$, this breaks down.

Question 1: Can we have $M\models\neg\mathsf{LT}$ but $M^\mathcal{U}\models\mathsf{LT}$ (or even $\mathsf{AC}$)?

Without any choice in $M$, I don't see how to ensure a failure of choice in $M^\mathcal{U}$. In particular, if $\mathscr{A}=(A_k)_{k\in K}$ is a family of nonempty sets in $M$, a choice function $f$ for $j(\mathscr{A})$ in $M^\mathcal{U}$ might, for some $k\in K$, satisfy $$f(j(k))\in j(A_k)\setminus \{j(a): a\in A_k\}$$ and so not yield (directly at least) a choice function for $\mathscr{A}$ in $M$.
There's also a "local" version of this question:

Question 2: Can we have a choice instance $\mathscr{A}\in M$ such that $M\models$ "$\mathscr{A}$ has no choice function" but $M^\mathcal{U}\models$ "$j(\mathscr{A})$ has a choice function"?

 A: If $M^\mathcal{U} \models$ extensionality, then the answer is "no".
I claim the following are equivalent:

*

*$M^\mathcal{U} \models$ extensionality

*$M \models$ "For all families $\{A_i\}_{i \in I}$ of sets with all $A_i$ nonempty, there is some $V \in \mathcal{U}$ and some choice function $f \in \prod\limits_{v \in V} A_v$".

*For all propositions $\phi(c_1, \ldots, c_n)$ in the language of set theory, for all $[f_1], \ldots, [f_n] \in M^\mathcal{U}$, $M^\mathcal{U} \models \phi([f_1], \ldots, [f_n])$ if and only if $M \models \{i \in I \mid \phi(f_1(i), \ldots, f_n(i))\} \in \mathcal{U}$ [a special case of a "class-sized Los's theorem scheme"]

*The canonical map $j : M \to M^\mathcal{U}$ is an elementary embedding.

If this claim is true, then the answer to the above question is essentially "no". I assume that OP only cares about cases where $M^\mathcal{U}$ is a model of $\mathbf{ZF}$ or, at the very least, is a model of some very weak set-theoretic axioms which would include extensionality. If that is the case, then $M$ and $M^\mathcal{U}$ are elementarily equivalent and thus model the same sentences in the language of set theory. So if $M \models \mathbf{ZF} + \neg \mathbf{LT}$ and we can get a model $M^\mathcal{U} \models \mathbf{ZF}$, then $M^\mathcal{U} \models \neg \mathbf{LT}$.
Edit: see Asaf’s comment linking to a paper of Spector in which he asserts the above result (though he doesn’t walk through the full proof).
I have not covered what happens when $M^\mathcal{U}$ does not model extensionality, both because I don't really know and because I strongly suspect that it is of no interest to OP.
Also equivalent to the above is $M \models $ "Los's theorem holds for $\mathcal{U}$". We will not use (or prove) this fact, but I thought it was relevant to the topic.
We will now show $1 \implies 2$. Indeed, suppose $M^\mathcal{U} \models$ extensionality. Consider some $A \in M$ such that $M \models $ "$A$ is an $I$-indexed family of nonempty sets". Then note that $[A] \in M^\mathcal{U}$. And $M^\mathcal{U} \models [A] \neq m(\emptyset)$. Since $M^\mathcal{U} \models$ extensionality, we know that either $M^\mathcal{U} \models \exists x (x \in [A] \land x \notin m(\emptyset) \lor x \in m(\emptyset) \land x \notin [A])$.
Take some $[f] \in M$ such that $M^\mathcal{U} \models [f] \in [A] \land [f] \notin m(\emptyset) \lor [f] \in m(\emptyset) \land [f] \notin [A]$. Then we have two cases. The first case is $M^\mathcal{U} \models [f] \in [A] \land [f] \notin m(\emptyset)$. In this case, we have $M^\mathcal{U} \models [f] \in [A]$. So there is some $V \in \mathcal{U}$ such that $M \models \forall v \in V (f(v) \in A(v))$. Then $M \models f|_V \in \prod\limits_{v \in V} A_v$. This completes our proof.
Now we show that $2 \implies 3$. To do this is a straightforward induction on $\phi$. To keep things simple, WLOG let $\phi$ only have $\land$, $\neg$, and $\exists$.
Base case 1: $\phi(c_1, \ldots, c_n) :\equiv c_j = c_k$. In this case, we see that $M^\mathcal{V} \models [f_j] = [f_k]$ iff $[f_j] = [f_k]$ iff $M \models \{i \in I \mid f_j(i) = f_k(i)\} \in \mathcal{U}$.
Base case 2: $\phi(c_1, \ldots, c_n) :\equiv c_j \in c_k$. Exactly the same as above, except swap $=$ for $\in$.
Inductive step 1: Write $\phi(c_1, \ldots, c_n) :\equiv \neg \psi(c_1, \ldots, c_n)$. Then $M^\mathcal{U} \models \neg \psi([f_1], \ldots, [f_n])$ iff $M^\mathcal{U} \nvDash \psi([f_1], \ldots, [f_n])$ iff $M \nvDash \{i \in I \mid \psi(f_1(i), \ldots, f_n(i))\} \in \mathcal{U}$ iff $M \vDash \{i \in I \mid \psi(f_1(i), \ldots, f_n(i))\} \notin \mathcal{U}$ iff $M \vDash \{i \in I \mid \neg \psi(f_1(i), \ldots, f_n(i))\} \in \mathcal{U}$ (the last step uses the properties of an ultrafilter: if $S \subseteq I$ and $S \notin \mathcal{U}$, then $I \setminus S \in \mathcal{U}$).
Inductive step 2: $\land$. Like inductive step 1, it's fairly straightforward and uses the properties of a filter right at the end.
Inductive step 3: Write $\phi(c_1, \ldots, c_n) = \exists c_{n + 1} \psi(c_1, \ldots, c_n, c_{n + 1})$. Suppose $M^\mathcal{U} \models \exists c_{n + 1} \psi([f_1], \ldots, [f_n], c_{n + 1})$. Then there is some $[f_{n + 1}] \in M^\mathcal{U}$ such that $M^\mathcal{U} \models \psi([f_1], \ldots, [f_n], [f_{n + 1}])$. Then $M \models \{i \in I \mid \psi(f_1(i), \ldots, f_n(i), f_{n + 1}(i))\} \in \mathcal{U}$. And of course $M \models \{i \in I \mid \psi(f_1(i), \ldots, f_n(i), f_{n + 1}(i))\} \subseteq \{i \in I \mid \exists c_{n + 1} \psi(f_1(i), \ldots, f_n(i), c_{n + 1})\}$. Therefore, $M \models \{i \in I \mid \exists c_{n + 1} \psi(f_1(i), \ldots, f_n(i), c_{n + 1})\} \in \mathcal{U}$.
Conversely, suppose $M \models \{i \in I \mid \exists c_{n + 1} \psi(f_1(i), \ldots, f_n(i), c_{n + 1})\} \in \mathcal{U}$. Argue now within $M$. Let $V = \{i \in I \mid \exists c_{n + 1} \psi(f_1(i), \ldots, f_n(i), c_{n + 1})\}$. Then $\forall v \in V \exists c_{n + 1} \psi(f_1(v), \ldots, f_n(v), c_{n + 1})$. By the axiom scheme of collection (which is a theorem scheme in ZF), there exists some $B$ such that $\forall v \in V \exists b \in B \psi(f_1(v), \ldots, f_n(v), b)$. Now define a family of sets $\{A_i\}_{i \in I}$ by $A_i = \{b \in B \mid \psi(f_1(i), \ldots, f_n(i), b)\}$ if $i \in V$, and $\{\emptyset\}$ otherwise.
By (2), there is some $W \in \mathcal{U}$ and some choice function $f_{n + 1} : \prod\limits_{w \in W} A_w$. Extend the domain of $f_{n + 1}$ to all of $I$ however you like, for instance by defining $f_{n + 1}(i) = \emptyset$ for $i \notin W$.
Now note that $W \cap V \in \mathcal{U}$, and $W \cap V \subseteq \{i \in I \mid \psi(f_1(i), \ldots, f_n(i), f_{n + 1}(i))\}$. Then $\{i \in I \mid \psi(f_1(i), \ldots, f_n(i), f_{n + 1}(i)\} \in \mathcal{U}$.
So we have established that $M \models \exists f_{n + 1} (\{i \in I \mid \psi(f_1(i), \ldots, f_n(i), f_{n + 1}(i)\} \in \mathcal{U}$ and $f_{n + 1}$ is a function with domain $I)$. Then there is some $[f_{n + 1}] \in M^\mathcal{U}$ such that $M \models \{i \in I \mid \psi(f_1(i), \ldots, f_n(i), f_{n + 1}(i)\} \in \mathcal{U}$. Then by the inductive hypothesis, $M^\mathcal{U} \models \psi([f_1], \ldots, [f_n])$. Then $M^\mathcal{U} \models \exists c_{n + 1} \psi([f_1], \ldots, [f_n], c_{n + 1})$. This completes the proof.
Now, we show that $3 \implies 4$. Given an arbitrary $\phi(c_1, \ldots, c_n)$ and $a_1, \ldots, a_n \in M$, we see that $M \models \phi(a_1, \ldots, a_n)$ iff $M \models \{i \in I \mid \phi(a_1, \ldots, a_n)\} \in \mathcal{U}$ iff $M^\mathcal{U} \models \phi(m(a_1), \ldots, m(a_n))$. This completes the proof.
Finally, we show that $4 \implies 1$. We know that $M \models \mathbf{ZF}$, and therefore $M \models$ extensionality. Since $j : M \to M^\mathcal{U}$ and extensionality is a sentence, we see that $M^\mathcal{U} \models$ extensionality. $\square$
Finally, I’d like to add a perspective which is not seen in Spector’s paper. We look at this from a topos-theoretic point of view.
We begin with a Boolean well-pointed autological topos $C$, which is (roughly) the topos-theoretic equivalent of ZF - you can throw in a topos version of foundation to make the two totally equivalent. We then consider some object $I \in C$ and some $\mathcal{U} \subseteq P(I)$ such that $C \models$ “$\mathcal{U}$ is an ultrafilter on $I$“.
Now we can consider the slice topos $C / I$. Every sentence true in $C$ is true in the stack semantics (that is, the internal logic) of $C$. And the pullback functor $I \times - : C \to C / I$ preserves the stack semantics - the topos-theoretic analogue of an elementary embedding. So the sentences true in $C/I$’s stack semantics are exactly those true in $C$.
Now $\mathcal{U}$ gives us a filter on the truth values of $C / I$, which correspond to the subobjects of $I$. This allows us to do the filter-quotient construction on $C / I$ to obtain a new topos - call it $C^\mathcal{U}$.
Now in particular, it can be shown that the filter quotient of an autological topos is autological and, moreover, that the functor $[-] : C / I \to C^\mathcal{U}$ preserves the stack semantics. Because $\mathcal{U}$ is an ultrafilter, the topos $C^\mathcal{U}$ is 2-valued. Call the composite functor $j : C \to C^\mathcal{U}$; then $j$ preserves the stack semantics.
However, there is a minor snag, which is that $C^\mathcal{U}$ is not necessarily well-pointed and thus doesn’t directly give rise to an ordinary model of ZF. In fact, that $C^\mathcal{U}$ is well-pointed is equivalent to the above 4 conditions - to see this, note that a Boolean topos is well-pointed iff it is 2-valued and $1$ is projective. If this condition holds, then the topos-theoretic $C^\mathcal{U}$ and the set-theoretic version $M^\mathcal{U}$ are perfectly identical - if one starts with an $M$, considers its category of sets $C$, and builds the ultrapower $C^\mathcal{U}$, this is the same as first building the ultrapower $M^\mathcal{U}$ and then taking its category of sets.
But even if $C^\mathcal{U}$ is not well-pointed, it’s still a topos with exactly the same stack semantics as $C$, as witnessed by the stack semantics preserving functor $j$. And the stack semantics can be described by $C^\mathcal{U} \Vdash \phi([A_1], \ldots, [A_n], [f_1], \ldots, [f_m])$ if and only if $C \models \{i \in I \mid \phi(i^*(A_1), \ldots, i^*(A_n), i^*(f_1), \ldots, i^*(f_m))\} \in \mathcal{U}$ (where $i^*$ is the pullback along $i : 1 \to I$). The stack semantics of the global elements of $C^\mathcal{U}$ is precisely the topos theory phrasing of the theory $T$ described in section 3 of Spector’s paper.
