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 Complex.mulAction {R : Type u_1} [Monoid R] [MulAction R ] :
Equations
Equations
Equations
  • One or more equations did not get rendered due to their size.
instance Complex.instModule {R : Type u_1} [Semiring R] [Module R ] :
Equations
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]

    Fact version of the dimension of over , locally useful in the definition of the circle.

    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 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
    • =
    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.equivRealProdAddHom_apply (z : ) :
            Complex.equivRealProdAddHom z = (z.re, z.im)

            The natural AddEquiv from to ℝ × ℝ.

            Equations
            Instances For
              @[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_symm_apply_coe {A : Type u_1} [Ring A] [Algebra A] (F : →ₐ[] A) :
                  (Complex.lift.symm F) = F Complex.I
                  @[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'
                  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
                  • One or more equations did not get rendered due to their size.
                  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 = { toAddHom := { toFun := fun (a : (skewAdjoint A)) => { val := -Complex.I a, property := }, 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
                              @[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]
                              theorem Complex.selfAdjointEquiv_apply (z : (selfAdjoint )) :
                              Complex.selfAdjointEquiv z = (z).re
                              @[simp]
                              theorem Complex.selfAdjointEquiv_symm_apply (x : ) :
                              (LinearEquiv.symm Complex.selfAdjointEquiv) x = { val := x, property := }

                              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))

                                and are isomorphic as vector spaces over , or equivalently, as additive groups.