Intrinsic star operation on E →ₗ[R] F

This file defines the star operation on linear maps: (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.

Implementation notes

Note that in the case of when E = F for a finite-dimensional Hilbert space, this star is mathematically distinct from the global instance on E →ₗ[𝕜] E where star := LinearMap.adjoint. For that reason, the intrinsic star operation is scoped to IntrinsicStar.

def LinearMap.intrinsicStar {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [InvolutiveStar R] [AddCommMonoid E] [Module R E] [StarAddMonoid E] [StarModule R E] [AddCommMonoid F] [Module R F] [StarAddMonoid F] [StarModule R F] : Star (E →ₗ[R] F)

The intrinsic star operation on linear maps E →ₗ F defined by (star f) x = star (f (star x)).

Equations

• LinearMap.intrinsicStar = { star := fun (f : E →ₗ[R] F) => { toFun := fun (x : E) => star (f (star x)), map_add' := ⋯, map_smul' := ⋯ } }

@[simp]

theorem LinearMap.intrinsicStar_apply {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [InvolutiveStar R] [AddCommMonoid E] [Module R E] [StarAddMonoid E] [StarModule R E] [AddCommMonoid F] [Module R F] [StarAddMonoid F] [StarModule R F] (f : E →ₗ[R] F) (x : E) : (star f) x = star (f (star x))

def LinearMap.intrinsicInvolutiveStar {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [InvolutiveStar R] [AddCommMonoid E] [Module R E] [StarAddMonoid E] [StarModule R E] [AddCommMonoid F] [Module R F] [StarAddMonoid F] [StarModule R F] : InvolutiveStar (E →ₗ[R] F)

The involutive intrinsic star structure on linear maps.

Equations

• LinearMap.intrinsicInvolutiveStar = { toStar := LinearMap.intrinsicStar, star_involutive := ⋯ }

def LinearMap.intrinsicStarAddMonoid {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [InvolutiveStar R] [AddCommMonoid E] [Module R E] [StarAddMonoid E] [StarModule R E] [AddCommMonoid F] [Module R F] [StarAddMonoid F] [StarModule R F] : StarAddMonoid (E →ₗ[R] F)

The intrinsic star additive monoid structure on linear maps.

Equations

• LinearMap.intrinsicStarAddMonoid = { toInvolutiveStar := LinearMap.intrinsicInvolutiveStar, star_add := ⋯ }

theorem LinearMap.isSelfAdjoint_iff_map_star {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [InvolutiveStar R] [AddCommMonoid E] [Module R E] [StarAddMonoid E] [StarModule R E] [AddCommMonoid F] [Module R F] [StarAddMonoid F] [StarModule R F] (f : E →ₗ[R] F) : IsSelfAdjoint f ↔ ∀ (x : E), f (star x) = star (f x)

@[simp]

theorem StarHomClass.isSelfAdjoint {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [InvolutiveStar R] [AddCommMonoid E] [Module R E] [StarAddMonoid E] [StarModule R E] [AddCommMonoid F] [Module R F] [StarAddMonoid F] [StarModule R F] {S : Type u_4} [FunLike S E F] [LinearMapClass S R E F] [StarHomClass S E F] {f : S} : IsSelfAdjoint ↑f

theorem LinearMap.intrinsicStar_comp {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [InvolutiveStar R] [AddCommMonoid E] [Module R E] [StarAddMonoid E] [StarModule R E] [AddCommMonoid F] [Module R F] [StarAddMonoid F] [StarModule R F] {G : Type u_4} [AddCommMonoid G] [Module R G] [StarAddMonoid G] [StarModule R G] (f : E →ₗ[R] F) (g : G →ₗ[R] E) : star (f ∘ₗ g) = star f ∘ₗ star g

@[simp]

theorem LinearMap.intrinsicStar_id {R : Type u_1} {E : Type u_2} [Semiring R] [InvolutiveStar R] [AddCommMonoid E] [Module R E] [StarAddMonoid E] [StarModule R E] : star id = id

@[simp]

theorem LinearMap.intrinsicStar_zero {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [InvolutiveStar R] [AddCommMonoid E] [Module R E] [StarAddMonoid E] [StarModule R E] [AddCommMonoid F] [Module R F] [StarAddMonoid F] [StarModule R F] : star 0 = 0

theorem LinearMap.intrinsicStar_mulLeft {R : Type u_1} [Semiring R] [InvolutiveStar R] {E : Type u_5} [NonUnitalNonAssocSemiring E] [StarRing E] [Module R E] [StarModule R E] [SMulCommClass R E E] [IsScalarTower R E E] (x : E) : star (mulLeft R x) = mulRight R (star x)

theorem LinearMap.intrinsicStar_mulRight {R : Type u_1} [Semiring R] [InvolutiveStar R] {E : Type u_5} [NonUnitalNonAssocSemiring E] [StarRing E] [Module R E] [StarModule R E] [SMulCommClass R E E] [IsScalarTower R E E] (x : E) : star (mulRight R x) = mulLeft R (star x)

theorem LinearMap.intrinsicStarModule {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [InvolutiveStar R] [AddCommMonoid E] [Module R E] [StarAddMonoid E] [StarModule R E] [AddCommMonoid F] [Module R F] [StarAddMonoid F] [StarModule R F] [SMulCommClass R R F] : StarModule R (E →ₗ[R] F)