# mathlib3documentation

topology.algebra.module.star

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[simp]
theorem starL_apply (R : Type u_1) {A : Type u_2} [star_ring R] [ A] [ A] (ᾰ : A) :
(starL R) =
@[simp]
theorem starL_to_linear_equiv (R : Type u_1) {A : Type u_2} [star_ring R] [ A] [ A]  :
def starL (R : Type u_1) {A : Type u_2} [star_ring R] [ A] [ A]  :

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

Equations
@[simp]
theorem starL_symm_apply (R : Type u_1) {A : Type u_2} [star_ring R] [ A] [ A] (ᾰ : A) :
@[simp]
theorem starL'_apply (R : Type u_1) {A : Type u_2} [star_ring R] [ A] [ A] (ᾰ : A) :
(starL' R) =
@[simp]
theorem starL'_symm_apply (R : Type u_1) {A : Type u_2} [star_ring R] [ A] [ A] (ᾰ : A) :
((starL' R).symm) = (star_add_equiv.symm) (({to_fun := id A, map_add' := _, map_smul' := _, inv_fun := id A, left_inv := _, right_inv := _}.symm) ᾰ)
@[simp]
theorem starL'_to_linear_equiv (R : Type u_1) {A : Type u_2} [star_ring R] [ A] [ A]  :
= {to_fun := id A, map_add' := _, map_smul' := _, inv_fun := id A, left_inv := _, right_inv := _}
def starL' (R : Type u_1) {A : Type u_2} [star_ring R] [ A] [ 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.

Equations
theorem continuous_self_adjoint_part (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] [invertible 2]  :
theorem continuous_skew_adjoint_part (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] [invertible 2]  :
theorem continuous_decompose_prod_adjoint (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] [invertible 2]  :
theorem continuous_decompose_prod_adjoint_symm (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] [invertible 2]  :
@[simp]
theorem self_adjoint_partL_apply_coe (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] [invertible 2] (x : A) :
( A) x) = 2 (x +
def self_adjoint_partL (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] [invertible 2]  :

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

Equations
@[simp]
theorem self_adjoint_partL_coe (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] [invertible 2]  :
@[simp]
theorem skew_adjoint_partL_apply_coe (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] [invertible 2] (x : A) :
( A) x) = 2 (x -
@[simp]
theorem skew_adjoint_partL_coe (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] [invertible 2]  :
def skew_adjoint_partL (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] [invertible 2]  :

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

Equations
@[simp]
theorem star_module.decompose_prod_adjointL_to_linear_equiv (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] [invertible 2]  :
def star_module.decompose_prod_adjointL (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] [invertible 2]  :

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

Equations
@[simp]
theorem star_module.decompose_prod_adjointL_apply (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] [invertible 2] (ᾰ : A) :
= (, ᾰ)
@[simp]
theorem star_module.decompose_prod_adjointL_symm_apply (R : Type u_1) (A : Type u_2) [semiring R] [ A] [ A] [invertible 2] (ᾰ : (self_adjoint A) × (skew_adjoint A)) :
= (ᾰ.fst) + (ᾰ.snd)