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

• Define starLinearEquiv 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 IsOp R S and have an instance IsOp R R for commutative R.
• Also note that such a definition involving Rᵐᵒᵖ or is_op R S would require adding the appropriate RingHomInvPair instances to be able to define the semilinear equivalence.
@[simp]
theorem star_nat_cast_smul {R : Type u_1} {M : Type u_2} [] [] [Module R 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] [] [Module R 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} [] [] [Module R 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} [] [] [Module R M] [] (n : ) (x : M) :
star ((n)⁻¹ x) = (n)⁻¹ star x
@[simp]
theorem star_rat_cast_smul {R : Type u_1} {M : Type u_2} [] [] [Module R M] [] (n : ) (x : M) :
star (n x) = n star x
@[simp]
theorem star_rat_smul {R : Type u_3} [] [] [] (x : R) (n : ) :
star (n x) = n star x
@[simp]
theorem starLinearEquiv_symm_apply (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] :
∀ (a : A), ↑() a = Equiv.invFun starAddEquiv.toEquiv a
@[simp]
theorem starLinearEquiv_apply (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] :
∀ (a : A), ↑() a = star a
def starLinearEquiv (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] :

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

Instances For
def selfAdjoint.submodule (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] :

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

Instances For
def skewAdjoint.submodule (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] :

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

Instances For
@[simp]
theorem selfAdjointPart_apply_coe (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] (x : A) :
↑(↑() x) = 2 (x + star x)
def selfAdjointPart (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] :
A →ₗ[R] { x // x }

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

Instances For
@[simp]
theorem skewAdjointPart_apply_coe (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] (x : A) :
↑(↑() x) = 2 (x - star x)
def skewAdjointPart (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] :
A →ₗ[R] { x // x }

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

Instances For
theorem StarModule.selfAdjointPart_add_skewAdjointPart (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] (x : A) :
↑(↑() x) + ↑(↑() x) = x
theorem IsSelfAdjoint.coe_selfAdjointPart_apply (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] {x : A} (hx : ) :
↑(↑() x) = x
theorem IsSelfAdjoint.selfAdjointPart_apply (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] {x : A} (hx : ) :
↑() x = { val := x, property := hx }
theorem selfAdjointPart_comp_subtype_selfAdjoint (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] :
= LinearMap.id
theorem IsSelfAdjoint.skewAdjointPart_apply (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] {x : A} (hx : ) :
↑() x = 0
theorem skewAdjointPart_comp_subtype_selfAdjoint (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] :
theorem selfAdjointPart_comp_subtype_skewAdjoint (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] :
theorem skewAdjointPart_comp_subtype_skewAdjoint (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] :
= LinearMap.id
@[simp]
theorem StarModule.decomposeProdAdjoint_symm_apply (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] (a : { x // x } × { x // x }) :
= ↑() a.fst + ↑() a.snd
@[simp]
theorem StarModule.decomposeProdAdjoint_apply (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] (i : A) :
↑() i = (↑() i, ↑() i)
def StarModule.decomposeProdAdjoint (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] :
A ≃ₗ[R] { x // x } × { x // x }

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

Instances For
@[simp]
theorem algebraMap_star_comm {R : Type u_3} {A : Type u_4} [] [] [] [] [Algebra R A] [] (r : R) :
↑() (star r) = star (↑() r)