# Documentation

Mathlib.Data.Complex.Module

# Complex number as a vector space over ℝ#

This file contains the following instances:

• Any •-structure (SMul, MulAction, DistribMulAction, 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.reLm (ℝ-linear map);
• Complex.imLm (ℝ-linear map);
• Complex.ofRealAm (ℝ-algebra (homo)morphism);
• Complex.conjAe (ℝ-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 realPart and imaginaryPart for any element of a StarModule over ℂ.

## Notation #

• ℜ and ℑ for the realPart and imaginaryPart, respectively, in the locale ComplexStarModule.
instance Complex.mulAction {R : Type u_1} [] [] :
instance Complex.distribSMul {R : Type u_1} [] :
@[simp]
theorem AlgHom.map_coe_real_complex {A : Type u_3} [] [] (f : ) (x : ) :
f x = ↑() x

We need this lemma since Complex.coe_algebraMap diverts the simp-normal form away from AlgHom.commutes.

theorem Complex.algHom_ext {A : Type u_3} [] [] ⦃f : ⦃g : (h : = ) :
f = g

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

noncomputable def Complex.basisOneI :

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

Instances For
@[simp]
theorem Complex.coe_basisOneI_repr (z : ) :
↑(Complex.basisOneI.repr z) = ![z.re, z.im]
@[simp]
@[simp]

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

instance Module.complexToReal (E : Type u_1) [] [] :
instance Module.real_complex_tower (E : Type u_1) [] [] :
@[simp]
theorem Complex.coe_smul {E : Type u_1} [] [] (x : ) (y : E) :
x y = x y
instance SMulCommClass.complexToReal {M : Type u_1} {E : Type u_2} [] [] [SMul M E] [] :

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

instance FiniteDimensional.complexToReal (E : Type u_1) [] [] [] :
theorem rank_real_of_complex (E : Type u_1) [] [] :
= 2 *
theorem finrank_real_of_complex (E : Type u_1) [] [] :
instance StarModule.complexToReal {E : Type u_1} [] [Star E] [] [] :

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

Instances For
@[simp]

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

Instances For
@[simp]

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

Instances For
@[simp]

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

Instances For
@[simp]
@[simp]
theorem Complex.toMatrix_conjAe :
= Matrix.of ![![1, 0], ![0, -1]]

The matrix representation of conjAe.

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

@[simp]
theorem Complex.equivRealProdAddHom_apply (z : ) :
= (z.re, z.im)
@[simp]
theorem Complex.equivRealProdAddHom_symm_apply_re (p : ) :
().re = p.fst
@[simp]
theorem Complex.equivRealProdAddHom_symm_apply_im (p : ) :
().im = p.snd

The natural AddEquiv from ℂ to ℝ × ℝ.

Instances For
@[simp]
theorem Complex.equivRealProdLm_symm_apply_re :
∀ (a : ), ().re = a.fst
@[simp]
theorem Complex.equivRealProdLm_symm_apply_im :
∀ (a : ), ().im = a.snd
@[simp]
theorem Complex.equivRealProdLm_apply :
∀ (a : ), = (a.re, a.im)

The natural LinearEquiv from ℂ to ℝ × ℝ.

Instances For
def Complex.liftAux {A : Type u_1} [Ring 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.

Instances For
@[simp]
theorem Complex.liftAux_apply {A : Type u_1} [Ring A] [] (I' : A) (hI' : I' * I' = -1) (z : ) :
↑(Complex.liftAux I' hI') z = ↑() z.re + z.im I'
theorem Complex.liftAux_apply_I {A : Type u_1} [Ring A] [] (I' : A) (hI' : I' * I' = -1) :
↑(Complex.liftAux I' hI') Complex.I = I'
@[simp]
theorem Complex.lift_symm_apply_coe {A : Type u_1} [Ring A] [] (F : ) :
↑(Complex.lift.symm F) =
@[simp]
theorem Complex.lift_apply {A : Type u_1} [Ring A] [] (I' : { I' // I' * I' = -1 }) :
Complex.lift I' = Complex.liftAux I' (_ : I' * I' = -1)
def Complex.lift {A : Type u_1} [Ring A] [] :
{ I' // I' * I' = -1 } ()

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.

Instances For
@[simp]
@[simp]
@[simp]
theorem skewAdjoint.negISMul_apply_coe {A : Type u_1} [] [] [] [] (a : { x // x }) :
def skewAdjoint.negISMul {A : Type u_1} [] [] [] [] :
{ x // x } →ₗ[] { x // x }

Create a selfAdjoint element from a skewAdjoint element by multiplying by the scalar -Complex.I.

Instances For
theorem skewAdjoint.I_smul_neg_I {A : Type u_1} [] [] [] [] (a : { x // x }) :
noncomputable def realPart {A : Type u_1} [] [] [] [] :
A →ₗ[] { x // x }

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

Instances For
noncomputable def imaginaryPart {A : Type u_1} [] [] [] [] :
A →ₗ[] { x // x }

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 selfAdjoint and skewAdjoint parts, but in a star module over ℂ we have realPart_add_I_smul_imaginaryPart, which allows us to decompose into a linear combination of selfAdjoints.

Instances For

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

Instances For

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 selfAdjoint and skewAdjoint parts, but in a star module over ℂ we have realPart_add_I_smul_imaginaryPart, which allows us to decompose into a linear combination of selfAdjoints.

Instances For
theorem realPart_apply_coe {A : Type u_1} [] [] [] [] (a : A) :
↑(realPart a) = 2⁻¹ (a + star a)
theorem imaginaryPart_apply_coe {A : Type u_1} [] [] [] [] (a : A) :
↑(imaginaryPart a) = 2⁻¹ (a - star a)
theorem realPart_add_I_smul_imaginaryPart {A : Type u_1} [] [] [] [] (a : A) :
↑(realPart a) + Complex.I ↑(imaginaryPart 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 realPart_I_smul {A : Type u_1} [] [] [] [] (a : A) :
realPart () = -imaginaryPart a
@[simp]
theorem imaginaryPart_I_smul {A : Type u_1} [] [] [] [] (a : A) :
imaginaryPart () = realPart a
theorem realPart_smul {A : Type u_1} [] [] [] [] (z : ) (a : A) :
realPart (z a) = z.re realPart a - z.im imaginaryPart a
theorem imaginaryPart_smul {A : Type u_1} [] [] [] [] (z : ) (a : A) :
imaginaryPart (z a) = z.re imaginaryPart a + z.im realPart a
theorem skewAdjointPart_eq_I_smul_imaginaryPart {A : Type u_1} [] [] [] [] (x : A) :
↑(↑() x) = Complex.I ↑(imaginaryPart x)
theorem imaginaryPart_eq_neg_I_smul_skewAdjointPart {A : Type u_1} [] [] [] [] (x : A) :
↑(imaginaryPart x) = ↑(↑() x)
theorem IsSelfAdjoint.coe_realPart {A : Type u_1} [] [] [] [] {x : A} (hx : ) :
↑(realPart x) = x
theorem IsSelfAdjoint.imaginaryPart {A : Type u_1} [] [] [] [] {x : A} (hx : ) :
imaginaryPart x = 0
theorem realPart_comp_subtype_selfAdjoint {A : Type u_1} [] [] [] [] :
LinearMap.comp realPart () = LinearMap.id
theorem imaginaryPart_comp_subtype_selfAdjoint {A : Type u_1} [] [] [] [] :
LinearMap.comp imaginaryPart () = 0
@[simp]
theorem imaginaryPart_realPart {A : Type u_1} [] [] [] [] {x : A} :
imaginaryPart ↑(realPart x) = 0
@[simp]
theorem imaginaryPart_imaginaryPart {A : Type u_1} [] [] [] [] {x : A} :
imaginaryPart ↑(imaginaryPart x) = 0
@[simp]
theorem realPart_idem {A : Type u_1} [] [] [] [] {x : A} :
realPart ↑(realPart x) = realPart x
@[simp]
theorem realPart_imaginaryPart {A : Type u_1} [] [] [] [] {x : A} :
realPart ↑(imaginaryPart x) = imaginaryPart x
theorem realPart_surjective {A : Type u_1} [] [] [] [] :
theorem imaginaryPart_surjective {A : Type u_1} [] [] [] [] :
Function.Surjective imaginaryPart
theorem span_selfAdjoint {A : Type u_1} [] [] [] [] :
@[simp]
theorem Complex.selfAdjointEquiv_symm_apply (x : ) :
= { val := x, property := (_ : ↑() x = x) }
@[simp]
theorem Complex.selfAdjointEquiv_apply (z : { x // }) :
= (z).re

The natural ℝ-linear equivalence between selfAdjoint ℂ and ℝ.

Instances For
theorem Complex.coe_selfAdjointEquiv (z : { x // }) :
↑() = z
@[simp]
theorem realPart_ofReal (r : ) :
↑(realPart r) = r
@[simp]
theorem imaginaryPart_ofReal (r : ) :
imaginaryPart r = 0
theorem Complex.coe_realPart (z : ) :
↑(realPart z) = z.re
@[simp]
@[simp]

ℂ and ℝ are isomorphic as vector spaces over ℚ, or equivalently, as additive groups.