# Documentation

Mathlib.Topology.Algebra.Module.Star

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

@[simp]
theorem starL_symm_apply (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] :
@[simp]
theorem starL_apply (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] :
∀ (a : A), ↑() a = star a
def starL (R : Type u_1) {A : Type u_2} [] [] [] [] [Module R A] [] [] [] :

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

Instances For
@[simp]
theorem starL'_symm_apply (R : Type u_1) {A : Type u_2} [] [] [] [] [] [Module R A] [] [] [] :
∀ (a : A), ↑() a = ↑(LinearEquiv.symm ().toLinearEquiv) (↑(LinearEquiv.symm { toLinearMap := { toAddHom := { toFun := id, map_add' := (_ : ∀ (x y : A), Equiv.toFun ().toEquiv (x + y) = Equiv.toFun ().toEquiv x + Equiv.toFun ().toEquiv y) }, map_smul' := (_ : ∀ (r : R) (a : A), r a = star r a) }, invFun := id, left_inv := (_ : Function.LeftInverse ().toEquiv.invFun ().toEquiv.toFun), right_inv := (_ : Function.RightInverse ().toEquiv.invFun ().toEquiv.toFun) }) a)
@[simp]
theorem starL'_apply (R : Type u_1) {A : Type u_2} [] [] [] [] [] [Module R A] [] [] [] :
∀ (a : A), ↑() a = star a
def starL' (R : Type u_1) {A : Type u_2} [] [] [] [] [] [Module R A] [] [] [] :
A ≃L[R] A

If A is a topological module over a commutative R with trivial star and compatible actions, then star is a continuous linear equivalence.

Instances For
theorem continuous_selfAdjointPart (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] [] [] [] [] :
theorem continuous_skewAdjointPart (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] [] [] [] [] :
theorem continuous_decomposeProdAdjoint (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] [] [] [] :
theorem continuous_decomposeProdAdjoint_symm (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] [] :
@[simp]
theorem selfAdjointPartL_apply_coe (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] [] [] [] [] (x : A) :
↑(↑() x) = 2 x + 2 star x
@[simp]
theorem selfAdjointPartL_toFun_coe (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] [] [] [] [] (x : A) :
↑(↑() x) = 2 x + 2 star x
def selfAdjointPartL (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] [] [] [] [] :
A →L[R] { x // x }

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

Instances For
@[simp]
theorem skewAdjointPartL_apply_coe (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] [] [] [] [] (x : A) :
↑(↑() x) = 2 (x - star x)
@[simp]
theorem skewAdjointPartL_toFun_coe (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] [] [] [] [] (x : A) :
↑(↑() x) = 2 (x - star x)
def skewAdjointPartL (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] [] [] [] [] :
A →L[R] { x // x }

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

Instances For
@[simp]
theorem StarModule.decomposeProdAdjointL_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.decomposeProdAdjointL_apply (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] [] [] [] (i : A) :
↑() i = (↑() i, ↑() i)
def StarModule.decomposeProdAdjointL (R : Type u_1) (A : Type u_2) [] [] [] [] [Module R A] [] [] [] [] [] [] :
A ≃L[R] { x // x } × { x // x }

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

Instances For