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 = starAddEquiv.invFun 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.

Equations
  • starLinearEquiv R = let __src := starAddEquiv; { toLinearMap := { toAddHom := { toFun := star, map_add' := }, map_smul' := }, invFun := __src.invFun, left_inv := , right_inv := }
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.

    Equations
    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.

      Equations
      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] :

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

        Equations
        • selfAdjointPart R = { toAddHom := { toFun := fun (x : A) => { val := 2 (x + star x), property := }, map_add' := }, map_smul' := }
        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] :

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

          Equations
          • skewAdjointPart R = { toAddHom := { toFun := fun (x : A) => { val := 2 (x - star x), property := }, map_add' := }, map_smul' := }
          Instances For
            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 }

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem algebraMap_star_comm {R : Type u_1} {A : Type u_2} [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)
              theorem IsSelfAdjoint.algebraMap {R : Type u_1} (A : Type u_2) [CommSemiring R] [StarRing R] [Semiring A] [StarMul A] [Algebra R A] [StarModule R A] {r : R} (hr : IsSelfAdjoint r) :