Documentation

Mathlib.Algebra.Star.LinearMap

Intrinsic star operation on linear maps #

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 #

Because there is a global star instance on H ā†’ā‚—[š•œ] H (defined as the linear map adjoint on finite-dimensional Hilbert spaces), which is mathematically distinct from this star, we provide this instance on WithConv (E ā†’ā‚—[R] F).

The reason we chose WithConv is because together with the convolution product from Mathlib/RingTheory/Coalgebra/Convolution.lean, we get a ā‹†-algebra when star (WithConv.toConv comul) = WithConv.toConv (comm āˆ˜ comul).

source
@[instance_reducible]
instance 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 (WithConv (E ā†’ā‚—[R] F))

The intrinsic star operation on linear maps E ā†’ā‚— F defined by (star f) x = star (f (star x)).

Equations
source
@[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 : WithConv (E ā†’ā‚—[R] F)) (x : E) :
(star f).ofConv x = star (f.ofConv (star x))
source
@[instance_reducible]
instance 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 (WithConv (E ā†’ā‚—[R] F))

The involutive intrinsic star structure on linear maps.

Equations
source
@[instance_reducible]
instance 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 (WithConv (E ā†’ā‚—[R] F))

The intrinsic star additive monoid structure on linear maps.

Equations
source
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 : WithConv (E ā†’ā‚—[R] F)) :
IsSelfAdjoint f ā†” āˆ€ (x : E), f.ofConv (star x) = star (f.ofConv x)

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

source
@[deprecated LinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star (since := "2025-12-09")]
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 : WithConv (E ā†’ā‚—[R] F)) :
IsSelfAdjoint f ā†” āˆ€ (x : E), f.ofConv (star x) = star (f.ofConv x)

Alias of LinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star.

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

source
@[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 (WithConv.toConv ā†‘f)

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

source
@[deprecated IntrinsicStar.StarHomClass.isSelfAdjoint (since := "2025-12-09")]
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 (WithConv.toConv ā†‘f)

Alias of IntrinsicStar.StarHomClass.isSelfAdjoint.

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

source
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 : WithConv (E ā†’ā‚—[R] F)) (g : WithConv (G ā†’ā‚—[R] E)) :
star (WithConv.toConv (f.ofConv āˆ˜ā‚— g.ofConv)) = WithConv.toConv ((star f).ofConv āˆ˜ā‚— (star g).ofConv)
source
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 (WithConv.toConv (f āˆ˜ā‚— g)) = WithConv.toConv ((star (WithConv.toConv f)).ofConv āˆ˜ā‚— (star (WithConv.toConv g)).ofConv)
source
@[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 (WithConv.toConv id) = WithConv.toConv id
source
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
source
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 (WithConv.toConv (mulLeft R x)) = WithConv.toConv (mulRight R (star x))
source
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 (WithConv.toConv (mulRight R x)) = WithConv.toConv (mulLeft R (star x))
source
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 (WithConv.toConv (mul' R' E)) = WithConv.toConv (mul' R' E āˆ˜ā‚— ā†‘(TensorProduct.comm R' E E))
source
instance 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 (WithConv (E ā†’ā‚—[R] F))
source
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 : WithConv (E ā†’ā‚—[R] F)) (g : WithConv (G ā†’ā‚—[R] H)) :
star (WithConv.toConv (map f.ofConv g.ofConv)) = WithConv.toConv (map (star f).ofConv (star g).ofConv)
source
theorem TensorProduct.star_map_apply_eq_map_intrinsicStar {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 : WithConv (E ā†’ā‚—[R] F)) (g : WithConv (G ā†’ā‚—[R] H)) (x : TensorProduct R E G) :
star ((map f.ofConv g.ofConv) x) = (map (star f).ofConv (star g).ofConv) (star x)
source
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 : WithConv (F ā†’ā‚—[R] G)) :
star (WithConv.toConv (lTensor E f.ofConv)) = WithConv.toConv (lTensor E (star f).ofConv)
source
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 : WithConv (E ā†’ā‚—[R] F)) :
star (WithConv.toConv (rTensor G f.ofConv)) = WithConv.toConv (rTensor G (star f).ofConv)
source
theorem LinearMap.intrinsicStar_eq_comp {R : Type u_5} {E : Type u_6} {F : Type u_7} [CommSemiring R] [StarRing R] [AddCommMonoid E] [StarAddMonoid E] [Module R E] [StarModule R E] [AddCommMonoid F] [StarAddMonoid F] [Module R F] [StarModule R F] (f : WithConv (E ā†’ā‚—[R] F)) :
star f = WithConv.toConv (ā†‘(starLinearEquiv R) āˆ˜ā‚›ā‚— f.ofConv āˆ˜ā‚›ā‚— ā†‘(starLinearEquiv R))
source
theorem LinearMap.IntrinsicStar.starLinearEquiv_eq_arrowCongr {R : Type u_5} {E : Type u_6} {F : Type u_7} [CommSemiring R] [StarRing R] [AddCommMonoid E] [StarAddMonoid E] [Module R E] [StarModule R E] [AddCommMonoid F] [StarAddMonoid F] [Module R F] [StarModule R F] :
starLinearEquiv R = (WithConv.linearEquiv R (E ā†’ā‚—[R] F)).trans (((starLinearEquiv R).arrowCongr (starLinearEquiv R)).trans (WithConv.linearEquiv R (E ā†’ā‚—[R] F)).symm)
source
@[simp]
theorem LinearMap.intrinsicStar_toSpanSingleton {E : Type u_2} [AddCommMonoid E] [StarAddMonoid E] {S : Type u_5} [Semiring S] [StarAddMonoid S] [StarModule S S] [Module S E] [StarModule S E] (a : E) :
star (WithConv.toConv (toSpanSingleton S E a)) = WithConv.toConv (toSpanSingleton S E (star a))
source
theorem LinearMap.intrinsicStar_smulRight {E : Type u_2} {F : Type u_3} [AddCommMonoid E] [StarAddMonoid E] [AddCommMonoid F] [StarAddMonoid F] {S : Type u_5} [Semiring S] [StarAddMonoid S] [StarModule S S] [Module S E] [StarModule S E] [Module S F] [StarModule S F] (f : WithConv (E ā†’ā‚—[S] S)) (x : F) :
star (WithConv.toConv (f.ofConv.smulRight x)) = WithConv.toConv ((star f).ofConv.smulRight (star x))
source
theorem LinearMap.intrinsicStar_convMul {R : Type u_5} {A : Type u_6} {C : Type u_7} [CommSemiring R] [StarRing R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarRing A] [StarModule R A] [AddCommMonoid C] [Module R C] [StarAddMonoid C] [StarModule R C] [CoalgebraStruct R C] (h : star (WithConv.toConv CoalgebraStruct.comul) = WithConv.toConv (ā†‘(TensorProduct.comm R C C) āˆ˜ā‚— CoalgebraStruct.comul)) (f g : WithConv (C ā†’ā‚—[R] A)) :
star (f * g) = star g * star f
source
@[reducible, inline]
abbrev LinearMap.convIntrinsicStarRing {R : Type u_5} {A : Type u_6} {C : Type u_7} [CommSemiring R] [StarRing R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [StarRing A] [StarModule R A] [AddCommMonoid C] [Module R C] [StarAddMonoid C] [StarModule R C] [Coalgebra R C] (h : star (WithConv.toConv CoalgebraStruct.comul) = WithConv.toConv (ā†‘(TensorProduct.comm R C C) āˆ˜ā‚— CoalgebraStruct.comul)) :
StarRing (WithConv (C ā†’ā‚—[R] A))

The convolutive intrinsic star ring on linear maps from coalgebras to ā‹†-algebras, given that star (toConv comul) = toConv (comm āˆ˜ā‚— comul).

In finite-dimensional Cā‹†-algebras, under the GNS construction, and the adjoint coalgebra, we get this hypothesis.

See note [reducible non-instances].

Equations
Instances For
    source
    @[simp]
    theorem LinearMap.intrinsicStar_single {R : Type u_5} [CommSemiring R] [StarRing R] {n : Type u_8} [DecidableEq n] {B : n ā†’ Type u_9} [(i : n) ā†’ AddCommMonoid (B i)] [(i : n) ā†’ Module R (B i)] [(i : n) ā†’ StarAddMonoid (B i)] [āˆ€ (i : n), StarModule R (B i)] (i : n) :
    star (WithConv.toConv (single R B i)) = WithConv.toConv (single R B i)
    source
    theorem Pi.intrinsicStar_comul {R : Type u_5} [CommSemiring R] [StarRing R] {n : Type u_8} [DecidableEq n] {B : n ā†’ Type u_9} [(i : n) ā†’ AddCommMonoid (B i)] [(i : n) ā†’ Module R (B i)] [(i : n) ā†’ StarAddMonoid (B i)] [āˆ€ (i : n), StarModule R (B i)] [Fintype n] [(i : n) ā†’ CoalgebraStruct R (B i)] (h : āˆ€ (i : n), star (WithConv.toConv CoalgebraStruct.comul) = WithConv.toConv (ā†‘(TensorProduct.comm R (B i) (B i)) āˆ˜ā‚— CoalgebraStruct.comul)) :
    star (WithConv.toConv CoalgebraStruct.comul) = WithConv.toConv (ā†‘(TensorProduct.comm R ((i : n) ā†’ B i) ((i : n) ā†’ B i)) āˆ˜ā‚— CoalgebraStruct.comul)
    source
    @[simp]
    theorem Pi.intrinsicStar_comul_commSemiring {R : Type u_5} [CommSemiring R] [StarRing R] {n : Type u_8} [DecidableEq n] [Fintype n] :
    star (WithConv.toConv CoalgebraStruct.comul) = WithConv.toConv (ā†‘(TensorProduct.comm R (n ā†’ R) (n ā†’ R)) āˆ˜ā‚— CoalgebraStruct.comul)
    source
    @[instance_reducible]
    instance Pi.convIntrinsicStarRingCommSemiring {R : Type u_5} [CommSemiring R] [StarRing R] {n : Type u_8} [DecidableEq n] [Fintype n] {m : Type u_10} :
    StarRing (WithConv ((n ā†’ R) ā†’ā‚—[R] m ā†’ R))

    The intrinsic star convolutive ring on linear maps from n ā†’ R to m ā†’ R.

    Equations
    source
    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 : WithConv ((m ā†’ R) ā†’ā‚—[R] n ā†’ R)) :
    toMatrix' (star f).ofConv = (toMatrix' f.ofConv).map star
    source
    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 : WithConv ((m ā†’ R) ā†’ā‚—[R] n ā†’ R)) :
    IsSelfAdjoint f ā†” āˆ€ (i : n) (j : m), IsSelfAdjoint (toMatrix' f.ofConv 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.

    source
    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 (WithConv.toConv (toLin' A)) = WithConv.toConv (toLin' (A.map star))
    source
    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 (WithConv.toConv (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.

    source
    @[instance_reducible]
    instance 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 (WithConv (End R E)Ė£)

    Intrinsic star operation for (End R E)Ė£.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    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 : WithConv (End R E)} (hf : IsUnit f.ofConv) :
    IsUnit (star f).ofConv
    source
    @[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 : WithConv (End R E)} :
    IsUnit (star f).ofConv ā†” IsUnit f.ofConv
    source
    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 : WithConv (End R V)) (Ī± : R) (x : V) :
    x āˆˆ (star f).ofConv.eigenspace Ī± ā†” star x āˆˆ f.ofConv.eigenspace (star Ī±)
    source
    @[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 : WithConv (End R V)) :
    spectrum R (star f).ofConv = star (spectrum R f.ofConv)