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
šŸ”ø coverage
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
    šŸ“ coverage
    @[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
    šŸ”ø coverage
    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
      šŸ”ø coverage
      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
        šŸ“ coverage
        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
        šŸ“ coverage
        @[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
        šŸ“ coverage
        @[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
        šŸ“ coverage
        @[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
        šŸ“ coverage
        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
        šŸ“ coverage
        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
        šŸ“ coverage
        @[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
        šŸ“ coverage
        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
        šŸ“ coverage
        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
        šŸ“ coverage
        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
        šŸ“ coverage
        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
        šŸ“ coverage
        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
        šŸ“ coverage
        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
        šŸ“ coverage
        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
        šŸ“ coverage
        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
        šŸ“ coverage
        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
        šŸ“ coverage
        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
        šŸ“ coverage
        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
        šŸ“ coverage
        @[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
        šŸ“ coverage
        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
        šŸ“ coverage
        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
        šŸ”ø coverage
        @[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
            šŸ“ coverage
            @[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
            šŸ“ coverage
            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
            šŸ“ coverage
            @[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
            šŸ”ø coverage
            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
              šŸ“ coverage
              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
              šŸ“ coverage
              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
              šŸ“ coverage
              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
              šŸ“ coverage
              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
              šŸ”ø coverage
              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
                source
                šŸ“ coverage
                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
                šŸ“ coverage
                @[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
                šŸ“ coverage
                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
                šŸ“ coverage
                @[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)