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
linear_map.is_real
{E : Type u_1}
{F : Type u_2}
{K : Type u_3}
[semiring K]
[add_comm_monoid E]
[add_comm_monoid F]
[module K E]
[module K F]
[has_star E]
[has_star F]
(φ : E →ₗ[K] F) :
Prop
Equations
- φ.is_real = ∀ (x : E), ⇑φ (has_star.star x) = has_star.star (⇑φ x)
def
linear_map.real
{E : Type u_1}
{F : Type u_2}
{K : Type u_3}
[add_comm_monoid E]
[star_add_monoid E]
[add_comm_monoid F]
[star_add_monoid F]
[semiring K]
[module K E]
[module K F]
[has_involutive_star K]
[star_module K E]
[star_module K F]
(φ : E →ₗ[K] F) :
Equations
- φ.real = {to_fun := λ (x : E), has_star.star (⇑φ (has_star.star x)), map_add' := _, map_smul' := _}
theorem
linear_map.real_eq
{E : Type u_1}
{F : Type u_2}
{K : Type u_3}
[add_comm_monoid E]
[star_add_monoid E]
[add_comm_monoid F]
[star_add_monoid F]
[semiring K]
[module K E]
[module K F]
[has_involutive_star K]
[star_module K E]
[star_module K F]
(φ : E →ₗ[K] F)
(x : E) :
⇑(φ.real) x = has_star.star (⇑φ (has_star.star x))
theorem
linear_map.is_real_iff
{E : Type u_1}
{F : Type u_2}
{K : Type u_3}
[add_comm_monoid E]
[star_add_monoid E]
[add_comm_monoid F]
[star_add_monoid F]
[semiring K]
[module K E]
[module K F]
[has_involutive_star K]
[star_module K E]
[star_module K F]
(φ : E →ₗ[K] F) :
theorem
linear_map.real_add
{E : Type u_1}
{F : Type u_2}
{K : Type u_3}
[add_comm_monoid E]
[star_add_monoid E]
[add_comm_monoid F]
[star_add_monoid F]
[semiring K]
[module K E]
[module K F]
[has_involutive_star K]
[star_module K E]
[star_module K F]
(f g : E →ₗ[K] F) :
theorem
linear_map.real_sum
{E : Type u_1}
{F : Type u_2}
{K : Type u_3}
[add_comm_monoid E]
[star_add_monoid E]
[add_comm_monoid F]
[star_add_monoid F]
[semiring K]
[module K E]
[module K F]
[has_involutive_star K]
[star_module K E]
[star_module K F]
{n : Type u_4}
{s : finset n}
(f : n → (E →ₗ[K] F)) :
theorem
linear_map.real_real
{E : Type u_1}
{F : Type u_2}
{K : Type u_3}
[add_comm_monoid E]
[star_add_monoid E]
[add_comm_monoid F]
[star_add_monoid F]
[semiring K]
[module K E]
[module K F]
[has_involutive_star K]
[star_module K E]
[star_module K F]
(f : E →ₗ[K] F) :
theorem
linear_map.real_comp
{E : Type u_1}
{F : Type u_2}
{K : Type u_3}
[add_comm_monoid E]
[star_add_monoid E]
[add_comm_monoid F]
[star_add_monoid F]
[semiring K]
[module K E]
[module K F]
[has_involutive_star K]
[star_module K E]
[star_module K F]
{G : Type u_4}
[add_comm_monoid G]
[star_add_monoid G]
[module K G]
[star_module K G]
(f : E →ₗ[K] F)
(g : G →ₗ[K] E) :
theorem
linear_map.real_star_alg_equiv_conj
{E : Type u_1}
{K : Type u_2}
[comm_semiring K]
[semiring E]
[algebra K E]
[has_involutive_star K]
[star_add_monoid E]
[star_module K E]
(f : E →ₗ[K] E)
(φ : E ≃⋆ₐ[K] E) :
theorem
linear_map.real_star_alg_equiv_conj_iff
{E : Type u_1}
{K : Type u_2}
[comm_semiring K]
[semiring E]
[algebra K E]
[has_involutive_star K]
[star_add_monoid E]
[star_module K E]
(f : E →ₗ[K] E)
(φ : E ≃⋆ₐ[K] E) :
def
linear_map.real_ring_equiv
{R : Type u_1}
{E : Type (max u_2 u_3)}
[semiring R]
[add_comm_monoid E]
[star_add_monoid E]
[module R E]
[has_involutive_star R]
[star_module R E] :
theorem
linear_map.mul_right_real
{E : Type u_1}
{K : Type u_2}
[comm_semiring K]
[non_unital_semiring E]
[has_involutive_star K]
[star_ring E]
[module K E]
[star_module K E]
[smul_comm_class K E E]
[is_scalar_tower K E E]
(x : E) :
(linear_map.mul_right K x).real = linear_map.mul_left K (has_star.star x)
theorem
linear_map.mul_left_real
{E : Type u_1}
{K : Type u_2}
[comm_semiring K]
[non_unital_semiring E]
[has_involutive_star K]
[star_ring E]
[module K E]
[star_module K E]
[smul_comm_class K E E]
[is_scalar_tower K E E]
(x : E) :
(linear_map.mul_left K x).real = linear_map.mul_right K (has_star.star x)
theorem
linear_map.real.spectrum
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[star_add_monoid E]
[star_module 𝕜 E]
[finite_dimensional 𝕜 E]
(φ : E →ₗ[𝕜] E) :
spectrum 𝕜 φ.real = has_star.star (spectrum 𝕜 φ)
theorem
linear_map.real.eigenspace
{𝕜 : Type u_1}
[is_R_or_C 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[star_add_monoid E]
[star_module 𝕜 E]
(φ : E →ₗ[𝕜] E)
(α : 𝕜)
(x : E) :
x ∈ module.End.eigenspace φ.real α ↔ has_star.star x ∈ module.End.eigenspace φ (has_star.star α)
theorem
linear_map.real_neg
{E : Type u_1}
{F : Type u_2}
{K : Type u_3}
[add_comm_monoid E]
[star_add_monoid E]
[add_comm_group F]
[star_add_monoid F]
[semiring K]
[module K E]
[module K F]
[has_involutive_star K]
[star_module K E]
[star_module K F]
(f : E →ₗ[K] F) :
theorem
linear_map.real_sub
{E : Type u_1}
{F : Type u_2}
{K : Type u_3}
[add_comm_monoid E]
[star_add_monoid E]
[add_comm_group F]
[star_add_monoid F]
[semiring K]
[module K E]
[module K F]
[has_involutive_star K]
[star_module K E]
[star_module K F]
(f g : E →ₗ[K] F) :
theorem
linear_map.real_smul
{E : Type u_1}
{F : Type u_2}
{K : Type u_3}
[comm_semiring K]
[add_comm_monoid E]
[add_comm_monoid F]
[star_ring K]
[star_add_monoid E]
[star_add_monoid F]
[module K E]
[module K F]
[star_module K E]
[star_module K F]
(f : E →ₗ[K] F)
(α : K) :
theorem
linear_map.real_inj_eq
{E : Type u_1}
{F : Type u_2}
{K : Type u_3}
[semiring K]
[add_comm_monoid E]
[add_comm_monoid F]
[has_involutive_star K]
[star_add_monoid E]
[star_add_monoid F]
[module K E]
[module K F]
[star_module K E]
[star_module K F]
(f g : E →ₗ[K] F) :
theorem
linear_map.is_real_one
{E : Type u_1}
{K : Type u_2}
[semiring K]
[add_comm_monoid E]
[module K E]
[has_star E] :
1.is_real
theorem
linear_map.real_one
{E : Type u_1}
{K : Type u_2}
[semiring K]
[has_involutive_star K]
[add_comm_monoid E]
[star_add_monoid E]
[module K E]
[star_module K E] :