Intrinsic star operation on continuous linear maps

This file defines the star operation on continuous 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.

This is the continuous version of the intrinsic star on linear maps (see Mathlib/Algebra/Star/LinearMap.lean).

Implementation notes

Because there is a global star instance on H →L[𝕜] H (defined as the linear map adjoint on Hilbert spaces), which is mathematically distinct from this star, we provide this instance on WithConv (E →L[R] F).

@[implicit_reducible]

instance ContinuousLinearMap.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] [TopologicalSpace E] [TopologicalSpace F] [ContinuousStar E] [ContinuousStar F] : Star (WithConv (E →L[R] F))

The intrinsic star operation on continuous linear maps defined by (star f) x = star (f (star x)).

@[simp]

theorem ContinuousLinearMap.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] [TopologicalSpace E] [TopologicalSpace F] [ContinuousStar E] [ContinuousStar F] (f : WithConv (E →L[R] F)) (x : E) : (star f).ofConv x = star (f.ofConv (star x))

@[simp]

theorem ContinuousLinearMap.toLinearMap_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] [TopologicalSpace E] [TopologicalSpace F] [ContinuousStar E] [ContinuousStar F] (f : WithConv (E →L[R] F)) : ↑(star f).ofConv = (star (WithConv.toConv ↑f.ofConv)).ofConv

theorem ContinuousLinearMap.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] [TopologicalSpace E] [TopologicalSpace F] [ContinuousStar E] [ContinuousStar F] (f : WithConv (E →L[R] F)) : IsSelfAdjoint f ↔ ∀ (x : E), f.ofConv (star x) = star (f.ofConv x)

theorem ContinuousLinearMap.IntrinsicStar.isSelfAdjoint_toLinearMap_iff {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] [TopologicalSpace E] [TopologicalSpace F] [ContinuousStar E] [ContinuousStar F] (f : WithConv (E →L[R] F)) : IsSelfAdjoint (WithConv.toConv ↑f.ofConv) ↔ IsSelfAdjoint f

@[implicit_reducible]

instance ContinuousLinearMap.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] [TopologicalSpace E] [TopologicalSpace F] [ContinuousStar E] [ContinuousStar F] : InvolutiveStar (WithConv (E →L[R] F))

The involutive intrinsic star structure on continuous linear maps.

@[implicit_reducible]

instance ContinuousLinearMap.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] [TopologicalSpace E] [TopologicalSpace F] [ContinuousStar E] [ContinuousStar F] [ContinuousAdd F] : StarAddMonoid (WithConv (E →L[R] F))

The intrinsic star additive monoid structure on continuous linear maps.

theorem ContinuousLinearMap.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] [TopologicalSpace E] [TopologicalSpace F] [ContinuousStar E] [ContinuousStar F] {G : Type u_4} [AddCommMonoid G] [Module R G] [StarAddMonoid G] [StarModule R G] [TopologicalSpace G] [ContinuousStar G] (f : WithConv (E →L[R] F)) (g : WithConv (G →L[R] E)) : star (WithConv.toConv (f.ofConv.comp g.ofConv)) = WithConv.toConv ((star f).ofConv.comp (star g).ofConv)

theorem ContinuousLinearMap.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] [TopologicalSpace E] [TopologicalSpace F] [ContinuousStar E] [ContinuousStar F] {G : Type u_4} [AddCommMonoid G] [Module R G] [StarAddMonoid G] [StarModule R G] [TopologicalSpace G] [ContinuousStar G] (f : E →L[R] F) (g : G →L[R] E) : star (WithConv.toConv (f.comp g)) = WithConv.toConv ((star (WithConv.toConv f)).ofConv.comp (star (WithConv.toConv g)).ofConv)

@[simp]

theorem ContinuousLinearMap.intrinsicStar_id {R : Type u_1} {E : Type u_2} [Semiring R] [InvolutiveStar R] [AddCommMonoid E] [Module R E] [StarAddMonoid E] [StarModule R E] [TopologicalSpace E] [ContinuousStar E] : star (WithConv.toConv (ContinuousLinearMap.id R E)) = WithConv.toConv (ContinuousLinearMap.id R E)

@[simp]

theorem ContinuousLinearMap.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] [TopologicalSpace E] [TopologicalSpace F] [ContinuousStar E] [ContinuousStar F] : star (WithConv.toConv 0) = WithConv.toConv 0

@[simp]

theorem ContinuousLinearMap.intrinsicStar_toSpanSingleton {E : Type u_2} [AddCommMonoid E] [StarAddMonoid E] [TopologicalSpace E] [ContinuousStar E] {S : Type u_4} [Semiring S] [StarAddMonoid S] [StarModule S S] [Module S E] [StarModule S E] [TopologicalSpace S] [ContinuousStar S] [ContinuousSMul S E] (a : E) : star (WithConv.toConv (toSpanSingleton S a)) = WithConv.toConv (toSpanSingleton S (star a))

theorem ContinuousLinearMap.intrinsicStar_smulRight {E : Type u_2} {F : Type u_3} [AddCommMonoid E] [StarAddMonoid E] [AddCommMonoid F] [StarAddMonoid F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousStar E] [ContinuousStar F] {S : Type u_4} [Semiring S] [StarAddMonoid S] [StarModule S S] [Module S E] [StarModule S E] [TopologicalSpace S] [ContinuousStar S] [Module S F] [StarModule S F] [ContinuousSMul S F] (f : WithConv (E →L[S] S)) (x : F) : star (WithConv.toConv (f.ofConv.smulRight x)) = WithConv.toConv ((star f).ofConv.smulRight (star x))

instance ContinuousLinearMap.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] [TopologicalSpace E] [TopologicalSpace F] [ContinuousStar E] [ContinuousStar F] [SMulCommClass R R F] [ContinuousConstSMul R F] : StarModule R (WithConv (E →L[R] F))

theorem ContinuousLinearMap.intrinsicStar_eq_comp {E : Type u_2} {F : Type u_3} [AddCommMonoid E] [StarAddMonoid E] [AddCommMonoid F] [StarAddMonoid F] [TopologicalSpace E] [TopologicalSpace F] [ContinuousStar E] [ContinuousStar F] {R : Type u_4} [CommSemiring R] [StarRing R] [Module R E] [StarModule R E] [Module R F] [StarModule R F] (f : WithConv (E →L[R] F)) : star f = WithConv.toConv ((↑(starL R)).comp (f.ofConv.comp ↑(starL R)))