My question arises from thinking about how we can obtain class forcing extensions from truncations of set forcing extensions in the presence of a (strongly) inaccessible cardinal in the following sense. Let $\kappa$ be an inaccessible cardinal and let $\mathbb P$ be a forcing such that $\mathbb P \subseteq V_{\kappa}$. Now we can consider $\mathbb P$ simultaneously as a set forcing (in $V$) and as a class forcing over $V_{\kappa}$. Now let $G$ be a $(V;\mathbb P)$-generic filter. Then we can ask how $V[G]$ and $V_{\kappa}[G]$ relate to each other, where in this context $V_{\kappa}[G] := \{ \sigma_G : \sigma\in V^{\mathbb P}\cap V_{\kappa} \}$.
A naive approach would be to conjecture that $V_{\kappa}[G] = (V_{\kappa})^{V[G]}$. This is of course not true in general: if $\mathbb P$ is the Levy collapse $\mathrm{Col}(\omega, <\kappa)$, then, e.g., we have $\wp^{V[G]}(\omega) \in (V_{\kappa})^{V[G]}\setminus V_\kappa[G]$, the underlying problem being that $(V_{\kappa})^{V[G]}$ is a model of the power set axiom, whereas $V_{\kappa}[G]$ is not.
We can remedy this last problem by considering $H_{\kappa}$ instead of $V_\kappa$ in the above argument (which is the same in the ground model); and indeed we get the following
Fact: Let $\kappa$ be inaccessible and $\mathbb P\subseteq H_{\kappa}^V$ a forcing preserving the regularity of $\kappa$. Let $G$ be a $(V;\mathbb P)$-generic filter. Then $H_\kappa^V[G] = (H_\kappa)^{V[G]}$.
Proof. The difficult direction is to show that $(H_\kappa)^{V[G]} \subseteq H_\kappa^V[G]$. For this let $x\in (H_\kappa)^{V[G]}$ and assume (inductively) that $x\subseteq H_\kappa^V[G]$. Then let $\sigma\in V^{\mathbb P}$ be such that $\sigma_G = x$ and $\mathrm{dom}(\sigma) \subseteq V^{\mathbb P}\cap H_{\kappa}^V$. In $V[G]$ we define a function $f: x\to \kappa$ by setting
$$ f(y) := \min\{ \alpha < \kappa : \exists\langle \tau, p\rangle\in \sigma\cap V_{\alpha+1} (p\in G \wedge \tau_G = y) \} $$
for any $y\in x$. Now note that $f``x$ is bounded below $\kappa$, since $\kappa$ is regular in $V[G]$ and by assumption there can be no surjection from $x$ onto $\kappa$. Thus take $\alpha < \kappa$ such that $f``x\subseteq \alpha$ and let $\sigma' := \sigma\cap V_{\alpha}$. Then $\sigma'_G = \sigma_G = x$ and $\sigma' \in V^{\mathbb P}\cap H^V_{\kappa}$ by inaccessibility of $\kappa$ in $V$. Therefore $x\in H_\kappa^V[G]$. $\Box$
This proof depends on the fact that $\mathbb P$ preserves the regularity of $\kappa$, but on the other hand I could not construct a counterexample for a forcing singularizing $\kappa$. This leads me to ask the following
Question: Let $\kappa$ be inaccessible. Can there be a forcing $\mathbb P\subseteq H_{\kappa}^V$ that does not collapse $\kappa$ and such that there is some $(V;\mathbb P)$-generic filter $G$ with $H_{\kappa}^V[G] \neq (H_{\kappa})^{V[G]}$ ?
