# 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`.

source
@[instance 90]
instance Complex.instSMulCommClassOfReal {R : Type u_1} {S : Type u_2} [SMul R ℝ] [SMul S ℝ] [SMulCommClass R S ℝ] :
SMulCommClass R S ℂ
source
@[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 ℂ
source
@[instance 90]
instance Complex.instIsCentralScalarOfReal {R : Type u_1} [SMul R ℝ] [SMul R ᵐᵒᵖ ℝ] [IsCentralScalar R ℝ] :
IsCentralScalar R ℂ
source
@[instance 90]
instance Complex.mulAction {R : Type u_1} [Monoid R] [MulAction R ℝ] :
MulAction R ℂ
Equations

- Complex.mulAction = { toSMul := Complex.SMul.instSMulRealComplex, one_smul := ⋯, mul_smul := ⋯ }

source
@[instance 90]
instance Complex.distribSMul {R : Type u_1} [DistribSMul R ℝ] :
DistribSMul R ℂ
Equations

- Complex.distribSMul = { toSMul := Complex.SMul.instSMulRealComplex, smul_zero := ⋯, smul_add := ⋯ }

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

- Complex.instDistribMulActionOfReal = { toSMul := Complex.distribSMul.toSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

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

- Complex.instModule = { toDistribMulAction := Complex.instDistribMulActionOfReal, add_smul := ⋯, zero_smul := ⋯ }

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

- Complex.instAlgebraOfReal = { toSMul := Complex.SMul.instSMulRealComplex, algebraMap := Complex.ofRealHom.comp (algebraMap R ℝ), commutes' := ⋯, smul_def' := ⋯ }

source
instance Complex.instStarModuleReal :
StarModule ℝ ℂ
source
@[simp]
theorem Complex.coe_algebraMap :
⇑(algebraMap ℝ ℂ) = ofReal
source
@[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`.

source
theorem Complex.algHom_ext {A : Type u_3} [Semiring A] [Algebra ℝ A] ⦃f g : ℂ →ₐ[ℝ] A⦄ (h : f I = g I) :
f = g

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

source
theorem Complex.algHom_ext_iff {A : Type u_3} [Semiring A] [Algebra ℝ A] {f g : ℂ →ₐ[ℝ] A} :
f = g ↔ f I = g I
source
noncomputable def Complex.basisOneI :
Module.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.

Instances For

source
@[simp]
theorem Complex.coe_basisOneI_repr (z : ℂ) :
⇑(basisOneI.repr z) = ![z.re, z.im]
source
@[simp]
theorem Complex.coe_basisOneI :
⇑basisOneI = ![1, I]
source
@[instance 900]
instance Module.complexToReal (E : Type u_1) [AddCommGroup E] [Module ℂ E] :
Module ℝ E
Equations

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

source
@[instance 900]
instance Algebra.complexToReal {A : Type u_1} [Semiring A] [Algebra ℂ A] :
Algebra ℝ A
Equations

- Algebra.complexToReal = RestrictScalars.algebra ℝ ℂ A

source
@[simp]
theorem Complex.coe_smul {E : Type u_1} [AddCommGroup E] [Module ℂ E] (x : ℝ) (y : E) :
↑x • y = x • y
source
@[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`.

source
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`.

source
@[instance 900]
instance StarModule.complexToReal {E : Type u_1} [AddCommGroup E] [Star E] [Module ℂ E] [StarModule ℂ E] :
StarModule ℝ E
source
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 }

Instances For

source
@[simp]
theorem Complex.reLm_coe :
⇑reLm = re
source
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 }

Instances For

source
@[simp]
theorem Complex.imLm_coe :
⇑imLm = im
source
def Complex.ofRealAm :
ℝ →ₐ[ℝ] ℂ

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

Equations

- Complex.ofRealAm = Algebra.ofId ℝ ℂ

Instances For

source
@[simp]
theorem Complex.ofRealAm_coe :
⇑ofRealAm = ofReal
source
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.

Instances For

source
@[simp]
theorem Complex.conjAe_coe :
⇑conjAe = ⇑(starRingEnd ℂ)
source
@[simp]
theorem Complex.toMatrix_conjAe :
(LinearMap.toMatrix basisOneI basisOneI) conjAe.toLinearMap = !![1, 0; 0, -1]

The matrix representation of `conjAe`.

source
theorem Complex.real_algHom_eq_id_or_conj (f : ℂ →ₐ[ℝ] ℂ) :
f = AlgHom.id ℝ ℂ ∨ f = ↑conjAe

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

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

The natural `LinearEquiv` from `ℂ` to `ℝ × ℝ`.

Equations

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

Instances For

source
@[simp]
theorem Complex.equivRealProdLm_symm_apply_im (a✝ : ℝ × ℝ) :
(equivRealProdLm.symm a✝).im = a✝.2
source
@[simp]
theorem Complex.equivRealProdLm_symm_apply_re (a✝ : ℝ × ℝ) :
(equivRealProdLm.symm a✝).re = a✝.1
source
@[simp]
theorem Complex.equivRealProdLm_apply (a✝ : ℂ) :
equivRealProdLm a✝ = (a✝.re, a✝.im)
source
theorem Complex.equivRealProdLm_symm_apply (p : ℝ × ℝ) :
equivRealProdLm.symm p = ↑p.1 + ↑p.2 * I
source
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) ⋯ ⋯

Instances For

source
@[simp]
theorem Complex.liftAux_apply {A : Type u_1} [Ring A] [Algebra ℝ A] (I' : A) (hI' : I' * I' = -1) (z : ℂ) :
(liftAux I' hI') z = (algebraMap ℝ A) z.re + z.im • I'
source
theorem Complex.liftAux_apply_I {A : Type u_1} [Ring A] [Algebra ℝ A] (I' : A) (hI' : I' * I' = -1) :
(liftAux I' hI') I = I'
source
@[simp]
theorem Complex.adjoin_I :
Algebra.adjoin ℝ {I} = ⊤
source
@[simp]
theorem Complex.range_liftAux {A : Type u_1} [Ring A] [Algebra ℝ A] (I' : A) (hI' : I' * I' = -1) :
(liftAux I' hI').range = Algebra.adjoin ℝ {I'}
source
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 `Quaternion`s.

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 := ⋯ }

Instances For

source
@[simp]
theorem Complex.lift_apply {A : Type u_1} [Ring A] [Algebra ℝ A] (I' : { I' : A // I' * I' = -1 }) :
lift I' = liftAux ↑I' ⋯
source
@[simp]
theorem Complex.lift_symm_apply_coe {A : Type u_1} [Ring A] [Algebra ℝ A] (F : ℂ →ₐ[ℝ] A) :
↑(lift.symm F) = F I
source
@[simp]
theorem Complex.liftAux_I :
liftAux I I_mul_I = AlgHom.id ℝ ℂ
source
@[simp]
theorem Complex.liftAux_neg_I :
liftAux (-I) ⋯ = ↑conjAe
source
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' := ⋯ }

Instances For

source
@[simp]
theorem skewAdjoint.negISMul_apply_coe {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : ↥(skewAdjoint A)) :
↑(negISMul a) = -Complex.I • ↑a
source
theorem skewAdjoint.I_smul_neg_I {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : ↥(skewAdjoint A)) :
Complex.I • ↑(negISMul a) = ↑a
source
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 ℝ

Instances For

source
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 `selfAdjoint`s.

Equations

- imaginaryPart = skewAdjoint.negISMul ∘ₗ skewAdjointPart ℝ

Instances For

source
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 "ℜ")

Instances For

source
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 `selfAdjoint`s.

Equations

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

Instances For

source
theorem realPart_apply_coe {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] (a : A) :
↑(realPart a) = 2⁻¹ • (a + star a)
source
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)
source
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.

source
@[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
source
@[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
source
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
source
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
source
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)
source
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)
source
theorem IsSelfAdjoint.coe_realPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} (hx : IsSelfAdjoint x) :
↑(realPart x) = x
source
theorem IsSelfAdjoint.imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} (hx : IsSelfAdjoint x) :
_root_.imaginaryPart x = 0
source
theorem realPart_comp_subtype_selfAdjoint {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] :
realPart ∘ₗ (selfAdjoint.submodule ℝ A).subtype = LinearMap.id
source
theorem imaginaryPart_comp_subtype_selfAdjoint {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] :
imaginaryPart ∘ₗ (selfAdjoint.submodule ℝ A).subtype = 0
source
@[simp]
theorem selfAdjoint.realPart_coe {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : ↥(selfAdjoint A)} :
realPart ↑x = x
source
@[simp]
theorem selfAdjoint.imaginaryPart_coe {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : ↥(selfAdjoint A)} :
imaginaryPart ↑x = 0
source
theorem imaginaryPart_realPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} :
imaginaryPart ↑(realPart x) = 0
source
theorem imaginaryPart_imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} :
imaginaryPart ↑(imaginaryPart x) = 0
source
theorem realPart_idem {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} :
realPart ↑(realPart x) = realPart x
source
theorem realPart_imaginaryPart {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] {x : A} :
realPart ↑(imaginaryPart x) = imaginaryPart x
source
theorem realPart_surjective {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] :
Function.Surjective ⇑realPart
source
theorem imaginaryPart_surjective {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] :
Function.Surjective ⇑imaginaryPart
source
theorem span_selfAdjoint {A : Type u_1} [AddCommGroup A] [Module ℂ A] [StarAddMonoid A] [StarModule ℂ A] :
Submodule.span ℂ ↑(selfAdjoint A) = ⊤
source
def Complex.selfAdjointEquiv :
↥(selfAdjoint ℂ) ≃ₗ[ℝ] ℝ

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

Equations

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

Instances For

source
@[simp]
theorem Complex.selfAdjointEquiv_apply (z : ↥(selfAdjoint ℂ)) :
selfAdjointEquiv z = (↑z).re
source
@[simp]
theorem Complex.selfAdjointEquiv_symm_apply (x : ℝ) :
selfAdjointEquiv.symm x = ⟨↑x, ⋯⟩
source
theorem Complex.coe_selfAdjointEquiv (z : ↥(selfAdjoint ℂ)) :
↑(selfAdjointEquiv z) = ↑z
source
@[simp]
theorem realPart_ofReal (r : ℝ) :
↑(realPart ↑r) = ↑r
source
@[simp]
theorem imaginaryPart_ofReal (r : ℝ) :
imaginaryPart ↑r = 0
source
theorem Complex.coe_realPart (z : ℂ) :
↑(realPart z) = ↑z.re
source
theorem star_mul_self_add_self_mul_star {A : Type u_2} [NonUnitalNonAssocRing 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))