mathlib documentation

data.complex.module

Complex number as a vector space over `ℝ` #

This file contains the following instances:

Any •-structure (has_scalar, 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.

@[protected, instance]

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

has_scalar R ℂ

Equations

complex.has_scalar = {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_scalar R ℝ] (r : R) (z : ℂ) :

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

theorem complex.smul_im {R : Type u_1} [has_scalar 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_scalar R ℝ] [has_scalar 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_scalar R S] [has_scalar R ℝ] [has_scalar S ℝ] [is_scalar_tower R S ℝ] :

is_scalar_tower R S ℂ

@[protected, instance]

def complex.is_central_scalar {R : Type u_1} [has_scalar R ℝ] [has_scalar 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_scalar := complex.has_scalar mul_action.to_has_scalar, one_smul := _, mul_smul := _}

@[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_add := _, smul_zero := _}

@[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_scalar := {smul := has_scalar.smul complex.has_scalar}, 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' := _}

@[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, instance]

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_3, right_inv := complex.basis_one_I._proof_4}

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

module.rank ℝ ℂ = 2

theorem complex.dim_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 finite_dimensional.complex_to_real (E : Type u_1) [add_comm_group E] [module ℂ E] [finite_dimensional ℂ E] :

finite_dimensional ℝ E

theorem dim_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

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 := conj.to_fun, inv_fun := ⇑conj, 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 = ⇑conj

@[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 = ![![1, 0], ![0, -1]]

The matrix representation of conj_ae.

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