I am trying to write down by myself the proof of factor lemma, after staring at the proofs in Jech's textbook and Baumgartner's forcing survey and failed to gain much. It says an iteration forcing $\mathbb{P}_\alpha$ can be viewed as $\mathbb{P}_\beta*\dot{\mathbb{P}}_{\beta\alpha}$, where $\dot{\mathbb{P}}_{\beta\alpha}$ is a $\mathbb{P}_\beta$-name for an iteration of length $\alpha-\beta$ in the extension by $\mathbb{P}_\beta$.
Of course we are using the "correct definition" $\mathbb{P}*\dot{\mathbb{Q}}=\{(p,\dot{q}):p \in\dot{\mathbb{Q}}\land 1_{\mathbb{P}}\Vdash\dot{q}\in\dot{\mathbb{Q}}\}$, instead of the "incorrect definition" in Kunen, since although they agree for iteration with finite support, in general this one behaves better. But this definition of $\mathbb{P}*\dot{\mathbb{Q}}$, if taken literally, is terrible since it's a proper class. A common trick seems to be only considering those names $\dot{q}$ whose transitive closures have minimal sizes. My first question is why can't we just choose a representative from each equivalence class in a canonical way? By equivalence I mean $\pi\sim\sigma$ if $1_{\mathbb{P}}\Vdash\pi=\sigma$. I think I have found such a way: inductively define $W^{\mathbb{P}}_\alpha\subseteq V^{\mathbb{P}}_\alpha$ as follows: $W^{\mathbb{P}}_{\alpha+1}$ is the union of $W^{\mathbb{P}}_{\alpha}$ and the collection of all subsets $\pi$ of $W^{\mathbb{P}}_{\alpha}\times\mathbb{P}$ satisfying: (i) $\pi$ is not equivalent to any $\sigma\in W^{\mathbb{P}}_{\alpha}$, and (ii) $(\sigma,p)\in\pi$ iff $p\Vdash\sigma\in\pi$. Is it true that every name in $V^\mathbb{P}$ is equivalent to a unique name in $W^\mathbb{P}$? I think I also managed to show that for any $\tau\in V^\mathbb{P}$, $\{\sigma\in W^\mathbb{P}:1_{\mathbb{P}}\Vdash\sigma\in\tau\}$ is a set, and therefore can be used to define iterated forcing.
I'm a bit worried that if we don't have canonical representatives, then constructing dense embeddings between various posets may involve a lot of choice, and thus we must fix a choice function beforehand. This seems more suspicious when there are elementary embeddings floating around.
Second, at some point in the proof of the factor lemma, I found myself in need of the following: let $G$ be $\mathbb{P}$-generic over $V$, in $V[G]$ define a map that recursively transforms a $\mathbb{P}*\dot{\mathbb{Q}}$-name $\pi$ to a $\mathbb{Q}$-name $\bar{\pi}$, given by $\bar{\pi}=\{(\bar{\sigma},\dot{q}_G):(\sigma,(p,\dot{q}))\in\pi\land p\in G\}$; it would be of great help to me if this is a surjective map from $V^{\mathbb{P}*\dot{\mathbb{Q}}}$ to $(V[G])^{\mathbb{Q}}$. Is this true? Does it have a name/follow from some well-known result? I am attempting to write down $\mathbb{P}$-names for elements in $(V[G])^{\mathbb{Q}}$, define another map to transform them to $\mathbb{P}*\dot{\mathbb{Q}}$-names, and show the two transformations are sort of inverse to each other, but haven't sorted out the details.