PFA and the definability of the nonstationary ideal

We produce, relative to a $\mathsf{Z}\mathsf{F}\mathsf{C}$ model with a supercompact cardinal, a $\mathsf{Z}\mathsf{F}\mathsf{C}$ model of the Proper Forcing Axiom in which the nonstationary ideal on ${\omega }_1$ is ${\mathrm{\Pi }}_1$-definable in a parameter from $H_{{\mathrm{\aleph }}_2}$.