QuantumInfo.ForMathlib.ContinuousLinearMap

Let $M$ and $M_2$ be topological modules and $\sigma$ be a surjective ring homomorphism. For the zero continuous linear map $0: M \to M_2$, its range is the bottom element of the submodule lattice, which is the zero submodule $\{0\}$.

The kernel of the zero continuous semilinear map from a topological module $M$ to a topological module $M_2$ is equal to the top element of the submodule lattice of $M$ (i.e., the entire module $M$). Specifically, if $0: M \toSL[\sigma] M_2$ is the zero map, then $\ker(0) = \top$.

Let $M$ and $M_2$ be topological modules and $\sigma$ be a ring homomorphism. For any semilinear map $f: M \to M_2$ and a proof $hf$ that $f$ is continuous, the kernel of the continuous semilinear map induced by $f$ (denoted as $\text{ContinuousLinearMap.mk } f \text{ } hf$) is equal to the kernel of the underlying linear map $f$, i.e., $\ker(\text{mk } f \text{ } hf) = \ker f$.

Let $A: \mathbb{C}^n \to \mathbb{C}^n$ (or more generally, $A: \text{EuclideanSpace } \mathbb{k}^n \to \text{EuclideanSpace } \mathbb{k}^n$) be a symmetric continuous linear map (a Hermitian operator). Then its range (support) is equal to the join (supremum) of all its eigenspaces corresponding to non-zero eigenvalues: $$\text{range}(A) = \bigoplus_{\mu \neq 0} \text{eigenspace}(A, \mu)$$ where $\text{eigenspace}(A, \mu)$ denotes the subspace of vectors $v$ such that $A(v) = \mu v$.