Why does $Mf$ always support an $Mf$-orientation?

Question

Let $f:X\to BGL_1(\mathbb{S})$ be a morphism of $E_n$-spaces and determine a principle $GL_1(\mathbb{S})$-bundle over $X$. Then it can be shown in the classical case that there is always a Thom isomorphism $Mf\wedge Mf\to Mf\wedge X_+$ (Mahowald shows this, for instance here, modulo the concerns about operadic structure).

I'm interested in understanding how this map is produced in the modern $\infty$-categorical framework developed in work of Ando, Blumberg, Gepner and others. What this comes down to is showing that there is an orientation of $f$. This can be described as an equivalence of functors between $F=f\circ(-\wedge Mf):X\to BGL_1(\mathbb{S})\to BGL_1(Mf)$ and $\ast:X\to BGL_1(Mf)$. In other words, there should be an equivalence $F\simeq p^*Mf$ in the category $Mf_X\mathrm{-line}\simeq Fun(X^{op},Mf\mathrm{-line})$ where $Mf\mathrm{-line}$ is the category of $Mf$-modules which are equivalent to $Mf$ and $p:X\to \ast$ is the terminal map (note that to simplify notation I've called the composite map $F$). Such an equivalence would, upon applying $p_!$, yield an equivalence $Mf\wedge Mf=p_!F\simeq p_!p^\ast Mf=Mf\wedge X_+$.

One way to try to obtain such an orientation is to notice that the multiplication map $Mf\wedge Mf\to Mf$ is actually a map $p_!F\to Mf$ in $Mf\mathrm{-mod}$, which yields a map (simply by noting that $p_!$ is left adjoint to $p^\ast$) $F\to p^\ast Mf$ in $Mf_{X}\mathrm{-mod}$.

My question is the following: why is the map so obtained an equivalence? If it is not, is there another map $MF\to Mf$ that does give us this equivalence?

Answer 1

The updated version of A simple universal property of Thom ring spectra has a new section on multiplicative orientations. Corollary 3.17 proves that any $n$-fold loop map $f$ has an $E_{n-1}$ $Mf$-orientation.

Answer 2

I just want to add another answer to this, which is Corollary 4.16 of arXiv:1810:00734. This result of course uses Omar and Tobias' in an essential way, so is not somehow independent, but what it does do (using the preceding theorem in that paper) is give an explicit construction of that equivalence as the coaction followed by the multiplication on $Mf$, and identifies this with the map constructed (somewhat less explicitly) in Corollary 2.26 of arXiv:1403.4325, which to some extent is another aspect of my original question.