Documentation

Mathlib.Data.Complex.Module

Complex number as a vector space over #

This file contains the following instances:

It also defines bundled versions of four standard maps (respectively, the real part, the imaginary part, the embedding of in , and the complex conjugate):

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 #

@[instance 90]
instance Complex.instSMulCommClassOfReal {R : Type u_1} {S : Type u_2} [SMul R ] [SMul S ] [SMulCommClass R S ] :
@[instance 90]
instance Complex.instIsScalarTowerOfReal {R : Type u_1} {S : Type u_2} [SMul R S] [SMul R ] [SMul S ] [IsScalarTower R S ] :
@[instance 90]
instance Complex.mulAction {R : Type u_1} [Monoid R] [MulAction R ] :
Equations
    @[instance 90]
    Equations
      @[instance 90]
      Equations
        @[instance 100]
        instance Complex.instModule {R : Type u_1} [Semiring R] [Module R ] :
        Equations
          @[instance 95]
          Equations
            @[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 g : →ₐ[] A (h : f I = g I) :
            f = g

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

            theorem Complex.algHom_ext_iff {A : Type u_3} [Semiring A] [Algebra A] {f g : →ₐ[] A} :
            f = g f I = g I
            noncomputable def Complex.basisOneI :

            has a basis over given by 1 and I.

            Equations
              Instances For
                @[simp]
                @[instance 900]
                instance Module.complexToReal (E : Type u_1) [AddCommGroup E] [Module E] :
                Equations
                  @[instance 900]
                  instance Algebra.complexToReal {A : Type u_1} [Semiring A] [Algebra A] :
                  Equations
                    @[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] :

                    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.

                    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.

                    @[instance 900]

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

                    Equations
                      Instances For
                        @[simp]

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

                        Equations
                          Instances For
                            @[simp]

                            -algebra morphism version of the canonical embedding of in .

                            Equations
                              Instances For

                                -algebra isomorphism version of the complex conjugation function from to

                                Equations
                                  Instances For
                                    @[simp]

                                    The matrix representation of conjAe.

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

                                    The natural LinearEquiv from to ℝ × ℝ.

                                    Equations
                                      Instances For
                                        @[simp]
                                        theorem Complex.equivRealProdLm_apply (a✝ : ) :
                                        equivRealProdLm a✝ = (a✝.re, a✝.im)
                                        def Complex.liftAux {A : Type u_1} [Ring A] [Algebra A] (I' : A) (hf : I' * I' = -1) :

                                        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
                                          Instances For
                                            @[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'
                                            theorem Complex.liftAux_apply_I {A : Type u_1} [Ring A] [Algebra A] (I' : A) (hI' : I' * I' = -1) :
                                            (liftAux I' hI') I = 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
                                              Instances For
                                                @[simp]
                                                theorem Complex.lift_apply {A : Type u_1} [Ring A] [Algebra A] (I' : { I' : A // I' * I' = -1 }) :
                                                lift I' = liftAux I'
                                                @[simp]
                                                theorem Complex.lift_symm_apply_coe {A : Type u_1} [Ring A] [Algebra A] (F : →ₐ[] A) :
                                                (lift.symm F) = F I
                                                @[simp]

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

                                                Equations
                                                  Instances For
                                                    @[simp]
                                                    noncomputable def realPart {A : Type u_1} [AddCommGroup A] [Module A] [StarAddMonoid A] [StarModule 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
                                                      Instances For
                                                        noncomputable def imaginaryPart {A : Type u_1} [AddCommGroup A] [Module A] [StarAddMonoid A] [StarModule 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
                                                          Instances For

                                                            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
                                                              Instances For

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

                                                                    theorem realPart_smul {A : Type u_1} [AddCommGroup A] [Module A] [StarAddMonoid A] [StarModule A] (z : ) (a : A) :
                                                                    theorem IsSelfAdjoint.coe_realPart {A : Type u_1} [AddCommGroup A] [Module A] [StarAddMonoid A] [StarModule A] {x : A} (hx : IsSelfAdjoint x) :
                                                                    (realPart x) = x
                                                                    @[simp]
                                                                    @[simp]
                                                                    theorem realPart_idem {A : Type u_1} [AddCommGroup A] [Module A] [StarAddMonoid A] [StarModule A] {x : A} :

                                                                    The natural -linear equivalence between selfAdjoint and .

                                                                    Equations
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem realPart_ofReal (r : ) :
                                                                        (realPart r) = r
                                                                        @[simp]
                                                                        theorem imaginaryPart_ofReal (r : ) :
                                                                        theorem Complex.coe_realPart (z : ) :
                                                                        (realPart z) = z.re