Invariants of C ⊗ N as equivariant level-constant maps

Fix a prime $p$ (as a Fact), a finite set $S$ of rational primes, a group $\Gamma$ in the zeroth universe with a normal subgroup $Sg$, a homomorphism $r \colon \Gamma \to \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$, a character $\chi \colon \Gamma \to (\mathbb{Z}/p)^{\times}$, and two representations $C, N$ of $\Gamma$ over $\mathbb{Z}/p$, with $N$ finite-dimensional over $\mathbb{Z}/p$. Assume given a $\mathbb{Z}/p$-linear isomorphism $e$ from $C$ onto the submodule levelConstantHom of maps $Sg \to \mathbb{Z}/p$, that is, the maps $\varphi$ with $\varphi(st) = \varphi(s) + \varphi(t)$ for all $s,t \in Sg$ which satisfy the predicate IsLevelConstantSr₁ for the restriction $r \circ Sg.\mathrm{subtype}$ and the set $S$; and assume the twisted equivariance hypothesis $he$: for all $g \in \Gamma$, $x \in C$ and $s,t \in Sg$ with $g^{-1} s g = t$ one has $e(\rho_C(g)x)(s) = \chi(g) \cdot e(x)(t)$. The conclusion asserts that the type of $\mathbb{Z}/p$-linear equivalences between the $\Gamma$-invariants of the representation on the tensor product $C \otimes N$ in $\mathrm{Rep}_{\mathbb{Z}/p}(\Gamma)$ and the submodule eqLevelConstantHom $r\,S\,Sg\,(N.\mathrm{twist}\,\chi)$ of maps $Sg \to N$ is nonempty; the latter consists of those $\varphi \colon Sg \to N$ which are additive, satisfy IsLevelConstantSr₁ for $r \circ Sg.\mathrm{subtype}$ and $S$ with values in $N$, and obey $\chi(g) \cdot \rho_N(g)(\varphi(t)) = \varphi(s)$ whenever $g^{-1} s g = t$. Only the existence of such an equivalence is asserted, no particular map being named.

This is the coefficient-moving step in the identification of restricted cohomology classes with level-constant homomorphisms: having described $C$ as the additive $S$-level-constant $\mathbb{Z}/p$-valued characters of $Sg$, $\chi$-equivariantly, it computes $(C \otimes N)^{\Gamma}$ as the $\Gamma$-equivariant $S$-level-constant maps $Sg \to N$ with coefficients twisted by $\chi$. It is used in the comparison of the dimension of the restricted-inflated $H^1_S$ with that of the invariants of a Selmer representation tensored with $N$.