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 ] :
Equations
  • =
@[instance 90]
instance Complex.instIsScalarTowerOfReal {R : Type u_1} {S : Type u_2} [SMul R S] [SMul R ] [SMul S ] [IsScalarTower R S ] :
Equations
  • =
@[instance 90]
Equations
  • =
@[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 : →ₐ[] 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 :

has a basis over given by 1 and I.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Complex.coe_basisOneI_repr (z : ) :
    (Complex.basisOneI.repr z) = ![z.re, z.im]
    @[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.

    Equations
    • =

    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.

    Equations
    • =
    @[instance 900]
    Equations
    • =

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

    Equations
    Instances For

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

      Equations
      Instances For

        -algebra morphism version of the canonical embedding of in .

        Equations
        Instances For

          -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
            @[simp]

            The matrix representation of conjAe.

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

            @[simp]
            theorem Complex.equivRealProdLm_apply :
            ∀ (a : ), Complex.equivRealProdLm a = (a.re, a.im)

            The natural LinearEquiv from to ℝ × ℝ.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              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 : ) :
                (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) :
                @[simp]
                theorem Complex.lift_apply {A : Type u_1} [Ring A] [Algebra A] (I' : { I' : A // I' * I' = -1 }) :
                Complex.lift I' = Complex.liftAux 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
                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 skewAdjoint.negISMul_apply_coe {A : Type u_1} [AddCommGroup A] [Module A] [StarAddMonoid A] [StarModule A] (a : (skewAdjoint A)) :
                  (skewAdjoint.negISMul a) = -Complex.I 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
                    theorem skewAdjoint.I_smul_neg_I {A : Type u_1} [AddCommGroup A] [Module A] [StarAddMonoid A] [StarModule A] (a : (skewAdjoint A)) :
                    Complex.I (skewAdjoint.negISMul a) = a
                    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)
                            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 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] :
                            realPart ∘ₗ (selfAdjoint.submodule A).subtype = LinearMap.id
                            theorem imaginaryPart_comp_subtype_selfAdjoint {A : Type u_1} [AddCommGroup A] [Module A] [StarAddMonoid A] [StarModule A] :
                            imaginaryPart ∘ₗ (selfAdjoint.submodule A).subtype = 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
                            @[simp]
                            @[simp]
                            theorem Complex.selfAdjointEquiv_apply (z : (selfAdjoint )) :
                            Complex.selfAdjointEquiv z = (↑z).re

                            The natural -linear equivalence between selfAdjoint and .

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              theorem Complex.coe_selfAdjointEquiv (z : (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
                              theorem star_mul_self_add_self_mul_star {A : Type u_2} [NonUnitalRing 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))