Physlib.Relativity.Tensors.Color.Lift

In the discrete category $\text{Discrete}(C)$ associated with a type $C$, a morphism $h : c_1 \to c_2$ exists if and only if $c_1 = c_2$. This function takes such a morphism $h$ and returns the canonical isomorphism $c_1 \cong c_2$ induced by this equality.

Given a functor $F : \text{Discrete } C \to \text{Rep}_k G$, which assigns a representation of a group $G$ over a field $k$ to each "color" in $C$, and an object $f \in \text{OverColor } C$ (which consists of an indexing set $I$ and a mapping $f.\text{hom} : I \to C$), the representation `toRep F f` is defined as the tensor product of representations corresponding to the colors in $f$. Specifically, the underlying vector space is the tensor product $\bigotimes_{i \in I} V_{f(i)}$, where $V_{f(i)}$ is the representation space of $F(f(i))$. For any group element $g \in G$, its action $\rho(g)$ on the tensor product is given by the tensor product of the individual actions: $$\rho(g) = \bigotimes_{i \in I} \rho_{f(i)}(g)$$ where $\rho_{f(i)}(g)$ is the linear map corresponding to $g$ in the representation $F(f(i))$.

Let $F : \text{Discrete } C \to \text{Rep}_k G$ be a functor that assigns a representation of a group $G$ over a field $k$ to each "color" in $C$. For any object $f \in \text{OverColor } C$ (consisting of an indexing set $I$ and a mapping $f.\text{hom} : I \to C$) and any group element $M \in G$, the linear map $(\text{toRep } F f).\rho(M)$ representing the action of $M$ on the tensor product representation $\text{toRep } F f$ is equal to the tensor product of the linear maps representing the action of $M$ on each constituent representation $F(f(i))$. Mathematically, this is expressed as: $$(\text{toRep } F f).\rho(M) = \bigotimes_{i \in I} (F(f(i))).\rho(M)$$ where the right-hand side denotes the linear map on the tensor product space induced by the collection of individual group actions.

Let $F : \text{Discrete } C \to \text{Rep}_k G$ be a functor that assigns a representation of a group $G$ over a field $k$ to each color in $C$. For an object $f \in \text{OverColor } C$, which consists of an indexing set $I$ and a mapping $f.\text{hom} : I \to C$, let $\text{toRep } F f$ be the representation defined by the tensor product of the representations $F(f.\text{hom}(i))$ for $i \in I$. For any group element $M \in G$ and any collection of vectors $\{x_i\}_{i \in I}$ where $x_i$ belongs to the representation space of $F(f.\text{hom}(i))$, the action of $M$ on the elementary tensor $\bigotimes_{i \in I} x_i$ is equal to the elementary tensor of the individual actions: $$(\text{toRep } F f).\rho(M) \left( \bigotimes_{i \in I} x_i \right) = \bigotimes_{i \in I} \left( F(f.\text{hom}(i)).\rho(M) (x_i) \right)$$

Let $F : \text{Discrete } C \to \text{Rep}_k G$ be a functor that assigns a representation of a group $G$ over a field $k$ to each color in $C$. Let $\mathbb{1}_{\text{OverColor } C}$ denote the monoidal unit object in the category $\text{OverColor } C$ (which corresponds to an empty indexing set). For any group element $g \in G$, the linear map $(\text{toRep } F (\mathbb{1}_{\text{OverColor } C})).\rho(g)$ representing the action of $g$ on the resulting representation is the identity map: $$(\text{toRep } F \mathbb{1}).\rho(g) = \text{id}$$ This reflects the fact that the representation associated with the monoidal unit (an empty tensor product) is the trivial representation.

Let $F : \text{Discrete } C \to \text{Rep}_k G$ be a functor that assigns a representation of a group $G$ over a field $k$ to each color in $C$. Consider a mapping $c : \text{Fin } 0 \to C$, which defines an object in the category $\text{OverColor } C$ indexed by the empty set $\text{Fin } 0$. For any group element $g \in G$, the linear map $(\text{toRep } F (\text{OverColor.mk } c)).\rho(g)$ representing the action of $g$ on the associated tensor product representation is the identity map: $$(\text{toRep } F (\text{OverColor.mk } c)).\rho(g) = \text{id}$$ This result confirms that the representation formed from an empty collection of indices (using the specific index set $\text{Fin } 0$) is the trivial representation.

Let $C$ be a collection of colors and $F : \text{Discrete } C \to \text{Rep}_k G$ be a functor that assigns a representation of a group $G$ over a field $k$ to each color. For any object $f$ in the category $\text{OverColor } C$, which consists of an indexing set $I$ (referred to as $f.\text{left}$) and a mapping $f.\text{hom} : I \to C$, the underlying vector space of the representation $\text{toRep } F f$ is the tensor product over $k$ of the vector spaces of the representations assigned to each color $f(i)$: $$(\text{toRep } F f).V = \bigotimes_{i \in I} (F(f(i))).V$$

Let $C$ be a set of colors and $F : \text{Discrete } C \to \text{Rep}_k(G)$ be a functor that assigns a representation of a group $G$ over a field $k$ to each color. Given two colors $c_1, c_2 \in C$ and a proof $h: c_1 = c_2$ of their equality, this definition provides the $k$-linear equivalence between the underlying vector spaces of the representations $F(c_1)$ and $F(c_2)$, denoted as $(F(c_1)).V \cong_k (F(c_2)).V$. This isomorphism is induced by the functorial image of the unique isomorphism in the discrete category corresponding to the equality $h$.

Let $C$ be a set of colors and $F : \text{Discrete } C \to \text{Rep}_k(G)$ be a functor that assigns a representation of a group $G$ over a field $k$ to each color. Given two colors $c_1, c_2 \in C$ and a proof $h$ that they are equal, let $\phi_h: (F(c_1)).V \cong_k (F(c_2)).V$ be the $k$-linear equivalence between the underlying vector spaces of the representations induced by the equality. For any group element $M \in G$ and any vector $x$ in the representation $F(c_1)$, applying the isomorphism $\phi_h$ commutes with the representation action $\rho$: $$\phi_h((F(c_1)).\rho(M, x)) = (F(c_2)).\rho(M, \phi_h(x))$$

Let $k$ be a field, $G$ be a group, and $F : \text{Discrete } C \to \text{Rep}_k G$ be a functor mapping each "color" $c \in C$ to a representation of $G$. Given two objects $f, g \in \text{OverColor } C$ (representing collections of colors indexed by sets $I$ and $J$ respectively) and a morphism $m : f \to g$, this definition provides a $k$-linear equivalence between the underlying vector spaces of the associated tensor product representations: $$(\text{toRep } F f).V \simeq_k (\text{toRep } F g).V$$ The isomorphism is constructed by reindexing the factors of the tensor product $\bigotimes_{i \in I} V_{f(i)}$ using the bijection $m : I \to J$ and applying the linear isomorphisms induced by the identity of colors $f(i) = g(m(i))$ for each index.

Let $k$ be a field, $G$ a group, and $C$ a set of colors. Let $F : \text{Discrete } C \to \text{Rep}_k G$ be a functor assigning a representation to each color. For any two objects $f, g \in \text{OverColor } C$ (with indexing sets $I$ and $J$ respectively) and a morphism $m : f \to g$ (defined by a bijection $\sigma : I \to J$ such that the colors match), let $\phi_m : (\text{toRep } F f).V \cong (\text{toRep } F g).V$ be the induced $k$-linear isomorphism between the tensor product spaces. For any family of vectors $x_i \in (F(f(i))).V$, the isomorphism $\phi_m$ maps the elementary tensor product $\bigotimes_{i \in I} x_i$ to an elementary tensor product in $J$ as follows: $$\phi_m \left( \bigotimes_{i \in I} x_i \right) = \bigotimes_{j \in J} \psi_j(x_{\sigma^{-1}(j)})$$ where $\psi_j : (F(f(\sigma^{-1}(j)))).V \cong (F(g(j))).V$ is the linear isomorphism induced by the color equality $f(\sigma^{-1}(j)) = g(j)$.

Let $k$ be a field, $G$ be a group, and $F: \text{Discrete } C \to \text{Rep}_k G$ be a functor mapping each "color" $c \in C$ to a representation $V_c$. For any morphism $m: f \to g$ in $\text{OverColor } C$ (where $f$ and $g$ represent collections of colors indexed by sets $I$ and $J$ respectively, and $m$ is a color-preserving bijection $\sigma: I \to J$), this definition constructs a $G$-representation homomorphism: $$\Phi_m : \text{toRep } F f \longrightarrow \text{toRep } F g$$ The underlying linear map of $\Phi_m$ is the isomorphism that reindexes the factors of the tensor product $\bigotimes_{i \in I} V_{f(i)}$ into $\bigotimes_{j \in J} V_{g(j)}$ using the bijection $\sigma$. This map is shown to be an intertwiner, meaning it commutes with the action of $G$ on the tensor product representations.

Let $k$ be a field, $G$ a group, and $C$ a set of colors. Let $F : \text{Discrete } C \to \text{Rep}_k G$ be a functor mapping each color $c \in C$ to a representation $V_c$. For any two objects $X, Y \in \text{OverColor } C$ (with indexing sets $I$ and $J$ respectively) and a morphism $f : X \to Y$ (defined by a color-preserving bijection $\sigma : I \to J$), let $\Phi_f : \text{toRep } F X \to \text{toRep } F Y$ be the induced homomorphism between the tensor product representations. Given a family of vectors $x_i \in V_{X(i)}$ for each $i \in I$, the action of $\Phi_f$ on the elementary tensor product is given by: $$\Phi_f \left( \bigotimes_{i \in I} x_i \right) = \bigotimes_{j \in J} \psi_j(x_{\sigma^{-1}(j)})$$ where $\psi_j : V_{X(\sigma^{-1}(j))} \to V_{Y(j)}$ is the $k$-linear isomorphism induced by the equality of colors $X(\sigma^{-1}(j)) = Y(j)$.

Let $k$ be a field, $G$ a group, and $C$ a set of colors. Let $F : \text{Discrete } C \to \text{Rep}_k G$ be a functor mapping colors to representations. For any object $X$ in the category $\text{OverColor } C$, the representation homomorphism $\Phi_{\text{id}_X}$ induced by the identity morphism $\text{id}_X$ on $X$ is equal to the identity morphism $\text{id}_{\text{toRep } F X}$ on the associated tensor product representation.

Let $k$ be a field, $G$ a group, and $C$ a set of colors. Let $F : \text{Discrete } C \to \text{Rep}_k G$ be a functor mapping colors to representations. For any objects $X, Y, Z$ in the category $\text{OverColor } C$ and morphisms $f : X \to Y$ and $g : Y \to Z$, the representation homomorphism $\Phi_{g \circ f}$ induced by the composition $g \circ f$ is equal to the composition of the individual representation homomorphisms induced by $f$ and $g$, denoted $\Phi_g \circ \Phi_f$.

Let $k$ be a field, $G$ be a group, and $C$ be a set of "colors". Given a functor $F : \text{Discrete } C \to \text{Rep}_k G$ that assigns a representation to each color, `toRepFunc` is the functor from the category of indexed colors $\text{OverColor } C$ to the category of representations $\text{Rep}_k G$. For an object $f \in \text{OverColor } C$ (an indexing set $I$ with a coloring map $f : I \to C$), the functor assigns the representation: $$\text{toRep } F f = \bigotimes_{i \in I} F(f(i))$$ For a morphism $m : f \to g$ in $\text{OverColor } C$ (a color-preserving bijection between the indexing sets), the functor assigns the representation homomorphism $\Phi_m$ that reindexes the factors of the tensor product.

Let $k$ be a field, $G$ be a group, and $C$ be a type of "colors". Given a functor $F : \text{Discrete } C \to \text{Rep}_k G$ that assigns a representation of $G$ to each color, let $\text{toRep } F : \text{OverColor } C \to \text{Rep}_k G$ be the functor that maps an object in $\text{OverColor } C$ (an indexed collection of colors) to its corresponding tensor product representation. The definition `toRepUnitIso` is an isomorphism in the category of representations $\text{Rep}_k G$: $$\mathbb{1}_{\text{Rep}_k G} \cong \text{toRep } F(\mathbb{1}_{\text{OverColor } C})$$ where $\mathbb{1}_{\text{Rep}_k G}$ is the monoidal unit of representations (the trivial representation on $k$) and $\mathbb{1}_{\text{OverColor } C}$ is the monoidal unit in $\text{OverColor } C$ (representing an empty set of indices). This isomorphism is induced by the canonical linear equivalence between the base field $k$ and the tensor product over an empty index set, $\bigotimes_{i \in \emptyset} V_i \cong k$.

Let $C$ be a type of colors, $k$ a field, and $G$ a group. Given a functor $F : \text{Discrete } C \to \text{Rep}_k G$ that assigns a representation to each color, and two types (indexing sets) $X$ and $Y$ with coloring maps $c_X : X \to C$ and $c_Y : Y \to C$, let $i \in X \oplus Y$ be an element of the disjoint union of the indexing sets. The definition `discreteSumEquiv` provides a linear equivalence between the representation associated with $i$ when viewed as an element of the individual components $X$ or $Y$, and the representation associated with $i$ via the combined coloring map $c_X \oplus c_Y : X \oplus Y \to C$. Specifically, if $i = \text{inl}(x)$, the equivalence identifies $F(c_X(x))$ with $F((c_X \oplus c_Y)(\text{inl}(x)))$; if $i = \text{inr}(y)$, it identifies $F(c_Y(y))$ with $F((c_X \oplus c_Y)(\text{inr}(y)))$. Since these objects are definitionally equal, the equivalence is the identity map $\text{id}$.

Let $C$ be a type of colors, $k$ a field, and $G$ a group. Given a functor $F : \text{Discrete } C \to \text{Rep}_k G$ that assigns a representation to each color, and two objects $X, Y$ in the category $\text{OverColor } C$, let $V_X$ and $V_Y$ be the underlying $k$-vector spaces of the representations `toRep F X` and `toRep F Y` respectively. The definition `μModEquiv` provides a $k$-linear equivalence: $$(V_X \otimes_k V_Y) \cong V_{X \otimes Y}$$ where $V_{X \otimes Y}$ is the vector space of the representation associated with the monoidal product $X \otimes Y$ in $\text{OverColor } C$. This equivalence identifies the tensor product of two $\Pi$-tensor products (indexed by the indexing sets of $X$ and $Y$) with a single $\Pi$-tensor product indexed by the disjoint union of those sets. It is constructed by composing the standard equivalence for tensor products of $\Pi$-tensor products (`tmulEquiv`) with the linear equivalence that identifies the colored indices across the sum (`discreteSumEquiv`).

Let $C$ be a type of colors, $k$ a field, and $G$ a group. Given a functor $F : \text{Discrete } C \to \text{Rep}_k G$ that assigns a representation to each color, let $X$ and $Y$ be objects in $\text{OverColor } C$ with indexing sets $I_X$ and $I_Y$ respectively. Let $p = (p_i)_{i \in I_X}$ and $q = (q_j)_{j \in I_Y}$ be families of vectors such that each $p_i$ and $q_j$ belong to the representations associated with the colors of the respective indices. The theorem states that the linear equivalence $\mu\text{ModEquiv}$ maps the tensor product of the pure tensors corresponding to $p$ and $q$ to a pure tensor over the disjoint union $I_X \oplus I_Y$: $$\mu\text{ModEquiv}(F, X, Y) \left( \left( \bigotimes_{i \in I_X} p_i \right) \otimes \left( \bigotimes_{j \in I_Y} q_j \right) \right) = \bigotimes_{k \in I_X \oplus I_Y} \text{discreteSumEquiv}(F, k)(\text{elim}(p, q, k))$$ where $\text{elim}(p, q, \cdot)$ is the function on $I_X \oplus I_Y$ that returns $p_i$ for an element in the left summand and $q_j$ for an element in the right summand, and $\text{discreteSumEquiv}$ is the canonical identification of the corresponding representation spaces.

Let $C$ be a type of colors, $k$ a field, and $G$ a group. Given a functor $F : \text{Discrete } C \to \text{Rep}_k G$ that assigns a representation to each color, and two objects $X, Y$ in the category $\text{OverColor } C$, the definition $\mu$ is the isomorphism of representations: $$\text{toRep } F X \otimes \text{toRep } F Y \cong \text{toRep } F (X \otimes Y)$$ where $\text{toRep } F X$ and $\text{toRep } F Y$ are the representations associated with $X$ and $Y$ (constructed as tensor products of the representations of their constituent colors), and $X \otimes Y$ is the monoidal product in $\text{OverColor } C$. This isomorphism lifts the linear equivalence $\mu\text{ModEquiv}$ between the underlying vector spaces to the category of representations, showing that the identification of indexing sets via disjoint union is compatible with the group action.

Let $C$ be a type of colors, $k$ a field, and $G$ a group. Given a functor $F : \text{Discrete } C \to \text{Rep}_k G$ that assigns a representation to each color, let $X$ and $Y$ be objects in $\text{OverColor } C$ with indexing sets $I_X$ and $I_Y$. Let $p = (p_i)_{i \in I_X}$ and $q = (q_j)_{j \in I_Y}$ be families of vectors such that each $p_i$ and $q_j$ belong to the representations associated with the colors of the respective indices. The monoidal coherence isomorphism $\mu : \text{toRep } F X \otimes \text{toRep } F Y \cong \text{toRep } F (X \otimes Y)$ satisfies the property that the image of the tensor product of the pure tensors for $p$ and $q$ is the pure tensor on the combined index set $I_X \oplus I_Y$: $$\mu \left( \left( \bigotimes_{i \in I_X} p_i \right) \otimes \left( \bigotimes_{j \in I_Y} q_j \right) \right) = \bigotimes_{k \in I_X \oplus I_Y} \text{discreteSumEquiv}(F, k)(\text{elim}(p, q, k))$$ where $\text{elim}(p, q, k)$ returns $p_i$ for $k = \text{inl}(i)$ and $q_j$ for $k = \text{inr}(j)$, and $\text{discreteSumEquiv}$ is the canonical linear identification between the representation spaces.

Let $C$ be a type of colors, $k$ a field, and $G$ a group. Let $F : \text{Discrete } C \to \text{Rep}_k G$ be a functor that assigns a representation to each color. For any types $X, Y$ with coloring maps $c_X : X \to C$ and $c_Y : Y \to C$, let $p = (p_i)_{i \in X}$ and $q = (q_j)_{j \in Y}$ be families of vectors such that each $p_i$ and $q_j$ belong to the representations associated with their respective colors. The isomorphism $\mu$ between the tensor product of representations $\text{toRep } F (X, c_X) \otimes \text{toRep } F (Y, c_Y)$ and the representation of the combined system $\text{toRep } F (X \oplus Y, c_X \oplus c_Y)$ satisfies: $$\mu \left( \left( \bigotimes_{i \in X} p_i \right) \otimes \left( \bigotimes_{j \in Y} q_j \right) \right) = \bigotimes_{k \in X \oplus Y} \text{discreteSumEquiv}(F, k)(\text{elim}(p, q, k))$$ where $\text{elim}(p, q, k)$ is the vector $p_i$ if $k = \text{inl}(i)$ and $q_j$ if $k = \text{inr}(j)$, and $\text{discreteSumEquiv}$ is the canonical linear equivalence between the corresponding representation spaces.

Let $C$ be a set of colors, $k$ a field, and $G$ a group. Let $F : \text{Discrete } C \to \text{Rep}_k G$ be a functor that assigns a representation to each color. For any objects $X, Y, Z$ in the category $\text{OverColor } C$ and a morphism $f : X \to Y$, let $\text{toRep } F$ denote the associated tensor product representation and $\Phi_f : \text{toRep } F X \to \text{toRep } F Y$ be the representation homomorphism induced by $f$. The monoidal natural isomorphism $\mu$ between the tensor product of representations and the representation of the monoidal product satisfies the left naturality condition: $$\mu_{Y, Z} \circ (\Phi_f \otimes \text{id}_{\text{toRep } F Z}) = \Phi_{f \otimes \text{id}_Z} \circ \mu_{X, Z}$$ where $\circ$ denotes the composition of homomorphisms and $\otimes$ denotes the monoidal product in the category of representations and in $\text{OverColor } C$.

Let $k$ be a field, $G$ a group, and $C$ a set of colors. Let $F : \text{Discrete } C \to \text{Rep}_k G$ be a functor mapping each color $c \in C$ to a representation $V_c$. For any objects $X, Y, X' \in \text{OverColor } C$ and a morphism $f : X \to Y$ (a color-preserving bijection), let $\text{toRep } F X$ be the representation formed by the tensor product of the components of $X$, and let $\Phi_f : \text{toRep } F X \to \text{toRep } F Y$ be the induced representation homomorphism. The monoidal coherence isomorphism $\mu_{A, B} : \text{toRep } F A \otimes \text{toRep } F B \cong \text{toRep } F (A \otimes B)$ satisfies the naturality condition: $$(\text{id}_{\text{toRep } F X'} \otimes \Phi_f) \gg \mu_{X', Y} = \mu_{X', X} \gg \Phi_{\text{id}_{X'} \otimes f}$$ where $\gg$ denotes the composition of morphisms in the category of representations, and $\text{id}_{X'} \otimes f$ is the morphism in $\text{OverColor } C$ corresponding to the whisker-left operation.

Let $C$ be a collection of colors, and $F : \text{Discrete } C \to \text{Rep}_k G$ be a functor that assigns a representation of a group $G$ over a field $k$ to each color. For any objects $X, Y, Z$ in the category $\text{OverColor } C$, let $V_X, V_Y, V_Z$ be the corresponding tensor product representations in $\text{Rep}_k G$. Let $\mu_{A,B} : V_A \otimes V_B \cong V_{A \otimes B}$ be the natural isomorphism that identifies the tensor products of representations, and let $\Phi(f) : V_A \to V_B$ be the representation homomorphism induced by a morphism $f : A \to B$ in $\text{OverColor } C$. Then the following diagram of isomorphisms commutes: $$\Phi(\alpha_{X, Y, Z}) \circ \mu_{X \otimes Y, Z} \circ (\mu_{X, Y} \otimes \text{id}_{V_Z}) = \mu_{X, Y \otimes Z} \circ (\text{id}_{V_X} \otimes \mu_{Y, Z}) \circ \alpha_{V_X, V_Y, V_Z}$$ where $\alpha_{X, Y, Z} : (X \otimes Y) \otimes Z \cong X \otimes (Y \otimes Z)$ is the associator in $\text{OverColor } C$ and $\alpha_{V_X, V_Y, V_Z} : (V_X \otimes V_Y) \otimes V_Z \cong V_X \otimes (V_Y \otimes V_Z)$ is the associator in the category of representations.

Let $k$ be a field, $G$ a group, and $C$ a type of colors. Given a functor $F: \text{Discrete } C \to \text{Rep}_k G$ that maps colors to representations, let $\text{toRep } F: \text{OverColor } C \to \text{Rep}_k G$ be the induced functor that maps an indexed collection of colors to its tensor product representation. For any object $X \in \text{OverColor } C$, the left unitor $\lambda_{\text{toRep } F X}: \mathbb{1}_{\text{Rep}_k G} \otimes \text{toRep } F X \cong \text{toRep } F X$ in the category of representations is equal to the composition of: 1. The unit isomorphism $\iota \otimes \text{id}_{\text{toRep } F X}$, where $\iota: \mathbb{1}_{\text{Rep}_k G} \cong \text{toRep } F(\mathbb{1}_{\text{OverColor } C})$ identifies the trivial representation with the representation of the empty index set. 2. The monoidal isomorphism $\mu_{\mathbb{1}, X}: \text{toRep } F(\mathbb{1}_{\text{OverColor } C}) \otimes \text{toRep } F X \cong \text{toRep } F(\mathbb{1}_{\text{OverColor } C} \otimes X)$. 3. The representation homomorphism $\Phi(\lambda_X): \text{toRep } F(\mathbb{1}_{\text{OverColor } C} \otimes X) \to \text{toRep } F X$ induced by the left unitor $\lambda_X: \mathbb{1}_{\text{OverColor } C} \otimes X \cong X$ in the category $\text{OverColor } C$. Mathematically, this is expressed as: $$\lambda_{\text{toRep } F X} = (\iota \otimes \text{id}_{\text{toRep } F X}) \gg \mu_{\mathbb{1}, X} \gg \Phi(\lambda_X)$$

Let $k$ be a field, $G$ a group, and $C$ a set of colors. Given a functor $F : \text{Discrete } C \to \text{Rep}_k G$ that assigns a representation to each color, let $\text{toRep } F : \text{OverColor } C \to \text{Rep}_k G$ be the functor that maps an indexed collection of colors to its tensor product representation. For any object $X \in \text{OverColor } C$, the right unitor $\rho_{\text{toRep } F X} : \text{toRep } F X \otimes \mathbb{1}_{\text{Rep}_k G} \to \text{toRep } F X$ in the category of representations satisfies the following coherence condition: $$\rho_{\text{toRep } F X} = \Phi_{\rho_X} \circ \mu_{X, \mathbb{1}} \circ (\text{id}_{\text{toRep } F X} \otimes \eta)$$ where: - $\eta : \mathbb{1}_{\text{Rep}_k G} \cong \text{toRep } F (\mathbb{1}_{\text{OverColor } C})$ is the unit isomorphism mapping the trivial representation to the representation of the empty index set. - $\mu_{X, \mathbb{1}} : \text{toRep } F X \otimes \text{toRep } F (\mathbb{1}_{\text{OverColor } C}) \cong \text{toRep } F (X \otimes \mathbb{1}_{\text{OverColor } C})$ is the monoidal coherence isomorphism. - $\Phi_{\rho_X} : \text{toRep } F (X \otimes \mathbb{1}_{\text{OverColor } C}) \to \text{toRep } F X$ is the representation homomorphism induced by the right unitor $\rho_X : X \otimes \mathbb{1}_{\text{OverColor } C} \to X$ in the category $\text{OverColor } C$.

Let $C$ be a type of colors, $k$ a field, and $G$ a group. Given a functor $F : \text{Discrete } C \to \text{Rep}_k G$ that assigns a representation to each color, let $X$ and $Y$ be objects in the category $\text{OverColor } C$. The monoidal coherence isomorphism $\mu_{X,Y} : \text{toRep } F X \otimes \text{toRep } F Y \cong \text{toRep } F (X \otimes Y)$ and the representation homomorphism $\text{homToRepHom } F (\beta_{X,Y})$ induced by the braiding $\beta_{X,Y} : X \otimes Y \cong Y \otimes X$ in $\text{OverColor } C$ satisfy the following compatibility relation with the braiding $\beta$ in the category of representations: $$\mu_{X,Y} \gg \text{homToRepHom } F (\beta_{X,Y}) = \beta_{\text{toRep } F X, \text{toRep } F Y} \gg \mu_{Y,X}$$ where $\gg$ denotes the composition of morphisms in $\text{Rep}_k G$.

Let $C$ be a type of colors, $k$ a field, and $G$ a group. Given a functor $F : \text{Discrete } C \to \text{Rep}_k G$ that assigns a representation to each color, let $X$ and $Y$ be objects in the category $\text{OverColor } C$. The representation homomorphism $\text{homToRepHom } F (\beta_{X,Y})$ induced by the braiding $\beta_{X,Y} : X \otimes Y \cong Y \otimes X$ in $\text{OverColor } C$ is equal to the following composition of morphisms in $\text{Rep}_k G$: $$\text{homToRepHom } F (\beta_{X,Y}) = \mu_{X,Y}^{-1} \gg \beta_{\text{toRep } F X, \text{toRep } F Y} \gg \mu_{Y,X}$$ where: - $\mu_{X,Y} : \text{toRep } F X \otimes \text{toRep } F Y \cong \text{toRep } F (X \otimes Y)$ is the monoidal coherence isomorphism associated with the lifting of $F$. - $\beta_{\text{toRep } F X, \text{toRep } F Y}$ is the braiding isomorphism in the category of representations $\text{Rep}_k G$. - $\gg$ denotes the composition of morphisms in diagrammatic order.

Let $k$ be a field, $G$ be a group, and $C$ be a set of colors. Given a functor $F : \text{Discrete } C \to \text{Rep}_k G$ that assigns a representation to each color, let $\mathcal{T}_F : \text{OverColor } C \to \text{Rep}_k G$ be the induced representation functor (which maps an indexed collection of colors to the tensor product of their corresponding representations). The structure `toRepFunc_laxBraidedFunctor` defines $\mathcal{T}_F$ as a lax braided monoidal functor. This structure is equipped with: 1. A unit morphism $\epsilon : \mathbb{1}_{\text{Rep}_k G} \to \mathcal{T}_F(\mathbb{1}_{\text{OverColor } C})$ mapping the trivial representation to the representation of the empty set of indices. 2. A natural transformation $\mu_{X,Y} : \mathcal{T}_F(X) \otimes \mathcal{T}_F(Y) \to \mathcal{T}_F(X \otimes Y)$ for any objects $X, Y \in \text{OverColor } C$. 3. The compatibility condition with the braiding $\beta$: $$\mathcal{T}_F(\beta_{X,Y}) \circ \mu_{X,Y} = \mu_{Y,X} \circ \beta_{\mathcal{T}_F(X), \mathcal{T}_F(Y)}$$ where $\beta_{X,Y}$ is the braiding in $\text{OverColor } C$ and $\beta_{\mathcal{T}_F(X), \mathcal{T}_F(Y)}$ is the braiding in the category of representations. It also satisfies the standard coherence axioms for associativity and unitality.