Semilinear Map

A function $f:M\to N$ between a Left R-Module $M$ and a Right S-Module $N$ is $\sigma$-semilinear for $\sigma:R^{\mathrm{op}}\to S$ if

• $f(x+y)=f(x)+f(y)$
• $f(rx)=f(x)\sigma(r)$

In other words, $f$ is Linear "up to a twist". Typically, $\sigma$ will be some Involution $(-)^{*}:R^{\mathrm{op}}\to R$ like Complex Conjugation.

More generally, a function $f:M\to N$ between a $(R_{1},S_{1})$ Bimodule $M$ and a $(R_{2},S_{2})$ Bimodule $N$ is $(\sigma,\rho)$ for $\sigma:R_{1}\to R_{2}$ and $\rho:S_{1}\to S_{2}$ if

• $f(x+y)=f(x)+f(y)$, EG: $f$ is a Group Homomorphism.
• $f(rx)=\sigma(r)f(x)$
• $f(xs)=f(x)\rho(s)$

The final two axioms are equivalent to requiring that $f(rxs)=\sigma(r)f(x)\rho(s)$, though it seems more natural to use the version that handles the two actions separately.

In terms of Displayed Categories

Semilinear maps are the correct morphisms in the Double Category of Bimodules, and Linear Maps are simply the vertical morphisms in this category. Note that this requires us to "unop" the definition of semilinear maps.

References

• https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Module/LinearMap/Defs.html#LinearMap Somewhat confusingly, Lean 4 refers to semilinear maps as linear maps, though this is not completely unreasonable.