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

## 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_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) :
= star
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