Commit 2025-10-23 20:09 e3d2a83c

feat(Algebra/Star): define the intrinsic star on linear maps (#29941) This pr defines the intrinsic star operation on linear maps E →ₗ F where (star f) x = star (f (star x)). This corresponds to a map being star-preserving, i.e., a map is self-adjoint iff it is star-preserving. This is scoped to IntrinsicStar as to not conflict with the global instance on E →ₗ[𝕜] E on finite-dimensional Hilbert spaces, where star is defined as LinearMap.adjoint. These are mathematically distinct instances. In a finite-dimensional C⋆-algebra with a positive linear functional, which induces the GNS Hilbert space (TODO) and a coalgebra given by the adjoint of the multiplication map and the algebra unit map (TODO), we get a star ring where multiplication is given by the convolution product (#25183) and star is given by the intrinsic star. In such a space, we can then define the isomorphism (E →ₗ[ℂ] F) ≃⋆ₐ (F ⊗[ℂ] Eᵐᵒᵖ), which is an important identification in the theory of non-commutative graphs.