Documentation

Mathlib.Algebra.Star.Module

The star operation, bundled as a star-linear equiv #

We define starLinearEquiv, which is the star operation bundled as a star-linear map. It is defined on a star algebra A over the base ring R.

This file also provides some lemmas that need Algebra.Module.Basic imported to prove.

TODO #

@[simp]
theorem star_nat_cast_smul {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [StarAddMonoid M] (n : ) (x : M) :
star (n x) = n star x
@[simp]
theorem star_int_cast_smul {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [StarAddMonoid M] (n : ) (x : M) :
star (n x) = n star x
@[simp]
theorem star_inv_nat_cast_smul {R : Type u_1} {M : Type u_2} [DivisionSemiring R] [AddCommMonoid M] [Module R M] [StarAddMonoid M] (n : ) (x : M) :
star ((n)⁻¹ x) = (n)⁻¹ star x
@[simp]
theorem star_inv_int_cast_smul {R : Type u_1} {M : Type u_2} [DivisionRing R] [AddCommGroup M] [Module R M] [StarAddMonoid M] (n : ) (x : M) :
star ((n)⁻¹ x) = (n)⁻¹ star x
@[simp]
theorem star_rat_cast_smul {R : Type u_1} {M : Type u_2} [DivisionRing R] [AddCommGroup M] [Module R M] [StarAddMonoid M] (n : ) (x : M) :
star (n x) = n star x
@[simp]
theorem star_rat_smul {R : Type u_3} [AddCommGroup R] [StarAddMonoid R] [Module R] (x : R) (n : ) :
star (n x) = n star x
@[simp]
theorem starLinearEquiv_symm_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] :
∀ (a : A), ↑(LinearEquiv.symm (starLinearEquiv R)) a = Equiv.invFun starAddEquiv.toEquiv a
@[simp]
theorem starLinearEquiv_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] :
∀ (a : A), ↑(starLinearEquiv R) a = star a
def starLinearEquiv (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] :

If A is a module over a commutative R with compatible actions, then star is a semilinear equivalence.

Instances For
    def selfAdjoint.submodule (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] :

    The self-adjoint elements of a star module, as a submodule.

    Instances For
      def skewAdjoint.submodule (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] :

      The skew-adjoint elements of a star module, as a submodule.

      Instances For
        @[simp]
        theorem selfAdjointPart_apply_coe (R : Type u_1) {A : Type u_2} [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] (x : A) :
        ↑(↑(selfAdjointPart R) x) = 2 (x + star x)
        def selfAdjointPart (R : Type u_1) {A : Type u_2} [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] :
        A →ₗ[R] { x // x selfAdjoint A }

        The self-adjoint part of an element of a star module, as a linear map.

        Instances For
          @[simp]
          theorem skewAdjointPart_apply_coe (R : Type u_1) {A : Type u_2} [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] (x : A) :
          ↑(↑(skewAdjointPart R) x) = 2 (x - star x)
          def skewAdjointPart (R : Type u_1) {A : Type u_2} [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] :
          A →ₗ[R] { x // x skewAdjoint A }

          The skew-adjoint part of an element of a star module, as a linear map.

          Instances For
            theorem StarModule.selfAdjointPart_add_skewAdjointPart (R : Type u_1) {A : Type u_2} [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] (x : A) :
            ↑(↑(selfAdjointPart R) x) + ↑(↑(skewAdjointPart R) x) = x
            theorem IsSelfAdjoint.coe_selfAdjointPart_apply (R : Type u_1) {A : Type u_2} [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] {x : A} (hx : IsSelfAdjoint x) :
            ↑(↑(selfAdjointPart R) x) = x
            theorem IsSelfAdjoint.selfAdjointPart_apply (R : Type u_1) {A : Type u_2} [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] {x : A} (hx : IsSelfAdjoint x) :
            ↑(selfAdjointPart R) x = { val := x, property := hx }
            theorem IsSelfAdjoint.skewAdjointPart_apply (R : Type u_1) {A : Type u_2} [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] {x : A} (hx : IsSelfAdjoint x) :
            ↑(skewAdjointPart R) x = 0
            @[simp]
            def StarModule.decomposeProdAdjoint (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] :
            A ≃ₗ[R] { x // x selfAdjoint A } × { x // x skewAdjoint A }

            The decomposition of elements of a star module into their self- and skew-adjoint parts, as a linear equivalence.

            Instances For
              @[simp]
              theorem algebraMap_star_comm {R : Type u_3} {A : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarMul A] [Algebra R A] [StarModule R A] (r : R) :
              ↑(algebraMap R A) (star r) = star (↑(algebraMap R A) r)