# mathlib3documentation

data.complex.module

# Complex number as a vector space over ℝ#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains the following instances:

• Any •-structure (has_smul, mul_action, distrib_mul_action, module, algebra) on ℝ imbues a corresponding structure on ℂ. This includes the statement that ℂ is an ℝ algebra.
• any complex vector space is a real vector space;
• any finite dimensional complex vector space is a finite dimensional real vector space;
• the space of ℝ-linear maps from a real vector space to a complex vector space is a complex vector space.

It also defines bundled versions of four standard maps (respectively, the real part, the imaginary part, the embedding of ℝ in ℂ, and the complex conjugate):

• complex.re_lm (ℝ-linear map);
• complex.im_lm (ℝ-linear map);
• complex.of_real_am (ℝ-algebra (homo)morphism);
• complex.conj_ae (ℝ-algebra equivalence).

It also provides a universal property of the complex numbers complex.lift, which constructs a ℂ →ₐ[ℝ] A into any ℝ-algebra A given a square root of -1.

In addition, this file provides a decomposition into real_part and imaginary_part for any element of a star_module over ℂ.

## Notation #

• ℜ and ℑ for the real_part and imaginary_part, respectively, in the locale complex_star_module.
@[protected, instance]
def complex.has_smul {R : Type u_1} [ ] :
Equations
theorem complex.smul_re {R : Type u_1} [ ] (r : R) (z : ) :
(r z).re = r z.re
theorem complex.smul_im {R : Type u_1} [ ] (r : R) (z : ) :
(r z).im = r z.im
@[simp]
theorem complex.real_smul {x : } {z : } :
x z = x * z
@[protected, instance]
def complex.smul_comm_class {R : Type u_1} {S : Type u_2} [ ] [ ] [ ] :
@[protected, instance]
def complex.is_scalar_tower {R : Type u_1} {S : Type u_2} [ S] [ ] [ ] [ ] :
@[protected, instance]
def complex.is_central_scalar {R : Type u_1} [ ] [ ]  :
@[protected, instance]
def complex.mul_action {R : Type u_1} [monoid R] [ ] :
Equations
@[protected, instance]
def complex.distrib_smul {R : Type u_1} [ ] :
Equations
@[protected, instance]
def complex.distrib_mul_action {R : Type u_1} [semiring R]  :
Equations
@[protected, instance]
def complex.module {R : Type u_1} [semiring R] [ ] :
Equations
@[protected, instance]
def complex.algebra {R : Type u_1} [ ] :
Equations
@[protected, instance]
@[simp]
@[simp]
theorem alg_hom.map_coe_real_complex {A : Type u_3} [semiring A] [ A] (f : →ₐ[] A) (x : ) :
f x = A) x

We need this lemma since complex.coe_algebra_map diverts the simp-normal form away from alg_hom.commutes.

@[ext]
theorem complex.alg_hom_ext {A : Type u_3} [semiring A] [ A] ⦃f g : →ₐ[] A⦄ (h : = ) :
f = g

Two ℝ-algebra homomorphisms from ℂ are equal if they agree on complex.I.

@[protected]
theorem complex.ordered_smul  :
noncomputable def complex.basis_one_I  :

ℂ has a basis over ℝ given by 1 and I.

Equations
@[simp]
@[protected, instance]
@[simp]
@[simp]

fact version of the dimension of ℂ over ℝ, locally useful in the definition of the circle.

@[protected, instance]
def module.complex_to_real (E : Type u_1) [ E] :
E
Equations
@[protected, instance]
def module.real_complex_tower (E : Type u_1) [ E] :
@[simp, norm_cast]
theorem complex.coe_smul {E : Type u_1} [ E] (x : ) (y : E) :
x y = x y
@[protected, instance]
def smul_comm_class.complex_to_real {M : Type u_1} {E : Type u_2} [ E] [ E] [ E] :
E

The scalar action of ℝ on a ℂ-module E induced by module.complex_to_real commutes with another scalar action of M on E whenever the action of ℂ commutes with the action of M.

@[protected, instance]
def finite_dimensional.complex_to_real (E : Type u_1) [ E]  :
theorem rank_real_of_complex (E : Type u_1) [ E] :
= 2 *
theorem finrank_real_of_complex (E : Type u_1) [ E] :
@[protected, instance]
def star_module.complex_to_real {E : Type u_1} [has_star E] [ E] [ E] :
def complex.re_lm  :

Linear map version of the real part function, from ℂ to ℝ.

Equations
@[simp]
def complex.im_lm  :

Linear map version of the imaginary part function, from ℂ to ℝ.

Equations
@[simp]

ℝ-algebra morphism version of the canonical embedding of ℝ in ℂ.

Equations
@[simp]
def complex.conj_ae  :

ℝ-algebra isomorphism version of the complex conjugation function from ℂ to ℂ

Equations
@[simp]
theorem complex.conj_ae_coe  :
@[simp]

The matrix representation of conj_ae.

The identity and the complex conjugation are the only two ℝ-algebra homomorphisms of ℂ.

The natural add_equiv from ℂ to ℝ × ℝ.

Equations
@[simp]
theorem complex.equiv_real_prod_add_hom_apply (ᾰ : ) :
= (ᾰ.re, ᾰ.im)

The natural linear_equiv from ℂ to ℝ × ℝ.

Equations
@[simp]
theorem complex.equiv_real_prod_lm_apply (ᾰ : ) :
= (ᾰ.re, ᾰ.im)
@[simp]
@[simp]
def complex.lift_aux {A : Type u_1} [ring A] [ A] (I' : A) (hf : I' * I' = -1) :

There is an alg_hom from ℂ to any ℝ-algebra with an element that squares to -1.

See complex.lift for this as an equiv.

Equations
• hf =
@[simp]
theorem complex.lift_aux_apply {A : Type u_1} [ring A] [ A] (I' : A) (hI' : I' * I' = -1) (z : ) :
hI') z = A) z.re + z.im I'
theorem complex.lift_aux_apply_I {A : Type u_1} [ring A] [ A] (I' : A) (hI' : I' * I' = -1) :
hI') complex.I = I'
def complex.lift {A : Type u_1} [ring A] [ A] :
{I' // I' * I' = -1} ( →ₐ[] A)

A universal property of the complex numbers, providing a unique ℂ →ₐ[ℝ] A for every element of A which squares to -1.

This can be used to embed the complex numbers in the quaternions.

This isomorphism is named to match the very similar zsqrtd.lift.

Equations
@[simp]
theorem complex.lift_apply {A : Type u_1} [ring A] [ A] (I' : {I' // I' * I' = -1}) :
=
@[simp]
theorem complex.lift_symm_apply_coe {A : Type u_1} [ring A] [ A] (F : →ₐ[] A) :
@[simp]
@[simp]

Create a self_adjoint element from a skew_adjoint element by multiplying by the scalar -complex.I.

Equations
@[simp]
theorem skew_adjoint.neg_I_smul_apply_coe {A : Type u_1} [ A] [ A] (a : (skew_adjoint A)) :
theorem skew_adjoint.I_smul_neg_I {A : Type u_1} [ A] [ A] (a : (skew_adjoint A)) :
noncomputable def real_part {A : Type u_1} [ A] [ A] :

The real part ℜ a of an element a of a star module over ℂ, as a linear map. This is just self_adjoint_part ℝ, but we provide it as a separate definition in order to link it with lemmas concerning the imaginary_part, which doesn't exist in star modules over other rings.

Equations
noncomputable def imaginary_part {A : Type u_1} [ A] [ A] :

The imaginary part ℑ a of an element a of a star module over ℂ, as a linear map into the self adjoint elements. In a general star module, we have a decomposition into the self_adjoint and skew_adjoint parts, but in a star module over ℂ we have real_part_add_I_smul_imaginary_part, which allows us to decompose into a linear combination of self_adjoints.

Equations
@[simp]
theorem real_part_apply_coe {A : Type u_1} [ A] [ A] (a : A) :
@[simp]
theorem imaginary_part_apply_coe {A : Type u_1} [ A] [ A] (a : A) :
theorem real_part_add_I_smul_imaginary_part {A : Type u_1} [ A] [ A] (a : A) :

The standard decomposition of ℜ a + complex.I • ℑ a = a of an element of a star module over ℂ into a linear combination of self adjoint elements.

@[simp]
theorem real_part_I_smul {A : Type u_1} [ A] [ A] (a : A) :
@[simp]
theorem imaginary_part_I_smul {A : Type u_1} [ A] [ A] (a : A) :
theorem real_part_smul {A : Type u_1} [ A] [ A] (z : ) (a : A) :
theorem imaginary_part_smul {A : Type u_1} [ A] [ A] (z : ) (a : A) :