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.instSMulCommClassComplexInstSMulRealComplexInstSMulRealComplex {R : Type u_1} {S : Type u_2} [SMul R ℝ] [SMul S ℝ] [SMulCommClass R S ℝ] :

SMulCommClass R S ℂ

instance Complex.instIsScalarTowerComplexInstSMulRealComplexInstSMulRealComplex {R : Type u_1} {S : Type u_2} [SMul R S] [SMul R ℝ] [SMul S ℝ] [IsScalarTower R S ℝ] :

IsScalarTower R S ℂ

instance Complex.instIsCentralScalarComplexInstSMulRealComplexMulOpposite {R : Type u_1} [SMul R ℝ] [SMul Rᵐᵒᵖ ℝ] [IsCentralScalar R ℝ] :

IsCentralScalar R ℂ

instance Complex.mulAction {R : Type u_1} [Monoid R] [MulAction R ℝ] :

MulAction R ℂ

instance Complex.distribSMul {R : Type u_1} [DistribSMul R ℝ] :

DistribSMul R ℂ

instance Complex.instDistribMulActionComplexToMonoidToMonoidWithZeroToAddMonoidToAddMonoidWithOneAddGroupWithOne {R : Type u_1} [Semiring R] [DistribMulAction R ℝ] :

DistribMulAction R ℂ

instance Complex.instModuleComplexToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingComplex {R : Type u_1} [Semiring R] [Module R ℝ] :

instance Complex.instAlgebraComplexInstSemiringComplex {R : Type u_1} [CommSemiring R] [Algebra R ℝ] :

instance Complex.instStarModuleRealComplexToStarToInvolutiveStarInstAddMonoidRealToStarAddMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingRealInstStarRingRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingRealToAddMonoidToAddMonoidWithOneAddGroupWithOneInstRingComplexInstStarRingComplexToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingComplexInstSMulRealComplexToSMulInstCommSemiringRealSemiringId :

StarModule ℝ ℂ

@[simp]

theorem Complex.coe_algebraMap :

↑(algebraMap ℝ ℂ) = Complex.ofReal'

@[simp]

theorem AlgHom.map_coe_real_complex {A : Type u_3} [Semiring A] [Algebra ℝ A] (f : ℂ →ₐ[ℝ ] A) (x : ℝ) :

↑f ↑x = ↑(algebraMap ℝ A) 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} [Semiring A] [Algebra ℝ A] ⦃f : ℂ →ₐ[ℝ ] A⦄ ⦃g : ℂ →ₐ[ℝ ] A⦄ (h : ↑f Complex.I = ↑g Complex.I) :

f = g

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

noncomputable def Complex.basisOneI :

Basis (Fin 2) ℝ ℂ

ℂ 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]

theorem Complex.coe_basisOneI :

↑Complex.basisOneI = ![1, Complex.I]

instance Complex.instFiniteDimensionalRealComplexInstDivisionRingRealAddCommGroupInstModuleComplexToAddCommMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingComplexToSemiringToDivisionSemiringToModule :

FiniteDimensional ℝ ℂ

@[simp]

theorem Complex.finrank_real_complex :

FiniteDimensional.finrank ℝ ℂ = 2

@[simp]

theorem Complex.rank_real_complex :

Module.rank ℝ ℂ = 2

theorem Complex.rank_real_complex' :

Cardinal.lift.{u, 0} (Module.rank ℝ ℂ) = 2

theorem Complex.finrank_real_complex_fact :

Fact (FiniteDimensional.finrank ℝ ℂ = 2)

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

instance Module.complexToReal (E : Type u_1) [AddCommGroup E] [Module ℂ E] :

instance Module.real_complex_tower (E : Type u_1) [AddCommGroup E] [Module ℂ E] :

IsScalarTower ℝ ℂ E

@[simp]

theorem Complex.coe_smul {E : Type u_1} [AddCommGroup E] [Module ℂ E] (x : ℝ) (y : E) :

↑x • y = x • y

instance SMulCommClass.complexToReal {M : Type u_1} {E : Type u_2} [AddCommGroup E] [Module ℂ E] [SMul M E] [SMulCommClass ℂ M E] :

SMulCommClass ℝ 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) [AddCommGroup E] [Module ℂ E] [FiniteDimensional ℂ E] :

FiniteDimensional ℝ E

theorem rank_real_of_complex (E : Type u_1) [AddCommGroup E] [Module ℂ E] :

Module.rank ℝ E = 2 * Module.rank ℂ E

theorem finrank_real_of_complex (E : Type u_1) [AddCommGroup E] [Module ℂ E] :

FiniteDimensional.finrank ℝ E = 2 * FiniteDimensional.finrank ℂ E

instance StarModule.complexToReal {E : Type u_1} [AddCommGroup E] [Star E] [Module ℂ E] [StarModule ℂ E] :

StarModule ℝ E

def Complex.reLm :

ℂ →ₗ[ℝ ] ℝ

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

Instances For

@[simp]

theorem Complex.reLm_coe :

↑Complex.reLm = Complex.re

def Complex.imLm :

ℂ →ₗ[ℝ ] ℝ

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

Instances For

@[simp]

theorem Complex.imLm_coe :

↑Complex.imLm = Complex.im

def Complex.ofRealAm :

ℝ →ₐ[ℝ ] ℂ

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

Instances For

@[simp]

theorem Complex.ofRealAm_coe :

↑Complex.ofRealAm = Complex.ofReal'

def Complex.conjAe :

ℂ ≃ₐ[ℝ ] ℂ

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

Instances For

@[simp]

theorem Complex.conjAe_coe :

↑Complex.conjAe = ↑(starRingEnd ℂ)

@[simp]

theorem Complex.toMatrix_conjAe :

↑(LinearMap.toMatrix Complex.basisOneI Complex.basisOneI) (AlgEquiv.toLinearMap Complex.conjAe) = ↑Matrix.of ![![1, 0], ![0, -1]]

The matrix representation of conjAe.

theorem Complex.real_algHom_eq_id_or_conj (f : ℂ →ₐ[ℝ ] ℂ) :

f = AlgHom.id ℝ ℂ ∨ f = ↑Complex.conjAe

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

@[simp]

theorem Complex.equivRealProdAddHom_apply (z : ℂ) :

↑Complex.equivRealProdAddHom z = (z.re, z.im)

@[simp]

theorem Complex.equivRealProdAddHom_symm_apply_re (p : ℝ × ℝ) :

(↑(AddEquiv.symm Complex.equivRealProdAddHom) p).re = p.fst

@[simp]

theorem Complex.equivRealProdAddHom_symm_apply_im (p : ℝ × ℝ) :

(↑(AddEquiv.symm Complex.equivRealProdAddHom) p).im = p.snd

def Complex.equivRealProdAddHom :

ℂ ≃+ ℝ × ℝ

The natural AddEquiv from ℂ to ℝ × ℝ.

Instances For

@[simp]

theorem Complex.equivRealProdLm_symm_apply_re :

∀ (a : ℝ × ℝ), (↑(LinearEquiv.symm Complex.equivRealProdLm) a).re = a.fst

@[simp]

theorem Complex.equivRealProdLm_symm_apply_im :

∀ (a : ℝ × ℝ), (↑(LinearEquiv.symm Complex.equivRealProdLm) a).im = a.snd

@[simp]

theorem Complex.equivRealProdLm_apply :

∀ (a : ℂ), ↑Complex.equivRealProdLm a = (a.re, a.im)

def Complex.equivRealProdLm :

ℂ ≃ₗ[ℝ ] ℝ × ℝ

The natural LinearEquiv from ℂ to ℝ × ℝ.

Instances For

def Complex.liftAux {A : Type u_1} [Ring A] [Algebra ℝ A] (I' : A) (hf : I' * I' = -1) :

ℂ →ₐ[ℝ ] A

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] [Algebra ℝ A] (I' : A) (hI' : I' * I' = -1) (z : ℂ) :

↑(Complex.liftAux I' hI') z = ↑(algebraMap ℝ A) z.re + z.im • I'

theorem Complex.liftAux_apply_I {A : Type u_1} [Ring A] [Algebra ℝ 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] [Algebra ℝ A] (F : ℂ →ₐ[ℝ ] A) :

↑(↑Complex.lift.symm F) = ↑F Complex.I

@[simp]

theorem Complex.lift_apply {A : Type u_1} [Ring A] [Algebra ℝ A] (I' : { I' // I' * I' = -1 }) :

↑Complex.lift I' = Complex.liftAux ↑I' (_ : ↑I' * ↑I' = -1)

def Complex.lift {A : Type u_1} [Ring A] [Algebra ℝ 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.

Instances For

@[simp]

theorem Complex.liftAux_I :

Complex.liftAux Complex.I Complex.I_mul_I = AlgHom.id ℝ ℂ

@[simp]

theorem Complex.liftAux_neg_I :

Complex.liftAux (-Complex.I) (_ : -Complex.I * -Complex.I = -1) = ↑Complex.conjAe

@[simp]

theorem skewAdjoint.negISMul_apply_coe {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : { x // x ∈ skewAdjoint A }) :

↑(↑skewAdjoint.negISMul a) = -Complex.I • ↑a

def skewAdjoint.negISMul {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] :

{ x // x ∈ skewAdjoint A } →ₗ[ℝ ] { x // x ∈ selfAdjoint A }

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} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : { x // x ∈ skewAdjoint A }) :

Complex.I • ↑(↑skewAdjoint.negISMul a) = ↑a

noncomputable def realPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] :

A →ₗ[ℝ ] { x // x ∈ selfAdjoint 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.

Instances For

noncomputable def imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] :

A →ₗ[ℝ ] { x // x ∈ selfAdjoint 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.

Instances For

def ComplexStarModule.termℜ :

Lean.ParserDescr

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

def ComplexStarModule.termℑ :

Lean.ParserDescr

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} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : A) :

↑(↑realPart a) = 2⁻¹ • (a + star a)

theorem imaginaryPart_apply_coe {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : A) :

↑(↑imaginaryPart a) = -Complex.I • 2⁻¹ • (a - star a)

theorem realPart_add_I_smul_imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (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} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : A) :

↑realPart (Complex.I • a) = -↑imaginaryPart a

@[simp]

theorem imaginaryPart_I_smul {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : A) :

↑imaginaryPart (Complex.I • a) = ↑realPart a

theorem realPart_smul {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (z : ℂ) (a : A) :

↑realPart (z • a) = z.re • ↑realPart a - z.im • ↑imaginaryPart a

theorem imaginaryPart_smul {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (z : ℂ) (a : A) :

↑imaginaryPart (z • a) = z.re • ↑imaginaryPart a + z.im • ↑realPart a

theorem skewAdjointPart_eq_I_smul_imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (x : A) :

↑(↑(skewAdjointPart ℝ) x) = Complex.I • ↑(↑imaginaryPart x)

theorem imaginaryPart_eq_neg_I_smul_skewAdjointPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (x : A) :

↑(↑imaginaryPart x) = -Complex.I • ↑(↑(skewAdjointPart ℝ) x)

theorem IsSelfAdjoint.coe_realPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} (hx : IsSelfAdjoint x) :

↑(↑realPart x) = x

theorem IsSelfAdjoint.imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} (hx : IsSelfAdjoint x) :

↑imaginaryPart x = 0

theorem realPart_comp_subtype_selfAdjoint {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] :

LinearMap.comp realPart (Submodule.subtype (selfAdjoint.submodule ℝ A)) = LinearMap.id

theorem imaginaryPart_comp_subtype_selfAdjoint {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] :

LinearMap.comp imaginaryPart (Submodule.subtype (selfAdjoint.submodule ℝ A)) = 0

@[simp]

theorem imaginaryPart_realPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} :

↑imaginaryPart ↑(↑realPart x) = 0

@[simp]

theorem imaginaryPart_imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} :

↑imaginaryPart ↑(↑imaginaryPart x) = 0

@[simp]

theorem realPart_idem {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} :

↑realPart ↑(↑realPart x) = ↑realPart x

@[simp]

theorem realPart_imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} :

↑realPart ↑(↑imaginaryPart x) = ↑imaginaryPart x

theorem realPart_surjective {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] :

Function.Surjective ↑realPart

theorem imaginaryPart_surjective {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] :

Function.Surjective ↑imaginaryPart

theorem span_selfAdjoint {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] :

Submodule.span ℂ ↑(selfAdjoint A) = ⊤

@[simp]

theorem Complex.selfAdjointEquiv_symm_apply (x : ℝ) :

↑(LinearEquiv.symm Complex.selfAdjointEquiv) x = { val := ↑x, property := (_ : ↑(starRingEnd ℂ) ↑x = ↑x) }

@[simp]

theorem Complex.selfAdjointEquiv_apply (z : { x // x ∈ selfAdjoint ℂ }) :

↑Complex.selfAdjointEquiv z = (↑z).re

def Complex.selfAdjointEquiv :

{ x // x ∈ selfAdjoint ℂ } ≃ₗ[ℝ ] ℝ

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

Instances For

theorem Complex.coe_selfAdjointEquiv (z : { x // x ∈ selfAdjoint ℂ }) :

↑(↑Complex.selfAdjointEquiv z) = ↑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]

theorem Real.rank_rat_real :

Module.rank ℚ ℝ = Cardinal.continuum

@[simp]

theorem Complex.rank_rat_complex :

Module.rank ℚ ℂ = Cardinal.continuum

theorem Complex.nonempty_linearEquiv_real :

Nonempty (ℂ ≃ₗ[ℚ ] ℝ)

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