Restriction of Scalars

Let $M$ be an $(R,S)$ Semiring Bimodule, $f:A\to R,g:B\to S$ be a pair of Semiring Homomorphisms, as in the following diagram:

The restriction of scalars of $M$ along $(f,g)$ is the $(A,B)$ Semiring Bimodule $f^{*}Mg^{*}$ formed whose underlying Commutative Monoid is $M$, with the left action $\lambda:A\times M\to M$ given by $\lambda(a,m)=f(a)\cdot m$ and the right action $\rho:M\times B\to M$ given by $\rho(m,b)=m\cdot g(b)$.

Moreover, the identity map $mathrm{id}{ifx..lse\par i}:M\to M$ is definitionally a $(f,g)$ Semilinear Map $f^{*}Mg^{*}\to M$ as $mathrm{id}{ifx..lse\par i}(a\cdot x\cdot b)$ is definitionally equal to $f(a)\cdot mathrm{id}{ifx..lse\par i}(x)\cdot g(b)$. This fills in the missing portion of our square:

Moreover, this is the universal such filler; for any other square

there exists a unique factorisation of $\psi$ through our square

Again, this holds essentially by definition, and the factorization of $\psi$ is just $\psi$ itself!

In much more concise terms, the restriction of scalars is the Cartesian Lift of $M$ along $(f,g)$ in the Double Category of Bimodules.