# 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 90]
instance Complex.instSMulCommClassOfReal {R : Type u_1} {S : Type u_2} [] [] [] :
Equations
• =
@[instance 90]
instance Complex.instIsScalarTowerOfReal {R : Type u_1} {S : Type u_2} [SMul R S] [] [] [] :
Equations
• =
@[instance 90]
instance Complex.instIsCentralScalarOfReal {R : Type u_1} [] [] [] :
Equations
• =
@[instance 90]
instance Complex.mulAction {R : Type u_1} [] [] :
Equations
• Complex.mulAction =
@[instance 90]
instance Complex.distribSMul {R : Type u_1} [] :
Equations
• Complex.distribSMul =
@[instance 90]
instance Complex.instDistribMulActionOfReal {R : Type u_1} [] [] :
Equations
• Complex.instDistribMulActionOfReal = let __src := Complex.distribSMul; let __src_1 := Complex.mulAction;
@[instance 100]
instance Complex.instModule {R : Type u_1} [] [] :
Equations
• Complex.instModule =
@[instance 95]
instance Complex.instAlgebraOfReal {R : Type u_1} [] [] :
Equations
@[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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Complex.coe_basisOneI_repr (z : ) :
(Complex.basisOneI.repr z) = ![z.re, z.im]
@[simp]
Equations
@[simp]

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

@[instance 900]
instance Module.complexToReal (E : Type u_1) [] [] :
Equations
@[instance 900]
instance Algebra.complexToReal {A : Type u_1} [] [] :
Equations
• Algebra.complexToReal =
@[simp]
theorem Complex.coe_smul {E : Type u_1} [] [] (x : ) (y : E) :
x y = x y
@[instance 900]
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.

Equations
• =
instance IsScalarTower.complexToReal {M : Type u_1} {E : Type u_2} [] [] [] [] [SMul M E] [] :

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

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

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

Equations
Instances For
@[simp]

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

Equations
Instances For
@[simp]

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

Equations
Instances For
@[simp]

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

Equations
• One or more equations did not get rendered due to their size.
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 : ) :
@[simp]
@[simp]

The natural AddEquiv from ℂ to ℝ × ℝ.

Equations
Instances For
@[simp]
theorem Complex.equivRealProdLm_symm_apply_im :
∀ (a : ), ( a).im = a.2
@[simp]
theorem Complex.equivRealProdLm_apply :
∀ (a : ), Complex.equivRealProdLm a = (a.re, a.im)
@[simp]
theorem Complex.equivRealProdLm_symm_apply_re :
∀ (a : ), ( a).re = a.1

The natural LinearEquiv from ℂ to ℝ × ℝ.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Complex.equivRealProdLm_symm_apply (p : ) :
p = p.1 + p.2 * Complex.I
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.

Equations
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) :
@[simp]
theorem Complex.lift_apply {A : Type u_1} [Ring A] [] (I' : { I' : A // I' * I' = -1 }) :
Complex.lift I' = Complex.liftAux I'
@[simp]
theorem Complex.lift_symm_apply_coe {A : Type u_1} [Ring A] [] (F : ) :
(Complex.lift.symm F) =
def Complex.lift {A : Type u_1} [Ring A] [] :
{ I' : A // 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.

Equations
• Complex.lift = { toFun := fun (I' : { I' : A // I' * I' = -1 }) => Complex.liftAux I' , invFun := fun (F : ) => ⟨, , left_inv := , right_inv := }
Instances For
@[simp]
@[simp]
@[simp]
theorem skewAdjoint.negISMul_apply_coe {A : Type u_1} [] [] [] [] (a : ()) :
def skewAdjoint.negISMul {A : Type u_1} [] [] [] [] :
() →ₗ[] ()

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

Equations
• skewAdjoint.negISMul = { toFun := fun (a : ()) => ⟨, , map_add' := , map_smul' := }
Instances For
theorem skewAdjoint.I_smul_neg_I {A : Type u_1} [] [] [] [] (a : ()) :
noncomputable def realPart {A : Type u_1} [] [] [] [] :
A →ₗ[] ()

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.

Equations
• realPart =
Instances For
noncomputable def imaginaryPart {A : Type u_1} [] [] [] [] :
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 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.

Equations
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.

Equations
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.

Equations
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} [] [] [] [] :
realPart ∘ₗ .subtype = LinearMap.id
theorem imaginaryPart_comp_subtype_selfAdjoint {A : Type u_1} [] [] [] [] :
imaginaryPart ∘ₗ .subtype = 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_apply (z : ()) :
@[simp]
theorem Complex.selfAdjointEquiv_symm_apply (x : ) :
x = x,

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Complex.coe_selfAdjointEquiv (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
theorem star_mul_self_add_self_mul_star {A : Type u_2} [] [] [] [] [] [] (a : A) :
star a * a + a * star a = 2 ((realPart a) * (realPart a) + (imaginaryPart a) * (imaginaryPart a))
@[simp]
@[simp]

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