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).
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]
:
The intrinsic star operation on linear maps E →ₗ F defined by
(star f) x = star (f (star x)).
Equations
@[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)
:
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
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
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))
:
A linear map is self-adjoint (with respect to the intrinsic star) iff it is star-preserving.
@[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))
:
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.
@[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}
:
A star-preserving linear map is self-adjoint (with respect to the intrinsic star).
@[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}
:
Alias of IntrinsicStar.StarHomClass.isSelfAdjoint.
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 : WithConv (E →ₗ[R] F))
(g : WithConv (G →ₗ[R] E))
:
@[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]
:
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]
:
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)
:
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)
:
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]
:
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))
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))
:
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))
:
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))
:
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))
:
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)
@[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)
:
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))
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))
:
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)
:
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)
:
Given a matrix A, A.toLin' is self-adjoint (with respect to the intrinsic star)
iff all its elements are self-adjoint.
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]
:
Intrinsic star operation for (End R E)ˣ.
Equations
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)
:
@[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)}
:
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)
:
@[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))
: