mathlib3 documentation

data.complex.module

Complex number as a vector space over `ℝ` #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains the following instances:

Any •-structure (has_smul, mul_action, distrib_mul_action, 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.re_lm (ℝ-linear map);
complex.im_lm (ℝ-linear map);
complex.of_real_am (ℝ-algebra (homo)morphism);
complex.conj_ae (ℝ-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 real_part and imaginary_part for any element of a star_module over ℂ.

Notation #

ℜ and ℑ for the real_part and imaginary_part, respectively, in the locale complex_star_module.

@[protected, instance]

def complex.has_smul {R : Type u_1} [has_smul R ℝ] :

Equations

complex.has_smul = {smul := λ (r : R) (x : ℂ), {re := r • x.re - 0 * x.im, im := r • x.im + 0 * x.re}}

theorem complex.smul_re {R : Type u_1} [has_smul R ℝ] (r : R) (z : ℂ) :

(r • z).re = r • z.re

theorem complex.smul_im {R : Type u_1} [has_smul R ℝ] (r : R) (z : ℂ) :

(r • z).im = r • z.im

@[simp]

theorem complex.real_smul {x : ℝ} {z : ℂ} :

x • z = ↑x * z

@[protected, instance]

def complex.smul_comm_class {R : Type u_1} {S : Type u_2} [has_smul R ℝ] [has_smul S ℝ] [smul_comm_class R S ℝ] :

smul_comm_class R S ℂ

@[protected, instance]

def complex.is_scalar_tower {R : Type u_1} {S : Type u_2} [has_smul R S] [has_smul R ℝ] [has_smul S ℝ] [is_scalar_tower R S ℝ] :

is_scalar_tower R S ℂ

@[protected, instance]

def complex.is_central_scalar {R : Type u_1} [has_smul R ℝ] [has_smul Rᵐᵒᵖ ℝ] [is_central_scalar R ℝ] :

is_central_scalar R ℂ

@[protected, instance]

def complex.mul_action {R : Type u_1} [monoid R] [mul_action R ℝ] :

mul_action R ℂ

Equations

complex.mul_action = {to_has_smul := complex.has_smul mul_action.to_has_smul, one_smul := _, mul_smul := _}

@[protected, instance]

def complex.distrib_smul {R : Type u_1} [distrib_smul R ℝ] :

distrib_smul R ℂ

Equations

complex.distrib_smul = {to_smul_zero_class := {to_has_smul := complex.has_smul smul_zero_class.to_has_smul, smul_zero := _}, smul_add := _}

@[protected, instance]

def complex.distrib_mul_action {R : Type u_1} [semiring R] [distrib_mul_action R ℝ] :

distrib_mul_action R ℂ

Equations

complex.distrib_mul_action = {to_mul_action := complex.mul_action distrib_mul_action.to_mul_action, smul_zero := _, smul_add := _}

@[protected, instance]

def complex.module {R : Type u_1} [semiring R] [module R ℝ] :

Equations

complex.module = {to_distrib_mul_action := complex.distrib_mul_action module.to_distrib_mul_action, add_smul := _, zero_smul := _}

@[protected, instance]

def complex.algebra {R : Type u_1} [comm_semiring R] [algebra R ℝ] :

Equations

complex.algebra = {to_has_smul := {smul := has_smul.smul complex.has_smul}, to_ring_hom := {to_fun := (complex.of_real.comp (algebra_map R ℝ)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

@[protected, instance]

def complex.star_module :

star_module ℝ ℂ

@[simp]

theorem complex.coe_algebra_map :

⇑(algebra_map ℝ ℂ) = coe

@[simp]

theorem alg_hom.map_coe_real_complex {A : Type u_3} [semiring A] [algebra ℝ A] (f : ℂ →ₐ[ℝ ] A) (x : ℝ) :

⇑f ↑x = ⇑(algebra_map ℝ A) x

We need this lemma since complex.coe_algebra_map diverts the simp-normal form away from alg_hom.commutes.

@[ext]

theorem complex.alg_hom_ext {A : Type u_3} [semiring A] [algebra ℝ A] ⦃f g : ℂ →ₐ[ℝ ] A⦄ (h : ⇑f complex.I = ⇑g complex.I) :

f = g

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

@[protected]

theorem complex.ordered_smul :

ordered_smul ℝ ℂ

noncomputable def complex.basis_one_I :

basis (fin 2) ℝ ℂ

ℂ has a basis over ℝ given by 1 and I.

Equations

complex.basis_one_I = basis.of_equiv_fun {to_fun := λ (z : ℂ), ![z.re, z.im], map_add' := complex.basis_one_I._proof_1, map_smul' := complex.basis_one_I._proof_2, inv_fun := λ (c : fin 2 → ℝ), ↑(c 0) + c 1 • complex.I, left_inv := complex.basis_one_I._proof_5, right_inv := complex.basis_one_I._proof_6}

@[simp]

theorem complex.coe_basis_one_I_repr (z : ℂ) :

⇑(⇑(complex.basis_one_I.repr) z) = ![z.re, z.im]

@[simp]

theorem complex.coe_basis_one_I :

⇑complex.basis_one_I = ![1, complex.I]

@[protected, instance]

def complex.finite_dimensional :

finite_dimensional ℝ ℂ

@[simp]

theorem complex.finrank_real_complex :

finite_dimensional.finrank ℝ ℂ = 2

@[simp]

theorem complex.rank_real_complex :

module.rank ℝ ℂ = 2

theorem complex.rank_real_complex' :

(module.rank ℝ ℂ).lift = 2

theorem complex.finrank_real_complex_fact :

fact (finite_dimensional.finrank ℝ ℂ = 2)

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

@[protected, instance]

def module.complex_to_real (E : Type u_1) [add_comm_group E] [module ℂ E] :

Equations

module.complex_to_real E = restrict_scalars.module ℝ ℂ E

@[protected, instance]

def module.real_complex_tower (E : Type u_1) [add_comm_group E] [module ℂ E] :

is_scalar_tower ℝ ℂ E

@[simp, norm_cast]

theorem complex.coe_smul {E : Type u_1} [add_comm_group E] [module ℂ E] (x : ℝ) (y : E) :

↑x • y = x • y

@[protected, instance]

def smul_comm_class.complex_to_real {M : Type u_1} {E : Type u_2} [add_comm_group E] [module ℂ E] [has_smul M E] [smul_comm_class ℂ M E] :

smul_comm_class ℝ M E

The scalar action of ℝ on a ℂ-module E induced by module.complex_to_real commutes with another scalar action of M on E whenever the action of ℂ commutes with the action of M.

@[protected, instance]

def finite_dimensional.complex_to_real (E : Type u_1) [add_comm_group E] [module ℂ E] [finite_dimensional ℂ E] :

finite_dimensional ℝ E

theorem rank_real_of_complex (E : Type u_1) [add_comm_group E] [module ℂ E] :

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

theorem finrank_real_of_complex (E : Type u_1) [add_comm_group E] [module ℂ E] :

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

@[protected, instance]

def star_module.complex_to_real {E : Type u_1} [add_comm_group E] [has_star E] [module ℂ E] [star_module ℂ E] :

star_module ℝ E

def complex.re_lm :

ℂ →ₗ[ℝ ] ℝ

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

Equations

complex.re_lm = {to_fun := λ (x : ℂ), x.re, map_add' := complex.add_re, map_smul' := complex.re_lm._proof_1}

@[simp]

theorem complex.re_lm_coe :

⇑complex.re_lm = complex.re

def complex.im_lm :

ℂ →ₗ[ℝ ] ℝ

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

Equations

complex.im_lm = {to_fun := λ (x : ℂ), x.im, map_add' := complex.add_im, map_smul' := complex.im_lm._proof_1}

@[simp]

theorem complex.im_lm_coe :

⇑complex.im_lm = complex.im

def complex.of_real_am :

ℝ →ₐ[ℝ ] ℂ

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

Equations

complex.of_real_am = algebra.of_id ℝ ℂ

@[simp]

theorem complex.of_real_am_coe :

⇑complex.of_real_am = coe

def complex.conj_ae :

ℂ ≃ₐ[ℝ ] ℂ

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

Equations

complex.conj_ae = {to_fun := (star_ring_end ℂ).to_fun, inv_fun := ⇑(star_ring_end ℂ), left_inv := complex.conj_ae._proof_1, right_inv := complex.conj_ae._proof_2, map_mul' := complex.conj_ae._proof_3, map_add' := complex.conj_ae._proof_4, commutes' := complex.conj_of_real}

@[simp]

theorem complex.conj_ae_coe :

⇑complex.conj_ae = ⇑(star_ring_end ℂ)

@[simp]

theorem complex.to_matrix_conj_ae :

⇑(linear_map.to_matrix complex.basis_one_I complex.basis_one_I) complex.conj_ae.to_linear_map = ⇑matrix.of ![![1, 0], ![0, -1]]

The matrix representation of conj_ae.

theorem complex.real_alg_hom_eq_id_or_conj (f : ℂ →ₐ[ℝ ] ℂ) :

f = alg_hom.id ℝ ℂ ∨ f = ↑complex.conj_ae

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

def complex.equiv_real_prod_add_hom :

ℂ ≃+ ℝ × ℝ

The natural add_equiv from ℂ to ℝ × ℝ.

Equations

complex.equiv_real_prod_add_hom = {to_fun := complex.equiv_real_prod.to_fun, inv_fun := complex.equiv_real_prod.inv_fun, left_inv := complex.equiv_real_prod_add_hom._proof_1, right_inv := complex.equiv_real_prod_add_hom._proof_2, map_add' := complex.equiv_real_prod_add_hom._proof_3}

@[simp]

theorem complex.equiv_real_prod_add_hom_symm_apply_im (ᾰ : ℝ × ℝ) :

(⇑(complex.equiv_real_prod_add_hom.symm) ᾰ).im = ᾰ.snd

@[simp]

theorem complex.equiv_real_prod_add_hom_symm_apply_re (ᾰ : ℝ × ℝ) :

(⇑(complex.equiv_real_prod_add_hom.symm) ᾰ).re = ᾰ.fst

@[simp]

theorem complex.equiv_real_prod_add_hom_apply (ᾰ : ℂ) :

⇑complex.equiv_real_prod_add_hom ᾰ = (ᾰ.re, ᾰ.im)

def complex.equiv_real_prod_lm :

ℂ ≃ₗ[ℝ ] ℝ × ℝ

The natural linear_equiv from ℂ to ℝ × ℝ.

Equations

complex.equiv_real_prod_lm = {to_fun := complex.equiv_real_prod_add_hom.to_fun, map_add' := complex.equiv_real_prod_lm._proof_1, map_smul' := complex.equiv_real_prod_lm._proof_2, inv_fun := complex.equiv_real_prod_add_hom.inv_fun, left_inv := complex.equiv_real_prod_lm._proof_3, right_inv := complex.equiv_real_prod_lm._proof_4}

@[simp]

theorem complex.equiv_real_prod_lm_apply (ᾰ : ℂ) :

⇑complex.equiv_real_prod_lm ᾰ = (ᾰ.re, ᾰ.im)

@[simp]

theorem complex.equiv_real_prod_lm_symm_apply_im (ᾰ : ℝ × ℝ) :

(⇑(complex.equiv_real_prod_lm.symm) ᾰ).im = ᾰ.snd

@[simp]

theorem complex.equiv_real_prod_lm_symm_apply_re (ᾰ : ℝ × ℝ) :

(⇑(complex.equiv_real_prod_lm.symm) ᾰ).re = ᾰ.fst

def complex.lift_aux {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.lift_aux I' hf = alg_hom.of_linear_map ((algebra.of_id ℝ A).to_linear_map.comp complex.re_lm + (linear_map.to_span_singleton ℝ A I').comp complex.im_lm) _ _

@[simp]

theorem complex.lift_aux_apply {A : Type u_1} [ring A] [algebra ℝ A] (I' : A) (hI' : I' * I' = -1) (z : ℂ) :

⇑(complex.lift_aux I' hI') z = ⇑(algebra_map ℝ A) z.re + z.im • I'

theorem complex.lift_aux_apply_I {A : Type u_1} [ring A] [algebra ℝ A] (I' : A) (hI' : I' * I' = -1) :

⇑(complex.lift_aux I' hI') complex.I = I'

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

complex.lift = {to_fun := λ (I' : {I' // I' * I' = -1}), complex.lift_aux ↑I' _, inv_fun := λ (F : ℂ →ₐ[ℝ ] A), ⟨⇑F complex.I, _⟩, left_inv := _, right_inv := _}

@[simp]

theorem complex.lift_apply {A : Type u_1} [ring A] [algebra ℝ A] (I' : {I' // I' * I' = -1}) :

⇑complex.lift I' = complex.lift_aux ↑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_aux_I :

complex.lift_aux complex.I complex.I_mul_I = alg_hom.id ℝ ℂ

@[simp]

theorem complex.lift_aux_neg_I :

complex.lift_aux (-complex.I) _ = ↑complex.conj_ae

def skew_adjoint.neg_I_smul {A : Type u_1} [add_comm_group A] [module ℂ A] [star_add_monoid A] [star_module ℂ A] :

↥(skew_adjoint A) →ₗ[ℝ ] ↥(self_adjoint A)

Create a self_adjoint element from a skew_adjoint element by multiplying by the scalar -complex.I.

Equations

skew_adjoint.neg_I_smul = {to_fun := λ (a : ↥(skew_adjoint A)), ⟨-complex.I • ↑a, _⟩, map_add' := _, map_smul' := _}

@[simp]

theorem skew_adjoint.neg_I_smul_apply_coe {A : Type u_1} [add_comm_group A] [module ℂ A] [star_add_monoid A] [star_module ℂ A] (a : ↥(skew_adjoint A)) :

↑(⇑skew_adjoint.neg_I_smul a) = -complex.I • ↑a

theorem skew_adjoint.I_smul_neg_I {A : Type u_1} [add_comm_group A] [module ℂ A] [star_add_monoid A] [star_module ℂ A] (a : ↥(skew_adjoint A)) :

complex.I • ↑(⇑skew_adjoint.neg_I_smul a) = ↑a

noncomputable def real_part {A : Type u_1} [add_comm_group A] [module ℂ A] [star_add_monoid A] [star_module ℂ A] :

A →ₗ[ℝ ] ↥(self_adjoint A)

The real part ℜ a of an element a of a star module over ℂ, as a linear map. This is just self_adjoint_part ℝ, but we provide it as a separate definition in order to link it with lemmas concerning the imaginary_part, which doesn't exist in star modules over other rings.

Equations

real_part = self_adjoint_part ℝ

noncomputable def imaginary_part {A : Type u_1} [add_comm_group A] [module ℂ A] [star_add_monoid A] [star_module ℂ A] :

A →ₗ[ℝ ] ↥(self_adjoint 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 self_adjoint and skew_adjoint parts, but in a star module over ℂ we have real_part_add_I_smul_imaginary_part, which allows us to decompose into a linear combination of self_adjoints.

Equations

imaginary_part = skew_adjoint.neg_I_smul.comp (skew_adjoint_part ℝ)

@[simp]

theorem real_part_apply_coe {A : Type u_1} [add_comm_group A] [module ℂ A] [star_add_monoid A] [star_module ℂ A] (a : A) :

↑(⇑real_part a) = 2⁻¹ • (a + has_star.star a)

@[simp]

theorem imaginary_part_apply_coe {A : Type u_1} [add_comm_group A] [module ℂ A] [star_add_monoid A] [star_module ℂ A] (a : A) :

↑(⇑imaginary_part a) = -complex.I • 2⁻¹ • (a - has_star.star a)

theorem real_part_add_I_smul_imaginary_part {A : Type u_1} [add_comm_group A] [module ℂ A] [star_add_monoid A] [star_module ℂ A] (a : A) :

↑(⇑real_part a) + complex.I • ↑(⇑imaginary_part 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 real_part_I_smul {A : Type u_1} [add_comm_group A] [module ℂ A] [star_add_monoid A] [star_module ℂ A] (a : A) :

⇑real_part (complex.I • a) = -⇑imaginary_part a

@[simp]

theorem imaginary_part_I_smul {A : Type u_1} [add_comm_group A] [module ℂ A] [star_add_monoid A] [star_module ℂ A] (a : A) :

⇑imaginary_part (complex.I • a) = ⇑real_part a

theorem real_part_smul {A : Type u_1} [add_comm_group A] [module ℂ A] [star_add_monoid A] [star_module ℂ A] (z : ℂ) (a : A) :

⇑real_part (z • a) = z.re • ⇑real_part a - z.im • ⇑imaginary_part a

theorem imaginary_part_smul {A : Type u_1} [add_comm_group A] [module ℂ A] [star_add_monoid A] [star_module ℂ A] (z : ℂ) (a : A) :

⇑imaginary_part (z • a) = z.re • ⇑imaginary_part a + z.im • ⇑real_part a