Physlib.Mathematics.ConjModule

For a module $M$ over a commutative star-ring $k$, the conjugate module $\text{ConjModule} M$ is a type synonym for $M$ that carries the same additive group structure but is equipped with a twisted scalar action. Specifically, for any $r \in k$ and $v \in M$, the scalar multiplication in $\text{ConjModule} M$ is defined by $r \cdot v = \text{star}(r) v$, where $\text{star}$ denotes the involution on $k$.

The conjugate module $\text{ConjModule} M$ inherits the additive commutative group structure from the original module $M$. This means that addition and the additive identity in $\text{ConjModule} M$ are defined identically to those in $M$.

Given a module $M$ over a commutative star-ring $k$, the conjugate module $\text{ConjModule} M$ is equipped with a $k$-module structure where the scalar action is twisted by the ring involution $\text{star}$. Specifically, for any $r \in k$ and $v \in \text{ConjModule} M$, the scalar multiplication is defined as $r \cdot v = \text{star}(r) v$, where the right-hand side denotes the original scalar multiplication in $M$.

Let $M$ be a module over a commutative star-ring $k$. The map $\text{conjEquiv} : M \simeq \text{ConjModule } M$ is the canonical conjugate-linear equivalence between $M$ and its conjugate module $\text{ConjModule } M$. This map is the identity on the underlying additive group, meaning it sends each element $v \in M$ to itself. It is semilinear with respect to the ring involution $\text{star}$ of $k$, satisfying $\text{conjEquiv}(r \cdot v) = \text{star}(r) \cdot \text{conjEquiv}(v)$ where the scalar multiplication on the right-hand side is the twisted action defined in $\text{ConjModule } M$.

For a module $M$ over a commutative star-ring $k$, let $\text{ConjModule } M$ denote the conjugate module, which consists of the same additive group as $M$ but with a twisted scalar action defined by $r \cdot v = \text{star}(r) v$. The map $\text{ConjModule.involution}$ is the $k$-linear isomorphism $\text{ConjModule}(\text{ConjModule } M) \simeq_k M$ that identifies the double-conjugate module with the original module. This map is $k$-linear (rather than merely semilinear) because the composition of the ring involution $\text{star}$ with itself is the identity map on $k$. It is formally defined as the inverse of the composition of two canonical conjugate-linear equivalences.

For a commutative star-ring $k$ and an index set $\iota$, let $k^{(\iota)}$ (denoted in Lean as `ι →₀ k`) be the module of finitely supported functions from $\iota$ to $k$. The map `ConjModule.starFinsupp` is a conjugate-linear self-equivalence of $k^{(\iota)}$ that performs coordinate-wise conjugation. Specifically, for any function $f \in k^{(\iota)}$, the map sends $f$ to the function $i \mapsto \text{star}(f(i))$, where $\text{star}$ denotes the involution of the ring $k$.

Let $k$ be a commutative star-ring and $M$ be a $k$-module. Given a basis $b = \{e_i\}_{i \in \iota}$ for $M$, `Basis.conj b` is the corresponding basis for the conjugate module $\text{ConjModule } M$. The basis elements are the same as those in $b$ (mapped via the canonical equivalence $\text{conjEquiv}$), but the coordinates of a vector $v$ in this basis are the conjugates of its coordinates in the original basis. That is, if the representation of $v$ in $b$ is the family of scalars $(c_i)_{i \in \iota}$, then its representation in `Basis.conj b` is $(\text{star}(c_i))_{i \in \iota}$.

Let $k$ be a commutative star-ring and $M$ be a $k$-module. Let $b$ be a basis for $M$ indexed by $\iota$. For any element $v$ in the conjugate module $\text{ConjModule } M$ and any $i \in \iota$, the $i$-th coordinate of $v$ with respect to the conjugate basis $\text{Basis.conj } b$ is the conjugate (under the $\text{star}$ operation) of the $i$-th coordinate of the corresponding element in $M$ with respect to the original basis $b$. Mathematically, this is expressed as: $$(\text{Basis.conj } b).\text{repr}(v)_i = \text{star}(b.\text{repr}(\text{conjEquiv}^{-1}(v))_i)$$ where $\text{conjEquiv}^{-1}$ is the inverse of the canonical conjugate-linear equivalence between $M$ and $\text{ConjModule } M$.

Let $k$ be a commutative star-ring and $M$ a $k$-module. Given a basis $b = \{e_i\}_{i \in \iota}$ for $M$, let $\text{Basis.conj } b$ be the induced basis for the conjugate module $\text{ConjModule } M$. For any index $i \in \iota$, the $i$-th basis vector of $\text{Basis.conj } b$ is given by the image of the $i$-th vector of $b$ under the canonical conjugate-linear equivalence $\text{conjEquiv} : M \simeq \text{ConjModule } M$. Mathematically, this is expressed as $(\text{Basis.conj } b)_i = \text{conjEquiv}(b_i)$.