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.

def LinearMap.IsReal {M₁ : Type u_1} {M₂ : Type u_2} {F : Type u_3} [FunLike F M₁ M₂] [Star M₁] [Star M₂] (φ : F) :

Equations

LinearMap.IsReal φ = ∀ (x : M₁), φ (star x) = star (φ x)

Instances For

@[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 φ

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) :

Equations

φ.real = { toFun := fun (x : E) => star (φ (star x)), map_add' := ⋯, map_smul' := ⋯ }

Instances For

@[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))

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

@[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) :

(realSLinearEquiv φ) x = star (φ (star x))

@[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 g : E →ₗ[K] F) :

(f + g).real = f.real + g.real

@[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

@[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

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) :

IsReal φ ↔ φ.real = φ

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φ : IsReal φ) :

φ.real = φ

@[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

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

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) :

IsReal (φ.toLinearMap ∘ₗ f ∘ₗ φ.symm.toLinearMap) ↔ IsReal f

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

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) :

(mulRight K x).real = mulLeft K (star x)

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) :

(mulLeft K x).real = mulRight K (star x)

theorem LinearMap.real.spectrum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [StarAddMonoid E] [StarModule 𝕜 E] [FiniteDimensional 𝕜 E] (φ : E →ₗ[𝕜] E) :

_root_.spectrum 𝕜 φ.real = star (_root_.spectrum 𝕜 φ)

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 α)

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

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 g : E →ₗ[K] F) :

(f - g).real = f.real - g.real

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

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 g : E →ₗ[K] F) :

f = g ↔ f.real = g.real

theorem LinearMap.isRealOne {E : Type u_1} {K : Type u_2} [Semiring K] [AddCommMonoid E] [Module K E] [Star E] :

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] :

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] :

real 1 = 1