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} [SMul R ℝ] [SMul S ℝ] [SMulCommClass R S ℝ] : SMulCommClass R S ℂ

Equations

• ⋯ = ⋯

@[instance 90]

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

Equations

• ⋯ = ⋯

@[instance 90]

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

Equations

• ⋯ = ⋯

@[instance 90]

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

Equations

• Complex.mulAction = MulAction.mk ⋯ ⋯

@[instance 90]

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

Equations

• Complex.distribSMul = DistribSMul.mk ⋯

@[instance 90]

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

Equations

• Complex.instDistribMulActionOfReal = let __src := Complex.distribSMul; let __src_1 := Complex.mulAction; DistribMulAction.mk ⋯ ⋯

@[instance 100]

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

Equations

• Complex.instModule = Module.mk ⋯ ⋯

@[instance 95]

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

Equations

• Complex.instAlgebraOfReal = let __src := Complex.ofReal.comp (algebraMap R ℝ); Algebra.mk __src ⋯ ⋯

instance Complex.instStarModuleReal : StarModule ℝ ℂ

Equations

• Complex.instStarModuleReal = ⋯

@[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.

Equations

• One or more equations did not get rendered due to their size.

@[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.instFiniteDimensionalReal : FiniteDimensional ℝ ℂ

Equations

• Complex.instFiniteDimensionalReal = ⋯

@[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 900]

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

Equations

• Module.complexToReal E = RestrictScalars.module ℝ ℂ E

@[instance 900]

instance Algebra.complexToReal {A : Type u_1} [Semiring A] [Algebra ℂ A] : Algebra ℝ A

Equations

• Algebra.complexToReal = RestrictScalars.algebra ℝ ℂ A

@[simp]

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

@[instance 900]

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.

Equations

• ⋯ = ⋯

instance IsScalarTower.complexToReal {M : Type u_1} {E : Type u_2} [AddCommGroup M] [Module ℂ M] [AddCommGroup E] [Module ℂ E] [SMul M E] [IsScalarTower ℂ M E] : IsScalarTower ℝ 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) [AddCommGroup E] [Module ℂ E] [FiniteDimensional ℂ E] : FiniteDimensional ℝ E

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

def Complex.reLm : ℂ →ₗ[ℝ] ℝ

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

Equations

• Complex.reLm = { toFun := fun (x : ℂ) => x.re, map_add' := Complex.add_re, map_smul' := Complex.reLm.proof_1 }

@[simp]

theorem Complex.reLm_coe : ⇑Complex.reLm = Complex.re

def Complex.imLm : ℂ →ₗ[ℝ] ℝ

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

Equations

• Complex.imLm = { toFun := fun (x : ℂ) => x.im, map_add' := Complex.add_im, map_smul' := Complex.imLm.proof_1 }

@[simp]

theorem Complex.imLm_coe : ⇑Complex.imLm = Complex.im

def Complex.ofRealAm : ℝ →ₐ[ℝ] ℂ

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

Equations

• Complex.ofRealAm = Algebra.ofId ℝ ℂ

@[simp]

theorem Complex.ofRealAm_coe : ⇑Complex.ofRealAm = Complex.ofReal'

def Complex.conjAe : ℂ ≃ₐ[ℝ] ℂ

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complex.conjAe_coe : ⇑Complex.conjAe = ⇑(starRingEnd ℂ)

@[simp]

theorem Complex.toMatrix_conjAe : (LinearMap.toMatrix Complex.basisOneI Complex.basisOneI) Complex.conjAe.toLinearMap = 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_im (p : ℝ × ℝ) : (Complex.equivRealProdAddHom.symm p).im = p.2

@[simp]

theorem Complex.equivRealProdAddHom_symm_apply_re (p : ℝ × ℝ) : (Complex.equivRealProdAddHom.symm p).re = p.1

def Complex.equivRealProdAddHom : ℂ ≃+ ℝ × ℝ

The natural AddEquiv from ℂ to ℝ × ℝ.

Equations

• Complex.equivRealProdAddHom = let __src := Complex.equivRealProd; { toEquiv := __src, map_add' := Complex.equivRealProdAddHom.proof_1 }

theorem Complex.equivRealProdAddHom_symm_apply (p : ℝ × ℝ) : Complex.equivRealProdAddHom.symm p = ↑p.1 + ↑p.2 * Complex.I

@[simp]

theorem Complex.equivRealProdLm_symm_apply_im : ∀ (a : ℝ × ℝ), (Complex.equivRealProdLm.symm 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 : ℝ × ℝ), (Complex.equivRealProdLm.symm a).re = a.1

def Complex.equivRealProdLm : ℂ ≃ₗ[ℝ] ℝ × ℝ

The natural LinearEquiv from ℂ to ℝ × ℝ.

Equations

• One or more equations did not get rendered due to their size.

theorem Complex.equivRealProdLm_symm_apply (p : ℝ × ℝ) : Complex.equivRealProdLm.symm p = ↑p.1 + ↑p.2 * Complex.I

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.

Equations

• Complex.liftAux I' hf = AlgHom.ofLinearMap (Algebra.linearMap ℝ A ∘ₗ Complex.reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ Complex.imLm) ⋯ ⋯

@[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_apply {A : Type u_1} [Ring A] [Algebra ℝ 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] [Algebra ℝ A] (F : ℂ →ₐ[ℝ] A) : ↑(Complex.lift.symm F) = F Complex.I

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

• Complex.lift = { toFun := fun (I' : { I' : A // I' * I' = -1 }) => Complex.liftAux ↑I' ⋯, invFun := fun (F : ℂ →ₐ[ℝ] A) => ⟨F Complex.I, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[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.conjAe

@[simp]

theorem skewAdjoint.negISMul_apply_coe {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : ↥(skewAdjoint A)) : ↑(skewAdjoint.negISMul a) = -Complex.I • ↑a

def skewAdjoint.negISMul {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] : ↥(skewAdjoint A) →ₗ[ℝ] ↥(selfAdjoint A)

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

Equations

• skewAdjoint.negISMul = { toFun := fun (a : ↥(skewAdjoint A)) => ⟨-Complex.I • ↑a, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

theorem skewAdjoint.I_smul_neg_I {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : ↥(skewAdjoint A)) : Complex.I • ↑(skewAdjoint.negISMul a) = ↑a

noncomputable def realPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] : A →ₗ[ℝ] ↥(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.

Equations

• realPart = selfAdjointPart ℝ

noncomputable def imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] : A →ₗ[ℝ] ↥(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.

Equations

• imaginaryPart = skewAdjoint.negISMul ∘ₗ skewAdjointPart ℝ

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.

Equations

• ComplexStarModule.termℜ = Lean.ParserDescr.node `ComplexStarModule.termℜ 1024 (Lean.ParserDescr.symbol "ℜ")

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.

Equations

• ComplexStarModule.termℑ = Lean.ParserDescr.node `ComplexStarModule.termℑ 1024 (Lean.ParserDescr.symbol "ℑ")

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] : realPart ∘ₗ (selfAdjoint.submodule ℝ A).subtype = LinearMap.id

theorem imaginaryPart_comp_subtype_selfAdjoint {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] : imaginaryPart ∘ₗ (selfAdjoint.submodule ℝ A).subtype = 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_apply (z : ↥(selfAdjoint ℂ)) : Complex.selfAdjointEquiv z = (↑z).re

@[simp]

theorem Complex.selfAdjointEquiv_symm_apply (x : ℝ) : Complex.selfAdjointEquiv.symm x = ⟨↑x, ⋯⟩

def Complex.selfAdjointEquiv : ↥(selfAdjoint ℂ) ≃ₗ[ℝ] ℝ

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

Equations

• One or more equations did not get rendered due to their size.

theorem Complex.coe_selfAdjointEquiv (z : ↥(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

theorem star_mul_self_add_self_mul_star {A : Type u_2} [NonUnitalRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] (a : A) : star a * a + a * star a = 2 • (↑(realPart a) * ↑(realPart a) + ↑(imaginaryPart a) * ↑(imaginaryPart a))

@[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.