Buzzard–Diamond–Jarvis tensor-product conjecture in the definite case

Let $F$ be a totally real field, let $D$ be a quaternion algebra over $F$, and let $\overline{r}:G_F\to\mathrm{GL}_2(\mathbb F)$ be a two-dimensional continuous totally odd absolutely irreducible modular Galois representation. For each finite place $w$ write $\overline{\rho}_w=\overline{r}|_{G_{F_w}}$, and let $S^D_{\psi}(\mathbb F)[\mathfrak m_{\overline r}]$ be the corresponding localized space of mod $p$ automorphic forms. For each $w$, let $\pi^D_w(\overline r)$ be the associated smooth admissible representation of $(D\otimes_F F_w)^\times$, with the stated Serre-weight characterization at places $w\mid p$. Buzzard–Diamond–Jarvis' conjecture. If $\overline r$ is modular, there is a $(D\otimes_F\mathbb A_{F,f})^\times$-equivariant isomorphism

$$S^D_{\psi}(\mathbb F)[\mathfrak m_{\overline r}]\cong\otimes'_w\pi^D_w(\overline r).$$

At $w\mid p$, the representation satisfies $\operatorname{Hom}_{\mathrm{GL}_2(\mathcal O_{F_w})}(\sigma,\pi^D_w(\overline{\rho}))\neq0$ if and only if $\sigma\in\mathscr D(\overline{\rho}_w)$. The source recalls this as a conjecture of Buzzard, Diamond and Jarvis; its resolution status is not specified in the supplied text.