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.IntrinsicStar.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)

A linear map is self-adjoint (with respect to the intrinsic star) iff it is star-preserving.

@[simp]

theorem IntrinsicStar.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

A star-preserving linear map is self-adjoint (with respect to the intrinsic star).

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_6} [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_6} [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.intrinsicStar_mul' {R' : Type u_5} {E : Type u_6} [CommSemiring R'] [StarRing R'] [NonUnitalNonAssocSemiring E] [StarRing E] [Module R' E] [StarModule R' E] [SMulCommClass R' E E] [IsScalarTower R' E E] : star (mul' R' E) = mul' R' E ∘ₗ ↑(TensorProduct.comm R' E E)

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)

theorem TensorProduct.intrinsicStar_map {R : Type u_5} {E : Type u_6} {F : Type u_7} {G : Type u_8} {H : Type u_9} [CommSemiring R] [StarRing R] [AddCommMonoid E] [StarAddMonoid E] [Module R E] [StarModule R E] [AddCommMonoid F] [StarAddMonoid F] [Module R F] [StarModule R F] [AddCommMonoid G] [StarAddMonoid G] [Module R G] [StarModule R G] [AddCommMonoid H] [StarAddMonoid H] [Module R H] [StarModule R H] (f : E →ₗ[R] F) (g : G →ₗ[R] H) : star (map f g) = map (star f) (star g)

theorem LinearMap.intrinsicStar_lTensor {R : Type u_5} {E : Type u_6} {F : Type u_7} {G : Type u_8} [CommSemiring R] [StarRing R] [AddCommMonoid E] [StarAddMonoid E] [Module R E] [StarModule R E] [AddCommMonoid F] [StarAddMonoid F] [Module R F] [StarModule R F] [AddCommMonoid G] [StarAddMonoid G] [Module R G] [StarModule R G] (f : F →ₗ[R] G) : star (lTensor E f) = lTensor E (star f)

theorem LinearMap.intrinsicStar_rTensor {R : Type u_5} {E : Type u_6} {F : Type u_7} {G : Type u_8} [CommSemiring R] [StarRing R] [AddCommMonoid E] [StarAddMonoid E] [Module R E] [StarModule R E] [AddCommMonoid F] [StarAddMonoid F] [Module R F] [StarModule R F] [AddCommMonoid G] [StarAddMonoid G] [Module R G] [StarModule R G] (f : E →ₗ[R] F) : star (rTensor G f) = rTensor G (star f)

theorem LinearMap.toMatrix'_intrinsicStar {R : Type u_4} {m : Type u_5} {n : Type u_6} [CommSemiring R] [StarRing R] [Fintype m] [DecidableEq m] (f : (m → R) →ₗ[R] n → R) : toMatrix' (star f) = (toMatrix' f).map star

theorem LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix' {R : Type u_4} {m : Type u_5} {n : Type u_6} [CommSemiring R] [StarRing R] [Fintype m] [DecidableEq m] (f : (m → R) →ₗ[R] n → R) : IsSelfAdjoint f ↔ ∀ (i : n) (j : m), IsSelfAdjoint (toMatrix' f i j)

A linear map f : (m → R) →ₗ (n → R) is self-adjoint (with respect to the intrinsic star) iff its corresponding matrix f.toMatrix' has all self-adjoint elements. So star-preserving maps correspond to their matrices containing only self-adjoint elements.

theorem Matrix.intrinsicStar_toLin' {R : Type u_4} {m : Type u_5} {n : Type u_6} [CommSemiring R] [StarRing R] [Fintype m] [DecidableEq m] (A : Matrix n m R) : star (toLin' A) = toLin' (A.map star)

theorem Matrix.IntrinsicStar.isSelfAdjoint_toLin'_iff {R : Type u_4} {m : Type u_5} {n : Type u_6} [CommSemiring R] [StarRing R] [Fintype m] [DecidableEq m] (A : Matrix n m R) : IsSelfAdjoint (toLin' A) ↔ ∀ (i : n) (j : m), IsSelfAdjoint (A i j)

Given a matrix A, A.toLin' is self-adjoint (with respect to the intrinsic star) iff all its elements are self-adjoint.

def Module.End.Units.intrinsicStar {R : Type u_1} {E : Type u_2} [Semiring R] [InvolutiveStar R] [AddCommMonoid E] [Module R E] [StarAddMonoid E] [StarModule R E] : Star (End R E)ˣ

Intrinsic star operation for (End R E)ˣ.

Equations

• Module.End.Units.intrinsicStar = { star := fun (f : (Module.End R E)ˣ) => { val := star ↑f, inv := star ↑f⁻¹, val_inv := ⋯, inv_val := ⋯ } }

theorem Module.End.IsUnit.intrinsicStar {R : Type u_1} {E : Type u_2} [Semiring R] [InvolutiveStar R] [AddCommMonoid E] [Module R E] [StarAddMonoid E] [StarModule R E] {f : End R E} (hf : IsUnit f) : IsUnit (star f)

@[simp]

theorem Module.End.isUnit_intrinsicStar_iff {R : Type u_1} {E : Type u_2} [Semiring R] [InvolutiveStar R] [AddCommMonoid E] [Module R E] [StarAddMonoid E] [StarModule R E] {f : End R E} : IsUnit (star f) ↔ IsUnit f

theorem Module.End.mem_eigenspace_intrinsicStar_iff {R : Type u_4} {V : Type u_5} [CommRing R] [InvolutiveStar R] [AddCommGroup V] [StarAddMonoid V] [Module R V] [StarModule R V] (f : End R V) (α : R) (x : V) : x ∈ (star f).eigenspace α ↔ star x ∈ f.eigenspace (star α)

@[simp]

theorem Module.End.spectrum_intrinsicStar {R : Type u_4} {V : Type u_5} [CommRing R] [InvolutiveStar R] [AddCommGroup V] [StarAddMonoid V] [Module R V] [StarModule R V] (f : End R V) : spectrum R (star f) = star (spectrum R f)