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_equivfor noncommutativeR. 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 typeR →+* Rᵐᵒᵖ, which is very undesirable in the commutative case. One way out would be to define a new typeclassis_op R Sand have an instanceis_op R Rfor commutativeR. - Also note that such a definition involving
Rᵐᵒᵖoris_op R Swould require adding the appropriatering_hom_inv_pairinstances 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]
[module R A]
[star_module R A]
(ᾰ : A) :
⇑((star_linear_equiv R).symm) ᾰ = star_add_equiv.inv_fun ᾰ
@[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]
[module R A]
[star_module R A]
(ᾰ : A) :
⇑(star_linear_equiv R) ᾰ = star ᾰ
def
star_linear_equiv
(R : Type u_1)
{A : Type u_2}
[comm_ring R]
[star_ring R]
[semiring A]
[star_ring A]
[module R A]
[star_module R A] :
If A is a module over a commutative R with compatible actions,
then star is a semilinear equivalence.
Equations
- star_linear_equiv R = {to_fun := star has_involutive_star.to_has_star, map_add' := _, map_smul' := _, inv_fun := star_add_equiv.inv_fun, left_inv := _, right_inv := _}