Failure of Choice only for sets above a certain rank Let $\alpha$ be an ordinal. How can we show that the following theory is consistent?
$\mathrm{ZF}$ + "there exists a set with rank greater than $\alpha$ that is not well ordered" + "every set of rank lower than $\alpha$ is well ordered".
 A: The idea is to pick $\kappa$ which is large enough, and does not inject into $V_\alpha$. Then we add subsets to $\kappa$ and use them to generate subsets of $2^\kappa$ which cannot be well-ordered. These cannot be embedded into $V_\alpha$ either, so we finished our proof.
We begin with the forcing $P$ whose conditions are functions from $\kappa\times\kappa$ into $2$, with domain of cardinality $<\kappa$. $q$ is stronger than $p$ if $p\subseteq q$, and we denote this by $q\leq p$.
Easily, the forcing adds $\kappa$ new subsets to $\kappa$. But the forcing is $\kappa$-closed (or $<\kappa$-closed, depending on your flavor of terminology) so it doesn't add any subset to any smaller cardinal. In particular it doesn't add any subset to $V_\alpha$, so no sets of rank $\alpha$ are added.
We consider the following names, $\dot r_\alpha=\{(p,\check\beta)\mid p(\alpha,\beta)=1\}$, for $\alpha<\kappa$. These are the canonical names for the new subsets of $\kappa$ that are being added.
Let $\scr G$ be the group of all permutations of $\kappa$ in the ground model. Although it is enough to consider permutations which only move finitely many points at a time (as an analysis of the following argument will show). $\scr G$ acts on the poset $P$ in the following way: $$\pi p(\pi\alpha,\beta)=p(\alpha,\beta).$$
Extend those actions to actions of $P$-names, by defining $\pi\dot x=\{(\pi p,\pi\dot y)\mid (p,\dot y)\in\dot x\}$.  We have now the following lemma,

The Symmetry Lemma: For every formula $\varphi(\dot u_1,\ldots,\dot u_k)$ and every condition $p$, and every $\pi\in\scr G$: $$p\Vdash\varphi(\dot u_1,\ldots,\dot u_k)\iff\pi p\Vdash\varphi(\pi\dot u_1,\ldots,\pi\dot u_k).$$

Proof. Induction on the formulas and the names.
Now take any regular $\mu\leq\kappa$, and we will define a model in which the name $\dot R=\{(1,\dot r_\alpha)\mid\alpha<\kappa\}$ is interpreted to have Hartogs number $\mu$ (the least cardinal cannot be injected into the set), and $\sf DC_{<\mu}$ holds. In particular it shows that that set cannot be well-ordered, because it should have the Hartogs number of $\kappa^+$.
Define $\cal F$ to be a filter of subgroups of $\scr G$ where $H\in\cal F$ if and only if there exists $E\subseteq\kappa$ such that $|E|<\mu$, and all the permutations in $H$ fix $E$ pointwise. We define by induction the class $\sf HS$. Given a $P$-name $\dot x$, we say that $\dot x\in\sf HS$ if there exists $H\in\cal F$ such that whenever $\pi\in H$, $\pi\dot x=\dot x$, and if every $\dot y$ which appears in $\dot x$ is already in $\sf HS$.
If $H$ is a subgroup which contains the pointwise stabilizer of $E$, and $H$ fixes $\dot x$, we say that $E$ is a support for $\dot x$, and we note that every permutation which fixes $E$ pointwise will fix $\dot x$ as well.

Lemma 1: The following holds.
  
  
*
  
*For every $x$ in the ground model, $\check x\in\sf HS$. With $\varnothing$ as support.
  
*For every $\alpha<\kappa$, $\dot r_\alpha\in\sf HS$ with support $\{\alpha\}$.
  
*$\dot R\in\sf HS$ with the empty support.
  

Proof. Exercise.
Let $G\subseteq P$ be a generic filter. Let $V[G]$ be the generic extension of the universe and let $N=\{\dot x^G\mid\dot x\in\sf HS\}$ be the interpretation of all the names in $\sf HS$.

Lemma 2: $N$ is a transitive model of $\sf ZF$, and $V\subseteq N$.

Proof. Transitivity follows from the inductive definition of $\sf HS$; $V\subseteq N$ from the first point of the previous lemma; and $N\models\sf ZF$ because it is almost universal and closed under Goedel functions, but one can also verify the axioms directly (see also Jech "Set Theory", 3rd eds. Ch. 15). $\square$

Theorem: In $N$, $\sf AC$ fails.

Proof. Let $R=\dot R^G\in V$, we will show that it cannot be well-ordered in $N$, as promised.
From the last point of Lemma 1, $R\in N$. Suppose now that $f\colon \mu\to R$ is an injection, and $f\in N$. There exists some name $\dot f\in\sf HS$ and some $E\in[\kappa]^{<\mu}$ such that $\dot f=f$ and $E$ is a support for $\dot f$.
Let $p$ be a condition such that $p\Vdash\dot f\colon\check\mu\to\dot R$. We may assume without loss of generality that for some $\alpha\notin E$, and some $\gamma<\kappa$ we have $p\Vdash\dot f(\check\gamma)=\dot r_\alpha$.
Let $\alpha<\beta<\kappa$ such that $\beta\notin E$ and there is no ordinal $\delta$ such that $(\beta,\delta)\in\operatorname{dom} p$. We define the permutation $\pi$ to switch between $\alpha$ and $\beta$ and be the identity everywhere else.
Clearly $\pi$ fixes $E$ pointwise and therefore $\pi\dot f=\dot f$. Therefore by the symmetry lemma, $\pi p\Vdash\dot f\colon\check\mu\to\dot R$, and also $\pi p\Vdash\dot f(\check\gamma)=\dot r_\beta$.
If $p$ and $\pi p$ are compatible then we have a contradiction because $q\leq p,\pi p$ would have to force that $\dot r_\alpha=\dot f(\check\gamma)=\dot r_\beta$, and also $\dot r_\alpha\neq\dot r_\beta$!
And indeed if $(\xi,\zeta)\in\operatorname{dom} p$ then either $\xi=\alpha$ and then $\pi\xi=\beta$ and $(\beta,\zeta)\notin\operatorname{dom} p$ at all; or $\pi\xi=\xi$. Similarly for $\pi p$ exchanging $\beta$ with $\alpha$. Therefore the conditions $p$ and $\pi p$ are compatible and this is a contradiction. $\square$

Bonus Lemma: If $f\colon V[G]\to N$ such that $\operatorname{dom} f<\mu$, then there exists $\dot f\in\sf H$ such that $\dot f^G=f$.

Proof. Exercise (note that you have to use the fact that the forcing $P$ is $\kappa$-closed).
Now trivially $\sf DC_{<\mu}$ holds in $N$, because whenever $S$ is a subset of $X^<\gamma\times X$, for a non-empty $X$ and $\gamma<\mu$, satisfying the conditions of $\sf DC_{\gamma}$, there is a function $f$ witnessing that in $V[G]$ and by the bonus lemma, it is also in $N$.

Further bibliography:
Here is a list of places where these techniques are discussed, do note that the approaches and notations slightly differ from one place to another.


*

*Jech, "Set Theory", 3rd eds. (Springer 2006)

*Jech, "The Axiom of Choice". (North-Holland 1973)

*Dimitriou, "Symmetric Models, Singular Cardinal Patterns, and Indiscernibles. (PhD dissertation, Universität Bonn 2011)

*Karagila, "Vector Spaces and Antichains of Cardinals in Models of Set Theory". (MSc thesis, Ben-Gurion University of the Negev 2012)

