The idea of a projection $\pi\colon\mathbb{Q}\to\mathbb{P}$ of forcing notions is something like a combinatorial stand-in for the fact that forcing with $\mathbb{Q}$ produces a generic for $\mathbb{P}$. One then studies the necessary quotient forcing to get your from $V^{\mathbb{P}}$ to $V^{\mathbb{Q}}$ and hopes it isn't too bad for whatever it is that needs to happen. This type of argument is typical when dealing with Mitchell- or Prikry-like forcings.

Unfortunately, as far as I'm able to tell, a lot of the facts about projections are relegated to folklore and rarely stated carefully. Even the definition of a projection seems to be a slippery thing! For example, here is the definition that most sources I've consulted agree on:

An order-preserving map $\pi\colon\mathbb{Q}\to\mathbb{P}$ is a projection if

- $\pi(1_{\mathbb{Q}})=1_{\mathbb{P}}$ and
- for any $q\in\mathbb{Q}$ and any $p\leq \pi(q)$ there is $\bar{q}\leq q$ such that $\pi(\bar{q})\leq p$.

This definition appears, for example, in Cummings' chapter in the *Handbook of Set Theory*. However, in a different chapter of the same Handbook, Abraham gives a definition which strengthens (2) above to $\pi(\bar{q})=p$. Abraham also mentions a third, even stronger version of the definition.

It also seems that most textbooks/references prefer to talk about complete suborders rather than projections (this is what Kunen does, as well as Shelah in *Proper and Improper Forcing*). Complete suborders are closely related to projections, but the two concepts are distinct and the exact relationship isn't totally clear to me.

Is there a canonical writeup of what a forcing projection is, along with a list (preferably with proofs) of their key properties? Ideally, this would include a spelled out connection between $\mathbb{Q}$ adding a generic for $\mathbb{P}$ and a projection of $\mathbb{Q}$ to something like the Boolean completion of $\mathbb{P}$, as well as a discussion of quotient forcing.