Physlib.Relativity.Tensors.Color.Basic

Given a type $C$ representing the set of colors (index types) for tensors, $\text{OverColor}(C)$ is the core of the slice category $\text{Type}/C$. The objects of this category are maps $f: X \to C$, where $X$ is a type representing a collection of indices and $f$ assigns a color to each index. The morphisms are the isomorphisms of the slice category, which correspond to color-preserving bijections $\sigma: X \cong Y$ such that $g \circ \sigma = f$ for objects $f: X \to C$ and $g: Y \to C$.

For a given type $C$ of colors, the category $\text{OverColor}(C)$ is a groupoid. This means that every morphism in $\text{OverColor}(C)$—which represents a color-preserving bijection between two types of indices $X$ and $Y$—is an isomorphism. This groupoid structure is derived from the fact that $\text{OverColor}(C)$ is defined as the core of the slice category $\text{Type}/C$.

Given a mapping $f: X \to C$ from a type of indices $X$ to a type of colors $C$, this function constructs the corresponding object in the category $\text{OverColor}(C)$. In the context of tensor indices, this represents the assignment of a specific color to each index in a collection.

For an object $f$ in the category $\text{OverColor}(C)$, the function `hom` returns the underlying map $f: X \to C$ that assigns a color in $C$ to each index in the type $X$. In the context of the slice category $\text{Type}/C$, this corresponds to the morphism from the domain $X$ to the base $C$.

For an object $f$ in the category $\text{OverColor}(C)$, which represents a mapping $f: X \to C$ from a type of indices $X$ to a type of colors $C$, the function returns the underlying type $X$ of the indices.

Let $X$ be a type of indices and $C$ be a type of colors. For any mapping $f: X \to C$, the underlying map of the object $\text{mk}(f)$ in the category $\text{OverColor}(C)$, denoted as $(\text{mk } f).\text{hom}$, is equal to $f$.

Let $X$ be a type of indices and $C$ be a type of colors. For any mapping $f : X \to C$, the underlying type of indices associated with the object constructed by $\text{mk}(f)$ in the category $\text{OverColor}(C)$ is equal to $X$.

Given objects $f: X \to C$ and $g: Y \to C$ in the category $\text{OverColor}(C)$, where $X$ and $Y$ are types of indices and $C$ is the type of colors, a morphism $m: f \to g$ represents a color-preserving bijection between the indices. The function `hom` extracts the underlying bijection $\sigma: X \to Y$ associated with $m$, which satisfies the property $g \circ \sigma = f$.

Given objects $f: X \to C$ and $g: Y \to C$ in the category $\text{OverColor}(C)$, where $X$ and $Y$ are types of indices and $C$ is the type of colors, a morphism $m: f \to g$ represents a color-preserving bijection. The function `inv` extracts the underlying inverse bijection $\sigma^{-1}: Y \to X$ associated with $m$, which satisfies the property $f \circ \sigma^{-1} = g$.

In the category $\text{OverColor}(C)$, where objects are mappings $f: X \to C$ representing the assignment of colors to a set of indices $X$ and morphisms are color-preserving bijections, for any morphism $m: f \to g$, the composition of its forward morphism $m.\text{hom}$ and its inverse $m.\text{inv}$ is the identity morphism $\mathbb{1}_f$ on the object $f$.

In the category $\text{OverColor}(C)$, where objects are mappings $f: X \to C$ and $g: Y \to C$ representing the assignment of colors to sets of indices $X$ and $Y$, and morphisms are color-preserving bijections, for any morphism $m: f \to g$, the composition of its inverse morphism $m.\text{inv}$ and its forward morphism $m.\text{hom}$ is the identity morphism $\mathbb{1}_g$ on the target object $g$.

In the category $\text{OverColor}(C)$, an object is defined as a map $f : X \to C$ that assigns a color from the set $C$ to each index in the set $X$. A morphism $m : f \to g$ between two such objects $f : X \to C$ and $g : Y \to C$ represents a color-preserving bijection between the index sets $X$ and $Y$. Since $\text{OverColor}(C)$ is a groupoid, every such morphism is an isomorphism; this definition provides the inverse morphism $m^{-1} : g \to f$, corresponding to the inverse bijection of the underlying index sets.

In the category $\text{OverColor}(C)$, let $f: X \to C$ and $g: Y \to C$ be objects representing the assignment of colors to sets of indices $X$ and $Y$. For any two morphisms $m, n : f \to g$, if the underlying color-preserving bijections $m.\text{hom}$ and $n.\text{hom}$ (which are the morphisms in the slice category $\text{Type}/C$) are equal, then $m = n$.

In the category $\text{OverColor}(C)$, let $f: X \to C$ and $g: Y \to C$ be objects representing the assignment of colors from the set $C$ to the sets of indices $X$ and $Y$. For any two morphisms $m, n : f \to g$, representing color-preserving bijections between the index sets, $m$ and $n$ are equal if and only if for every index $x \in X$, their underlying functions $\sigma_m, \sigma_n : X \to Y$ satisfy $\sigma_m(x) = \sigma_n(x)$.

For a morphism $m: f \to g$ in the category $\text{OverColor}(C)$, where $f: X \to C$ and $g: Y \to C$ are objects representing the assignment of colors to sets of indices $X$ and $Y$, this function returns the underlying bijection (equivalence) between the types of indices $\sigma: X \simeq Y$. Since $\text{OverColor}(C)$ is the core of the slice category over $C$, the morphism $m$ uniquely determines a bijection that preserves colors, such that $g \circ \sigma = f$.

For any object $f$ in the category $\text{OverColor}(C)$, representing a mapping $f: X \to C$ from a type of indices $X$ to a type of colors $C$, the underlying bijection $\sigma: X \simeq X$ induced by the identity morphism $\mathbb{1}_f$ is the reflexive (identity) equivalence on $X$.

In the category $\text{OverColor}(C)$, for any objects $f, g, h$ and morphisms $m: f \to g$ and $n: g \to h$, the equivalence between the underlying types of indices induced by the composition of morphisms $m \gg n$ is equal to the composition of the individual equivalences induced by $m$ and $n$. That is, $$\text{toEquiv}(m \gg n) = \text{toEquiv}(m) \circ \text{toEquiv}(n)$$ where $\text{toEquiv}$ denotes the function that extracts the underlying color-preserving bijection (equivalence) between the index types of the objects, and $\circ$ denotes the composition of equivalences.

Let $C$ be a type of colors. Let $f: X \to C$ and $g: Y \to C$ be objects in the category $\text{OverColor}(C)$, and let $m: f \to g$ be a morphism. Let $\sigma: X \cong Y$ be the bijection between the index types induced by $m$. For any index $i \in Y$, the color assigned by $f$ to the image of $i$ under the inverse bijection $\sigma^{-1}$ is equal to the color assigned by $g$ to $i$, i.e., $f(\sigma^{-1}(i)) = g(i)$.

Let $C$ be a type representing colors. For any morphism $m: f \to g$ in the category $\text{OverColor}(C)$, where $f: X \to C$ and $g: Y \to C$ are objects assigning colors to index types $X$ and $Y$ respectively, let $\sigma: X \cong Y$ be the underlying bijection (equivalence) induced by $m$. Then the composition of $g$ with $\sigma$ is equal to $f$, that is, $g \circ \sigma = f$.

In the category $\text{OverColor}(C)$, let $m: f \to g$ be a morphism between two objects $f: X \to C$ and $g: Y \to C$, where $X$ and $Y$ are sets of indices and $C$ is the set of colors. Let $\sigma: X \cong Y$ be the color-preserving bijection between the index types induced by $m$. For any index $i \in Y$, the color assigned to the index $\sigma^{-1}(i)$ by the map $f$ is equal to the color assigned to the index $i$ by the map $g$. That is: $$f(\sigma^{-1}(i)) = g(i)$$

Let $C$ be a type representing colors for tensor indices. In the category $\text{OverColor}(C)$, let $f: X \to C$ and $g: Y \to C$ be two objects, and let $m: f \to g$ be a morphism between them. Let $\sigma: X \simeq Y$ be the color-preserving bijection between the sets of indices induced by $m$. For any index $i \in X$, the color assigned to $i$ by $f$ is equal to the color assigned to its image $\sigma(i)$ by $g$, that is: $$f(i) = g(\sigma(i)).$$

Given a morphism $m: f \to g$ in the category $\text{OverColor}(C)$, which represents a color-preserving bijection between two objects $f: X \to C$ and $g: Y \to C$, this definition constructs the corresponding categorical isomorphism $f \cong g$. The isomorphism is formed using $m$ as the forward map and its inverse $m^{-1}$ as the backward map.

Let $C$ be a type representing colors of tensor indices. In the category $\text{OverColor}(C)$ (the core of the slice category over $C$), let $m: f \to g$ and $n: g \to h$ be morphisms representing color-preserving bijections between sets of indices. The underlying bijection associated with the composite morphism $m \gg n$ is equal to the composition of the underlying bijections of $m$ and $n$, that is, $(m \gg n).\text{hom} = m.\text{hom} \gg n.\text{hom}$.

For a given type of colors $C$, the category $\text{OverColor}(C)$ (the core of the slice category $\text{Type}/C$) is equipped with a monoidal category structure defined using the disjoint union of index sets. - The **tensor product** of two objects $f: X \to C$ and $g: Y \to C$ is given by the map $f \oplus g: X \amalg Y \to C$, which applies $f$ to elements of $X$ and $g$ to elements of $Y$. - The **monoidal unit** is the unique map $\text{empty\_elim} : \emptyset \to C$ from the empty type. - The **associator**, **left unitor**, and **right unitor** are the isomorphisms in $\text{OverColor}(C)$ induced by the standard set-theoretic bijections $(X \amalg Y) \amalg Z \cong X \amalg (Y \amalg Z)$, $\emptyset \amalg X \cong X$, and $X \amalg \emptyset \cong X$, respectively.

For a given type of colors $C$, the category $\text{OverColor}(C)$—defined as the core of the slice category $\text{Type}/C$—is a monoidal category. The monoidal structure is defined by: - The **tensor product** of two objects $f: X \to C$ and $g: Y \to C$ is the map $f \otimes g: X \amalg Y \to C$, which acts as $f$ on the first component and $g$ on the second. - The **monoidal unit** is the unique map $\mathbf{1}: \emptyset \to C$ from the empty set. - The **associator** $\alpha_{f,g,h}: (f \otimes g) \otimes h \cong f \otimes (g \otimes h)$, **left unitor** $\lambda_f: \mathbf{1} \otimes f \cong f$, and **right unitor** $\rho_f: f \otimes \mathbf{1} \cong f$ are the isomorphisms induced by the canonical set-theoretic bijections for disjoint unions. This definition provides the proofs that these components satisfy the monoidal category axioms, including the pentagon and triangle identities.

The category $\text{OverColor}(C)$ is a braided monoidal category. For any two objects $f: X \to C$ and $g: Y \to C$, the braiding $\beta_{f,g}: f \otimes g \cong g \otimes f$ is the isomorphism in $\text{OverColor}(C)$ induced by the canonical bijection $\sigma: X \amalg Y \cong Y \amalg X$ that swaps the components of the disjoint union. This bijection preserves colors, such that $(g \otimes f) \circ \sigma = f \otimes g$. The definition includes proofs that this braiding is natural and satisfies the hexagon identities.

For a type $C$ representing colors, the category $\text{OverColor}(C)$ (defined as the core of the slice category $\text{Type}/C$) is a symmetric monoidal category. This symmetry is based on the braided monoidal structure where the braiding $\beta_{f,g}: f \otimes g \cong g \otimes f$ for objects $f: X \to C$ and $g: Y \to C$ is induced by the canonical swap map $\sigma: X \amalg Y \cong Y \amalg X$. The symmetry property ensures that $\beta_{g,f} \circ \beta_{f,g} = \text{id}_{f \otimes g}$ for all objects in the category.

Let $C$ be a type of colors and $n$ be a natural number. Let $f, g: \{0, \dots, n-1\} \to C$ be mappings that assign colors to a set of $n$ indices, defining two objects in the category $\text{OverColor}(C)$. For any two morphisms $\sigma, \sigma' : f \to g$, if their underlying bijections from $\{0, \dots, n-1\}$ to $\{0, \dots, n-1\}$ agree on all indices $i \in \{0, \dots, n-1\}$, then the morphisms are equal, $\sigma = \sigma'$.

Let $C$ be a type of colors and let $f: X \to C$ and $g: Y \to C$ be mappings representing two objects in the category $\text{OverColor}(C)$. The underlying bijection between the index sets $X \amalg Y$ and $Y \amalg X$ induced by the braiding isomorphism $\beta_{f,g}: f \otimes g \cong g \otimes f$ is the canonical swap map $\sigma: X \amalg Y \cong Y \amalg X$ that interchanges the two components of the disjoint union.

Let $C$ be a type of colors. For any two mappings $f: X \to C$ and $g: Y \to C$ representing objects in the category $\text{OverColor}(C)$, the bijection between the index sets $Y \amalg X$ and $X \amalg Y$ induced by the inverse braiding $\beta_{f,g}^{-1}: g \otimes f \cong f \otimes g$ is the canonical swap map $\sigma: Y \amalg X \cong X \amalg Y$ defined by swapping the order of the components in the disjoint union.

For any mappings $f: X \to C$, $g: Y \to C$, and $h: Z \to C$ representing objects in the category $\text{OverColor}(C)$ and any morphism $\sigma : f \to g$, the bijection between the index sets $Z \amalg X$ and $Z \amalg Y$ induced by the left whiskering $h \triangleleft \sigma$ (the tensor product $id_h \otimes \sigma$) is equal to the disjoint union of the identity bijection on $Z$ and the bijection between $X$ and $Y$ induced by $\sigma$.

For any mappings $f: X \to C$, $g: Y \to C$, and $h: Z \to C$ representing objects in the category $\text{OverColor}(C)$ and any morphism $\sigma : f \to g$, the bijection between the index sets $X \amalg Z$ and $Y \amalg Z$ induced by the right whiskering $\sigma \triangleright h$ is equal to the disjoint union of the bijection induced by $\sigma$ and the identity bijection on $Z$.

Let $C$ be a type representing the colors of tensor indices. For any objects $f: X \to C$, $g: Y \to C$, and $h: Z \to C$ in the category $\text{OverColor}(C)$, the associator isomorphism of the monoidal structure is denoted by $\alpha_{f,g,h} : (f \otimes g) \otimes h \cong f \otimes (g \otimes h)$. This theorem states that the underlying bijection (equivalence) of the morphism $\alpha_{f,g,h}.\text{hom}$ is the standard set-theoretic associativity for disjoint unions, $(X \amalg Y) \amalg Z \cong X \amalg (Y \amalg Z)$.

Let $C$ be a type of colors and let $f: X \to C$, $g: Y \to C$, and $h: Z \to C$ be objects in the category $\text{OverColor}(C)$. The category is equipped with a monoidal structure where the tensor product is given by the disjoint union of index sets. The underlying bijection of the inverse of the associator isomorphism $\alpha_{f,g,h}^{-1}: f \otimes (g \otimes h) \to (f \otimes g) \otimes h$ is exactly the inverse of the standard set-theoretic associativity for disjoint unions, $(X \amalg Y) \amalg Z \cong X \amalg (Y \amalg Z)$.

Let $C$ be a type representing colors of tensor indices. Given a coloring $c: X \to C$ of an index set $X$ and an equivalence (bijection) $e: X \cong Y$ between index sets, this definition constructs an isomorphism in the category $\text{OverColor}(C)$ between the object corresponding to $c$ and the object corresponding to the reindexed coloring $c \circ e^{-1} : Y \to C$. This isomorphism represents a color-preserving relabeling of indices from $X$ to $Y$.

Let $C$ be a type representing colors of tensor indices. For a coloring $c: X \to C$ of an index set $X$ and a bijection $e: X \cong Y$ between index sets, there is an induced isomorphism $\text{equivToIso}(e): c \cong c \circ e^{-1}$ in the category $\text{OverColor}(C)$. This theorem states that the underlying bijection of the forward morphism of this isomorphism is equal to $e$.

Let $C$ be a type representing colors of tensor indices. For a coloring $c: X \to C$ of an index set $X$ and a bijection $e: X \cong Y$ between index sets, there is an induced isomorphism $\text{equivToIso}(e): c \cong c \circ e^{-1}$ in the category $\text{OverColor}(C)$. This theorem states that the underlying bijection of the inverse of this isomorphism is equal to the inverse bijection $e^{-1}$.

Let $C$ be a type representing the colors of tensor indices. Given a coloring $c : X \to C$ of an index set $X$ and an equivalence (bijection) $e : X \cong Y$ between index sets $X$ and $Y$, this definition constructs a morphism in the category $\text{OverColor}(C)$ from the object representing $c$ to the object representing the reindexed coloring $c \circ e^{-1} : Y \to C$. This morphism is the color-preserving bijection $e$ that maps the indices in $X$ to their corresponding indices in $Y$.

Given a map $c: X \amalg Y \to C$ that assigns colors from a type $C$ to a disjoint union of index types $X$ and $Y$, there exists a natural isomorphism in the category $\text{OverColor}(C)$ between the object defined by $c$ and the tensor product of the objects defined by its restrictions to $X$ and $Y$. Specifically, $$\text{mk}(c) \cong \text{mk}(c \circ \iota_X) \otimes \text{mk}(c \circ \iota_Y)$$ where $\iota_X: X \to X \amalg Y$ and $\iota_Y: Y \to X \amalg Y$ are the canonical injections into the disjoint union. This isomorphism is induced by the identity map on the underlying type $X \amalg Y$, reflecting the monoidal structure of $\text{OverColor}(C)$ where the tensor product is defined by the disjoint union of index sets.

Let $C$ be a type representing colors of tensor indices. For any map $c: X \amalg Y \to C$ assigning colors to the disjoint union of index sets $X$ and $Y$, let $\text{mkSum}(c)$ be the natural isomorphism $\text{mk}(c) \cong \text{mk}(c \circ \iota_X) \otimes \text{mk}(c \circ \iota_Y)$ in the category $\text{OverColor}(C)$, where $\iota_X$ and $\iota_Y$ are the canonical injections. The underlying bijection between the index sets induced by the forward morphism of this isomorphism, denoted $\text{Hom.toEquiv}((\text{mkSum } c).\text{hom})$, is the identity equivalence on $X \amalg Y$.

For any map $c: X \amalg Y \to C$ assigning colors from a type $C$ to a disjoint union of index types $X$ and $Y$, let $\text{mkSum}(c)$ be the isomorphism $\text{mk}(c) \cong \text{mk}(c \circ \iota_X) \otimes \text{mk}(c \circ \iota_Y)$ in the category $\text{OverColor}(C)$, where $\iota_X$ and $\iota_Y$ are the canonical injections. The theorem states that the underlying bijection of the inverse morphism $(\text{mkSum}(c))^{-1}$ is the identity equivalence on the type $X \amalg Y$.

Given a type $X$ and two color-assigning maps $c_1, c_2 : X \to C$, if $c_1 = c_2$, there is a canonical isomorphism between the objects $\text{mk } c_1$ and $\text{mk } c_2$ in the category $\text{OverColor}(C)$. This isomorphism is induced by the identity bijection on the index type $X$.

For any mapping $c: X \to C$ defining an object in the category $\text{OverColor}(C)$, the forward morphism of the canonical isomorphism induced by the equality $c = c$ (via reflexivity) is equal to the identity morphism $\mathbb{1}_{\text{mk } c}$ in $\text{OverColor}(C)$.

Let $C$ be a type representing colors and $X$ a type representing indices. For any two color-assigning maps $c_1, c_2 : X \to C$ such that $c_1 = c_2$, let $\text{mkIso}(h)$ be the canonical isomorphism between the objects in $\text{OverColor}(C)$ defined by $c_1$ and $c_2$. The underlying function of the morphism component of this isomorphism, which maps the index set $X$ to itself, is the identity function $\text{id}_X$.

Let $C$ be a type of colors and $X$ a type of indices. For any two color-assigning maps $c_1, c_2 : X \to C$ such that $c_1 = c_2$, let $\text{mkIso}(h)$ be the canonical isomorphism between the objects in $\text{OverColor}(C)$ defined by $c_1$ and $c_2$. For any index $x \in X$, the underlying function of the forward morphism component of this isomorphism applied to $x$ is equal to $x$.

Let $C$ be a type of colors and $X$ a type of indices. For any two color-assigning maps $c_1, c_2 : X \to C$ such that $c_1 = c_2$, let $\text{mkIso}(h)$ be the canonical isomorphism between the objects represented by $c_1$ and $c_2$ in the category $\text{OverColor}(C)$. The underlying bijection of indices associated with the morphism component of this isomorphism is the identity equivalence on $X$.

Let $C$ be a type of colors and $X$ a type of indices. For any two color-assigning maps $c_1, c_2 : X \to C$ such that $h: c_1 = c_2$, let $\text{mkIso}(h)$ be the canonical isomorphism between the objects represented by $c_1$ and $c_2$ in the category $\text{OverColor}(C)$. The underlying bijection of indices associated with the inverse morphism $(\text{mkIso}(h))^{-1}$ is the identity equivalence on $X$.

Let $C$ be a type of colors, and let $X$ and $Y$ be types of indices. Suppose we have color-assigning maps $c: X \to C$ and $c_1: Y \to C$ representing objects in the category $\text{OverColor}(C)$. Given a bijection $e: X \simeq Y$ such that $c_1(y) = c(e^{-1}(y))$ for all $y \in Y$ (denoted by the proof $h$), the underlying function of the morphism $\text{equivToHomEq}(e, h)$ from $c$ to $c_1$ is equal to the function $e$.

Let $C$ be a type of colors, and let $X$ and $Y$ be types representing indices. Given two objects in the category $\text{OverColor}(C)$ defined by the color-assignment maps $c: X \to C$ and $c_1: Y \to C$, let $e: X \simeq Y$ be a bijection between the index sets. If $e$ satisfies the condition that for all $x \in Y$, $c_1(x) = (c \circ e^{-1})(x)$, then the underlying bijection of the morphism in $\text{OverColor}(C)$ induced by $e$ (denoted by `equivToHomEq e h`) is equal to $e$.