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 ℂ

Equations

• @Complex.instSMulCommClassComplexInstSMulRealComplexInstSMulRealComplex = @Complex.instSMulCommClassComplexInstSMulRealComplexInstSMulRealComplex.proof_1

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

Equations

• @Complex.instIsScalarTowerComplexInstSMulRealComplexInstSMulRealComplex = @Complex.instIsScalarTowerComplexInstSMulRealComplexInstSMulRealComplex.proof_1

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

Equations

• @Complex.instIsCentralScalarComplexInstSMulRealComplexMulOpposite = @Complex.instIsCentralScalarComplexInstSMulRealComplexMulOpposite.proof_1

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

Equations

• Complex.mulAction = MulAction.mk (_ : ∀ (x : ℂ), 1 • x = x) (_ : ∀ (r s : R) (x : ℂ), (r * s) • x = r • s • x)

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

Equations

• Complex.distribSMul = DistribSMul.mk (_ : ∀ (r : R) (x y : ℂ), r • (x + y) = r • x + r • y)

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

Equations

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

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

Equations

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

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

Equations

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

instance Complex.instStarModuleRealComplexToStarToInvolutiveStarInstAddMonoidRealToStarAddMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingRealInstStarRingRealToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingRealToAddMonoidToAddMonoidWithOneAddGroupWithOneInstRingComplexInstStarRingComplexToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingComplexInstSMulRealComplexToSMulInstCommSemiringRealSemiringId : StarModule ℝ ℂ

Equations

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

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

Equations

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

@[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] : Module ℝ E

Equations

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

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

Equations

• Module.real_complex_tower = Module.real_complex_tower.proof_1

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

Equations

• @SMulCommClass.complexToReal = @SMulCommClass.complexToReal.proof_1

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

Equations

• FiniteDimensional.complexToReal = FiniteDimensional.complexToReal.proof_1

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

Equations

• @StarModule.complexToReal = @StarModule.complexToReal.proof_1

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

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

Equations

• Complex.reLm = { toAddHom := { 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 = { toAddHom := { 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) (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 ℝ × ℝ.

Equations

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

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

Equations

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

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

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

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

Equations

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

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

Equations

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

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.

Equations

• realPart = selfAdjointPart ℝ

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.

Equations

• imaginaryPart = LinearMap.comp 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] : 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 ℝ.

Equations

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

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.