Existence of the mod-$l$ cycle homomorphism

Let $R_E(GL_n(\mathcal{O}_F))$ and $R_{\mathbb{F}}(GL_n(\mathcal{O}_F))$ be the Grothendieck groups of finite-length representations over $E$ and $\mathbb{F}$, respectively, and let $\mathcal{Z}(R^\square(\overline{\rho}))$ and $\mathcal{Z}(\overline{R}\,^\square(\overline{\rho}))$ denote the corresponding groups of cycles. Let $\operatorname{cyc}$ and $\operatorname{red}$ be the homomorphisms in the displayed diagram. Mod-$l$ cycle-homomorphism conjecture. There exists a unique homomorphism

$$\overline{\operatorname{cyc}}: R_{\mathbb{F}}(GL_n(\mathcal{O}_F)) \longrightarrow \mathcal{Z}(\overline{R}\,^\square(\overline{\rho}))$$

that makes the reduction diagram commute:

$$\begin{CD} R_E(GL_n(\mathcal{O}_F)) @>{\operatorname{cyc}}>> \mathcal{Z}(R^\square(\overline{\rho})) \\ @V{\operatorname{red}}VV @V{\operatorname{red}}VV \\ R_{\mathbb{F}}(GL_n(\mathcal{O}_F)) @>{\overline{\operatorname{cyc}}}>> \mathcal{Z}(\overline{R}\,^\square(\overline{\rho})). \end{CD}$$

The assertion gives a well-defined mod-$l$ counterpart to the characteristic-zero cycle map and is part of the geometric formulation of the Breuil--Mézard conjecture; the supplied text does not state whether it has been proved.