# mathlibdocumentation

algebra.star.module

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

We define star_linear_equiv, 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 #

• Define star_linear_equiv for noncommutative R. We only the commutative case for now since, in the noncommutative case, the ring hom needs to reverse the order of multiplication. This requires a ring hom of type R →+* Rᵐᵒᵖ, which is very undesirable in the commutative case. One way out would be to define a new typeclass is_op R S and have an instance is_op R R for commutative R.
• Also note that such a definition involving Rᵐᵒᵖ or is_op R S would require adding the appropriate ring_hom_inv_pair instances to be able to define the semilinear equivalence.
@[simp]
theorem star_int_cast_smul {R : Type u_1} {M : Type u_2} [ring R] [ M] (n : ) (x : M) :
@[simp]
theorem star_nat_cast_smul {R : Type u_1} {M : Type u_2} [semiring R] [ M] (n : ) (x : M) :
@[simp]
theorem star_inv_int_cast_smul {R : Type u_1} {M : Type u_2} [ M] (n : ) (x : M) :
@[simp]
theorem star_inv_nat_cast_smul {R : Type u_1} {M : Type u_2} [ M] (n : ) (x : M) :
@[simp]
theorem star_rat_cast_smul {R : Type u_1} {M : Type u_2} [ M] (n : ) (x : M) :
@[simp]
theorem star_rat_smul {R : Type u_1} [ R] (x : R) (n : ) :
@[simp]
theorem star_linear_equiv_symm_apply (R : Type u_1) {A : Type u_2} [comm_ring R] [star_ring R] [semiring A] [star_ring A] [ A] [ A] (ᾰ : A) :
.symm) =
@[simp]
theorem star_linear_equiv_apply (R : Type u_1) {A : Type u_2} [comm_ring R] [star_ring R] [semiring A] [star_ring A] [ A] [ A] (ᾰ : A) :
=
def star_linear_equiv (R : Type u_1) {A : Type u_2} [comm_ring R] [star_ring R] [semiring A] [star_ring A] [ A] [ A] :

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

Equations
def self_adjoint.submodule (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] :
A

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

Equations
def skew_adjoint.submodule (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] :
A

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

Equations
def self_adjoint_part (R : Type u_1) {A : Type u_2} [semiring R] [ A] [ A] [invertible 2] :

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

Equations
@[simp]
theorem self_adjoint_part_apply_coe (R : Type u_1) {A : Type u_2} [semiring R] [ A] [ A] [invertible 2] (x : A) :
( x) = 2 (x +
def skew_adjoint_part (R : Type u_1) {A : Type u_2} [semiring R] [ A] [ A] [invertible 2] :

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

Equations
@[simp]
theorem skew_adjoint_part_apply_coe (R : Type u_1) {A : Type u_2} [semiring R] [ A] [ A] [invertible 2] (x : A) :
( x) = 2 (x -
theorem star_module.self_adjoint_part_add_skew_adjoint_part (R : Type u_1) {A : Type u_2} [semiring R] [ A] [ A] [invertible 2] (x : A) :
( x) + ( x) = x
def star_module.decompose_prod_adjoint (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] [invertible 2] :

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

Equations
@[simp]
theorem star_module.decompose_prod_adjoint_apply (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] [invertible 2] (ᾰ : A) :
= (, ᾰ)
@[simp]
theorem star_module.decompose_prod_adjoint_symm_apply (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] [invertible 2] (ᾰ : (self_adjoint A) × (skew_adjoint A)) :
= (ᾰ.fst) + (ᾰ.snd)