QuantumInfo.ForMathlib.ULift

Given a type $\alpha$ equipped with an addition operation and an additive identity $0$ (represented by the `AddZero` class), this definition provides an `AddZero` structure for the universe-lifted type $\text{ULift } \alpha$. Specifically, the zero element in $\text{ULift } \alpha$ is defined as the lift of the zero in $\alpha$, and the addition of two elements in $\text{ULift } \alpha$ is defined by performing the addition on the underlying elements in $\alpha$ and then lifting the result.

For a type $\mathbb{k}$ equipped with a star operation $x \mapsto x^*$, there is a corresponding star operation on the universe-lifted type $\text{ULift}(\mathbb{k})$. For any element $x \in \text{ULift}(\mathbb{k})$, its star $x^*$ is defined by applying the star operation to its underlying value in $\mathbb{k}$, i.e., $x^* = \text{up}((\text{down } x)^*)$.

For a type $\mathbb{k}$ equipped with a star operation $x \mapsto x^*$, and any element $x$ in the universe-lifted type $\text{ULift}(\mathbb{k})$, the star of $x$ is given by $x^* = \text{up}((\text{down } x)^*)$. Here, $\text{down } x$ refers to the underlying value in $\mathbb{k}$ and $\text{up}$ refers to the constructor that lifts a value from $\mathbb{k}$ to $\text{ULift}(\mathbb{k})$.

For any type $\mathbb{k}$ equipped with an involutive star operation (an operation $x \mapsto x^*$ such that $(x^*)^* = x$ for all $x \in \mathbb{k}$), there is a corresponding involutive star operation on the universe-lifted type $\text{ULift}(\mathbb{k})$. This structure ensures that for any element $x \in \text{ULift}(\mathbb{k})$, the property $(x^*)^* = x$ is preserved under the lifting operation.

For any type $\mathbb{k}$ equipped with a multiplication and a star operation $x \mapsto x^*$ such that the property $(xy)^* = y^* x^*$ holds for all $x, y \in \mathbb{k}$, the universe-lifted type $\text{ULift}(\mathbb{k})$ also inherits this star-multiplication structure. The operations on $\text{ULift}(\mathbb{k})$ are defined by applying the corresponding operations to the underlying elements in $\mathbb{k}$.

For any non-unital non-associative semiring $\mathbb{k}$ equipped with a star ring structure, the universe-lifted type $\operatorname{ULift}(\mathbb{k})$ also forms a star ring. This structure inherits the star operation $x \mapsto x^*$ from $\mathbb{k}$, which satisfies the properties $(x + y)^* = x^* + y^*$, $(xy)^* = y^* x^*$, and $(x^*)^* = x$ for all elements $x, y$ in $\operatorname{ULift}(\mathbb{k})$.

Let $\mathbb{k}$ be a commutative star semiring. For any element $x$ in the universe-lifted type $\operatorname{ULift}(\mathbb{k})$, the star operation in $\operatorname{ULift}(\mathbb{k})$ commutes with the projection to the underlying ring $\mathbb{k}$. That is, the downward projection of the star of $x$ is equal to the star of the downward projection of $x$: $$(x^*).\text{down} = (x.\text{down})^*$$ where $x \mapsto x^*$ denotes the star involution.

For any normed field $\mathbf{k}$, its universe lift $\operatorname{ULift}(\mathbf{k})$ is also a normed field, inheriting the field operations and the norm from $\mathbf{k}$.

For any densely normed field $\mathbf{k}$, its universe lift $\operatorname{ULift}(\mathbf{k})$ is also a densely normed field, inheriting the field structure and the property that the set of norms of its elements is dense in $\mathbb{R}_{\ge 0}$.

Let $\alpha$ be a type equipped with an addition operation. For any element $x$ in the universe-lifted type $\text{ULift}(\alpha)$, applying the additive equivalence $\text{AddEquiv.ulift}$ to $x$ is equal to the underlying value $x.\text{down}$ in $\alpha$.

Let $\mathbb{k}$ be a field that satisfies the `RCLike` property (isomorphic to either the real numbers $\mathbb{R}$ or the complex numbers $\mathbb{C}$). The universe lift $\operatorname{ULift}(\mathbb{k})$ is also an `RCLike` field. This structure is defined by lifting the operations from $\mathbb{k}$, including the real part $\operatorname{re}$, the imaginary part $\operatorname{im}$, the complex conjugation $x \mapsto \bar{x}$, and the squared norm $\|x\|^2$, such that they satisfy the standard axioms for a field that behaves like $\mathbb{R}$ or $\mathbb{C}$.