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_natCast_smul {R : Type u_1} {M : Type u_2} [] [] [Module R M] [] (n : ) (x : M) :
star (n x) = n star x
@[simp]
theorem star_intCast_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_natCast_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_intCast_smul {R : Type u_1} {M : Type u_2} [] [] [Module R M] [] (n : ) (x : M) :
star ((n)⁻¹ x) = (n)⁻¹ star x
@[simp]
theorem star_ratCast_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), ().symm a = starAddEquiv.invFun 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.

Equations
• = let __src := starAddEquiv; { toFun := star, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }
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.

Equations
• = let __src := ; { toAddSubmonoid := __src.toAddSubmonoid, smul_mem' := }
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.

Equations
• = let __src := ; { toAddSubmonoid := __src.toAddSubmonoid, smul_mem' := }
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] ()

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

Equations
• = { toFun := fun (x : A) => 2 (x + star x), , map_add' := , map_smul' := }
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] ()

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

Equations
• = { toFun := fun (x : A) => 2 (x - star x), , map_add' := , map_smul' := }
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 = x, hx
theorem selfAdjointPart_comp_subtype_selfAdjoint (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] :
∘ₗ ().subtype = 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] [] [] [] :
∘ₗ ().subtype = 0
theorem selfAdjointPart_comp_subtype_skewAdjoint (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] :
∘ₗ ().subtype = 0
theorem skewAdjointPart_comp_subtype_skewAdjoint (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] :
∘ₗ ().subtype = LinearMap.id
@[simp]
theorem StarModule.decomposeProdAdjoint_apply (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] (i : A) :
= (() i, () i)
@[simp]
theorem StarModule.decomposeProdAdjoint_symm_apply (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] (a : () × ()) :
.symm a = ().subtype a.1 + ().subtype a.2
def StarModule.decomposeProdAdjoint (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] :
A ≃ₗ[R] () × ()

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} [] [] [] [] [Algebra R A] [] (r : R) :
() (star r) = star (() r)
theorem IsSelfAdjoint.algebraMap {R : Type u_1} (A : Type u_2) [] [] [] [] [Algebra R A] [] {r : R} (hr : ) :
theorem isSelfAdjoint_algebraMap_iff {R : Type u_1} {A : Type u_2} [] [] [] [] [Algebra R A] [] {r : R} (h : Function.Injective ()) :