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_natCast_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
@[deprecated star_natCast_smul]
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

Alias of star_natCast_smul.

@[simp]
theorem star_intCast_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
@[deprecated star_intCast_smul]
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

Alias of star_intCast_smul.

@[simp]
theorem star_inv_natCast_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
@[deprecated star_inv_natCast_smul]
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

Alias of star_inv_natCast_smul.

@[simp]
theorem star_inv_intCast_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
@[deprecated star_inv_intCast_smul]
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

Alias of star_inv_intCast_smul.

@[simp]
theorem star_ratCast_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
@[deprecated star_ratCast_smul]
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

Alias of star_ratCast_smul.

Per the naming convention, these two lemmas call (q • ·) nnrat_smul and rat_smul respectively, rather than nnqsmul and qsmul because the latter are reserved to the actions coming from DivisionSemiring and DivisionRing. We provide aliases with nnqsmul and qsmul for discoverability.

@[simp]
theorem star_nnrat_smul {R : Type u_1} [AddCommMonoid R] [StarAddMonoid R] [Module ℚ≥0 R] (q : ℚ≥0) (x : R) :
star (q x) = q star x

Note that this lemma holds for an arbitrary ℚ≥0-action, rather than merely one coming from a DivisionSemiring. We keep both the nnqsmul and nnrat_smul naming conventions for discoverability. See star_nnqsmul.

@[simp]
theorem star_rat_smul {R : Type u_1} [AddCommGroup R] [StarAddMonoid R] [Module R] (q : ) (x : R) :
star (q x) = q star x

Note that this lemma holds for an arbitrary -action, rather than merely one coming from a DivisionRing. We keep both the qsmul and rat_smul naming conventions for discoverability. See star_qsmul.

theorem star_nnqsmul {R : Type u_1} [AddCommMonoid R] [StarAddMonoid R] [Module ℚ≥0 R] (q : ℚ≥0) (x : R) :
star (q x) = q star x

Note that this lemma holds for an arbitrary ℚ≥0-action, rather than merely one coming from a DivisionSemiring. We keep both the nnqsmul and nnrat_smul naming conventions for discoverability. See star_nnrat_smul.

theorem star_qsmul {R : Type u_1} [AddCommGroup R] [StarAddMonoid R] [Module R] (q : ) (x : R) :
star (q x) = q star x

Note that this lemma holds for an arbitrary -action, rather than merely one coming from a DivisionRing. We keep both the qsmul and rat_smul naming conventions for discoverability. See star_rat_smul.

Equations
  • =
@[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), (starLinearEquiv R).symm 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 = { toFun := star, map_add' := , map_smul' := , invFun := starAddEquiv.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
        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
          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 = x, hx
            theorem selfAdjointPart_comp_subtype_selfAdjoint (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] :
            selfAdjointPart R ∘ₗ (selfAdjoint.submodule R A).subtype = LinearMap.id
            theorem skewAdjointPart_comp_subtype_skewAdjoint (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] :
            skewAdjointPart R ∘ₗ (skewAdjoint.submodule R A).subtype = LinearMap.id
            @[simp]
            theorem StarModule.decomposeProdAdjoint_symm_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] (a : (selfAdjoint A) × (skewAdjoint A)) :
            (StarModule.decomposeProdAdjoint R A).symm a = (selfAdjoint.submodule R A).subtype a.1 + (skewAdjoint.submodule R A).subtype a.2

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

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