Documentation

Monlib.LinearAlgebra.IsReal

real linear maps (a.k.a. star-preserving linear maps) #

This file defines the function linear_map.real which maps a linear map φ.real (x) = star (φ (star x)); so that φ is real (star-preserving) if and only if φ = φ.real.

source
def LinearMap.IsReal {M₁ : Type u_1} {M₂ : Type u_2} {F : Type u_3} [FunLike F M₁ M₂] [Star M₁] [Star M₂] (φ : F) :
Prop
Equations
Instances For
    source
    @[simp]
    theorem starHomClass.linearMap_isReal {M₁ : Type u_1} {M₂ : Type u_2} {F : Type u_3} [FunLike F M₁ M₂] [Star M₁] [Star M₂] [StarHomClass F M₁ M₂] (φ : F) :
    LinearMap.IsReal φ
    source
    def LinearMap.real {E : Type u_1} {F : Type u_2} {K : Type u_3} [AddCommMonoid E] [StarAddMonoid E] [AddCommMonoid F] [StarAddMonoid F] [Semiring K] [Module K E] [Module K F] [InvolutiveStar K] [StarModule K E] [StarModule K F] (φ : E →ₗ[K] F) :
    E →ₗ[K] F
    Equations
    • φ.real = { toFun := fun (x : E) => star (φ (star x)), map_add' := ⋯, map_smul' := ⋯ }
    Instances For
      source
      @[simp]
      theorem LinearMap.real_apply {E : Type u_1} {F : Type u_2} {K : Type u_3} [AddCommMonoid E] [StarAddMonoid E] [AddCommMonoid F] [StarAddMonoid F] [Semiring K] [Module K E] [Module K F] [InvolutiveStar K] [StarModule K E] [StarModule K F] (φ : E →ₗ[K] F) (x : E) :
      φ.real x = star (φ (star x))
      source
      def LinearMap.realSLinearEquiv {E : Type u_1} {F : Type u_2} {K : Type u_3} [AddCommMonoid E] [StarAddMonoid E] [AddCommMonoid F] [StarAddMonoid F] [CommSemiring K] [Module K E] [Module K F] [StarRing K] [StarModule K E] [StarModule K F] :
      (E →ₗ[K] F) ≃ₗ⋆[K] E →ₗ[K] F
      Equations
      • LinearMap.realSLinearEquiv = { toFun := fun (φ : E →ₗ[K] F) => φ.real, map_add' := ⋯, map_smul' := ⋯, invFun := fun (φ : E →ₗ[K] F) => φ.real, left_inv := ⋯, right_inv := ⋯ }
      Instances For
        source
        @[simp]
        theorem LinearMap.realSLinearEquiv_apply_apply {E : Type u_1} {F : Type u_2} {K : Type u_3} [AddCommMonoid E] [StarAddMonoid E] [AddCommMonoid F] [StarAddMonoid F] [CommSemiring K] [Module K E] [Module K F] [StarRing K] [StarModule K E] [StarModule K F] (φ : E →ₗ[K] F) (x : E) :
        (LinearMap.realSLinearEquiv φ) x = star (φ (star x))
        source
        @[simp]
        theorem LinearMap.real_add {E : Type u_2} {F : Type u_3} {K : Type u_1} [AddCommMonoid E] [StarAddMonoid E] [AddCommMonoid F] [StarAddMonoid F] [Semiring K] [Module K E] [Module K F] [InvolutiveStar K] [StarModule K E] [StarModule K F] (f : E →ₗ[K] F) (g : E →ₗ[K] F) :
        (f + g).real = f.real + g.real
        source
        @[simp]
        theorem LinearMap.real_sum {E : Type u_3} {F : Type u_4} {K : Type u_2} [AddCommMonoid E] [StarAddMonoid E] [AddCommMonoid F] [StarAddMonoid F] [Semiring K] [Module K E] [Module K F] [InvolutiveStar K] [StarModule K E] [StarModule K F] {n : Type u_1} {s : Finset n} (f : n → E →ₗ[K] F) :
        (∑ i ∈ s, f i).real = ∑ i ∈ s, (f i).real
        source
        @[simp]
        theorem LinearMap.real_real {E : Type u_2} {F : Type u_3} {K : Type u_1} [AddCommMonoid E] [StarAddMonoid E] [AddCommMonoid F] [StarAddMonoid F] [Semiring K] [Module K E] [Module K F] [InvolutiveStar K] [StarModule K E] [StarModule K F] (f : E →ₗ[K] F) :
        f.real.real = f
        source
        theorem LinearMap.isReal_iff {E : Type u_2} {F : Type u_3} {K : Type u_1} [AddCommMonoid E] [StarAddMonoid E] [AddCommMonoid F] [StarAddMonoid F] [Semiring K] [Module K E] [Module K F] [InvolutiveStar K] [StarModule K E] [StarModule K F] (φ : E →ₗ[K] F) :
        LinearMap.IsReal φ ↔ φ.real = φ
        source
        theorem LinearMap.real_of_isReal {E : Type u_2} {F : Type u_3} {K : Type u_1} [AddCommMonoid E] [StarAddMonoid E] [AddCommMonoid F] [StarAddMonoid F] [Semiring K] [Module K E] [Module K F] [InvolutiveStar K] [StarModule K E] [StarModule K F] {φ : E →ₗ[K] F} (hφ : LinearMap.IsReal φ) :
        φ.real = φ
        source
        @[simp]
        theorem LinearMap.real_comp {E : Type u_3} {F : Type u_4} {K : Type u_2} [AddCommMonoid E] [StarAddMonoid E] [AddCommMonoid F] [StarAddMonoid F] [Semiring K] [Module K E] [Module K F] [InvolutiveStar K] [StarModule K E] [StarModule K F] {G : Type u_1} [AddCommMonoid G] [StarAddMonoid G] [Module K G] [StarModule K G] (f : E →ₗ[K] F) (g : G →ₗ[K] E) :
        (f ∘ₗ g).real = f.real ∘ₗ g.real
        source
        theorem LinearMap.real_starAlgEquiv_conj {E : Type u_1} {K : Type u_2} {F : Type u_3} [CommSemiring K] [Semiring E] [Semiring F] [Algebra K E] [Algebra K F] [InvolutiveStar K] [StarAddMonoid E] [StarAddMonoid F] [StarModule K E] [StarModule K F] (f : E →ₗ[K] E) (φ : E ≃⋆ₐ[K] F) :
        (φ.toLinearMap ∘ₗ f ∘ₗ φ.symm.toLinearMap).real = φ.toLinearMap ∘ₗ f.real ∘ₗ φ.symm.toLinearMap
        source
        theorem LinearMap.real_starAlgEquiv_conj_iff {E : Type u_1} {F : Type u_2} {K : Type u_3} [CommSemiring K] [Semiring E] [Semiring F] [Algebra K E] [Algebra K F] [InvolutiveStar K] [StarAddMonoid E] [StarAddMonoid F] [StarModule K E] [StarModule K F] (f : E →ₗ[K] E) (φ : E ≃⋆ₐ[K] F) :
        LinearMap.IsReal (φ.toLinearMap ∘ₗ f ∘ₗ φ.symm.toLinearMap) ↔ LinearMap.IsReal f
        source
        def LinearMap.realRingEquiv {R : Type u_1} {E : Type u_2} [Semiring R] [AddCommMonoid E] [StarAddMonoid E] [Module R E] [InvolutiveStar R] [StarModule R E] :
        (E →ₗ[R] E) ≃+* (E →ₗ[R] E)
        Equations
        • LinearMap.realRingEquiv = { toFun := fun (f : E →ₗ[R] E) => f.real, invFun := fun (f : E →ₗ[R] E) => f.real, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
        Instances For
          source
          theorem LinearMap.mulRight_real {E : Type u_1} {K : Type u_2} [CommSemiring K] [NonUnitalSemiring E] [InvolutiveStar K] [StarRing E] [Module K E] [StarModule K E] [SMulCommClass K E E] [IsScalarTower K E E] (x : E) :
          (LinearMap.mulRight K x).real = LinearMap.mulLeft K (star x)
          source
          theorem LinearMap.mulLeft_real {E : Type u_1} {K : Type u_2} [CommSemiring K] [NonUnitalSemiring E] [InvolutiveStar K] [StarRing E] [Module K E] [StarModule K E] [SMulCommClass K E E] [IsScalarTower K E E] (x : E) :
          (LinearMap.mulLeft K x).real = LinearMap.mulRight K (star x)
          source
          theorem LinearMap.real.spectrum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [StarAddMonoid E] [StarModule 𝕜 E] [FiniteDimensional 𝕜 E] (φ : E →ₗ[𝕜] E) :
          spectrum 𝕜 φ.real = star (spectrum 𝕜 φ)
          source
          theorem LinearMap.real.eigenspace {𝕜 : Type u_2} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [StarAddMonoid E] [StarModule 𝕜 E] (φ : E →ₗ[𝕜] E) (α : 𝕜) (x : E) :
          x ∈ Module.End.eigenspace φ.real α ↔ star x ∈ Module.End.eigenspace φ (star α)
          source
          theorem LinearMap.real_neg {E : Type u_1} {F : Type u_2} {K : Type u_3} [AddCommMonoid E] [StarAddMonoid E] [AddCommGroup F] [StarAddMonoid F] [Semiring K] [Module K E] [Module K F] [InvolutiveStar K] [StarModule K E] [StarModule K F] (f : E →ₗ[K] F) :
          (-f).real = -f.real
          source
          theorem LinearMap.real_sub {E : Type u_1} {F : Type u_2} {K : Type u_3} [AddCommMonoid E] [StarAddMonoid E] [AddCommGroup F] [StarAddMonoid F] [Semiring K] [Module K E] [Module K F] [InvolutiveStar K] [StarModule K E] [StarModule K F] (f : E →ₗ[K] F) (g : E →ₗ[K] F) :
          (f - g).real = f.real - g.real
          source
          theorem LinearMap.real_smul {E : Type u_1} {F : Type u_2} {K : Type u_3} [CommSemiring K] [AddCommMonoid E] [AddCommMonoid F] [StarRing K] [StarAddMonoid E] [StarAddMonoid F] [Module K E] [Module K F] [StarModule K E] [StarModule K F] (f : E →ₗ[K] F) (α : K) :
          (α • f).real = (starRingEnd K) α • f.real
          source
          theorem LinearMap.real_inj_eq {E : Type u_1} {F : Type u_2} {K : Type u_3} [Semiring K] [AddCommMonoid E] [AddCommMonoid F] [InvolutiveStar K] [StarAddMonoid E] [StarAddMonoid F] [Module K E] [Module K F] [StarModule K E] [StarModule K F] (f : E →ₗ[K] F) (g : E →ₗ[K] F) :
          f = g ↔ f.real = g.real
          source
          theorem LinearMap.isRealOne {E : Type u_1} {K : Type u_2} [Semiring K] [AddCommMonoid E] [Module K E] [Star E] :
          LinearMap.IsReal 1
          source
          theorem LinearMap.isRealZero {E : Type u_1} {F : Type u_2} {K : Type u_3} [Semiring K] [AddCommMonoid E] [AddCommMonoid F] [Module K E] [Module K F] [Star E] [StarAddMonoid F] :
          LinearMap.IsReal 0
          source
          theorem LinearMap.real_one {E : Type u_1} {K : Type u_2} [Semiring K] [InvolutiveStar K] [AddCommMonoid E] [StarAddMonoid E] [Module K E] [StarModule K E] :
          LinearMap.real 1 = 1