Complex normed star modules and algebras #
Facts about star modules and star algebras over the complex numbers.
Main definitions #
star_module.mul_neg_I_lin: multiplication by -I as a real-linear equivalence between the skew-adjoint and self-adjoint elements of a star module.star_module.im: the imaginary part of an element of a star module, defined viaskew_adjoint_part.
@[simp]
theorem
star_module.mul_neg_I_lin_apply_coe
{E : Type u_1}
[add_comm_group E]
[star_add_monoid E]
[module ℂ E]
[star_module ℂ E]
(x : ↥(skew_adjoint E)) :
def
star_module.mul_neg_I_lin
{E : Type u_1}
[add_comm_group E]
[star_add_monoid E]
[module ℂ E]
[star_module ℂ E] :
↥(skew_adjoint E) ≃ₗ[ℝ] ↥(self_adjoint E)
Multiplication by -I as a real-linear equivalence between the skew-adjoint and self-adjoint elements of a star module.
@[simp]
theorem
star_module.mul_neg_I_lin_symm_apply_coe
{E : Type u_1}
[add_comm_group E]
[star_add_monoid E]
[module ℂ E]
[star_module ℂ E]
(x : ↥(self_adjoint E)) :
@[simp]
theorem
star_module.im_apply_coe
{E : Type u_1}
[add_comm_group E]
[star_add_monoid E]
[module ℂ E]
[star_module ℂ E]
(ᾰ : E) :
noncomputable
def
star_module.im
{E : Type u_1}
[add_comm_group E]
[star_add_monoid E]
[module ℂ E]
[star_module ℂ E] :
E →ₗ[ℝ] ↥(self_adjoint E)
The imaginary part of an element of a star module, as a real-linear map.
@[simp]
theorem
star_module.re_apply_coe
{E : Type u_1}
[add_comm_group E]
[star_add_monoid E]
[module ℂ E]
[star_module ℂ E]
(x : E) :
↑(⇑star_module.re x) = 2⁻¹ • x + 2⁻¹ • has_star.star x
noncomputable
def
star_module.re
{E : Type u_1}
[add_comm_group E]
[star_add_monoid E]
[module ℂ E]
[star_module ℂ E] :
E →ₗ[ℝ] ↥(self_adjoint E)
The real part of an element of a star module, as a real-linear map. This is simply an
abbreviation for self_adjoint_part ℝ.
theorem
star_module.re_add_im
{E : Type u_1}
[add_comm_group E]
[star_add_monoid E]
[module ℂ E]
[star_module ℂ E]
(x : E) :
↑(⇑star_module.re x) + complex.I • ↑(⇑star_module.im x) = x
An element of a complex star module can be decomposed into self-adjoint "real" and "imaginary" parts