mathlib documentation

algebra.star.module

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.

This file also provides some lemmas that need algebra.module.basic imported to prove.

TODO #

@[simp]
theorem star_int_cast_smul {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [star_add_monoid M] (n : ) (x : M) :
@[simp]
theorem star_nat_cast_smul {R : Type u_1} {M : Type u_2} [semiring R] [add_comm_monoid M] [module R M] [star_add_monoid M] (n : ) (x : M) :
@[simp]
theorem star_inv_int_cast_smul {R : Type u_1} {M : Type u_2} [division_ring R] [add_comm_group M] [module R M] [star_add_monoid M] (n : ) (x : M) :
@[simp]
theorem star_inv_nat_cast_smul {R : Type u_1} {M : Type u_2} [division_ring R] [add_comm_group M] [module R M] [star_add_monoid M] (n : ) (x : M) :
@[simp]
theorem star_rat_cast_smul {R : Type u_1} {M : Type u_2} [division_ring R] [add_comm_group M] [module R M] [star_add_monoid M] (n : ) (x : M) :
@[simp]
theorem star_rat_smul {R : Type u_1} [add_comm_group R] [star_add_monoid R] [module R] (x : R) (n : ) :
@[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) :
@[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) :
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
def self_adjoint.submodule (R : Type u_1) (A : Type u_2) [semiring R] [star_semigroup R] [has_trivial_star R] [add_comm_group A] [module R A] [star_add_monoid A] [star_module R A] :

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

Equations
def skew_adjoint.submodule (R : Type u_1) (A : Type u_2) [semiring R] [star_semigroup R] [has_trivial_star R] [add_comm_group A] [module R A] [star_add_monoid A] [star_module R A] :

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

Equations
def self_adjoint_part (R : Type u_1) {A : Type u_2} [semiring R] [star_semigroup R] [has_trivial_star R] [add_comm_group A] [module R A] [star_add_monoid A] [star_module R A] [invertible 2] :

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

Equations
@[simp]
theorem self_adjoint_part_apply_coe (R : Type u_1) {A : Type u_2} [semiring R] [star_semigroup R] [has_trivial_star R] [add_comm_group A] [module R A] [star_add_monoid A] [star_module R A] [invertible 2] (x : A) :
def skew_adjoint_part (R : Type u_1) {A : Type u_2} [semiring R] [star_semigroup R] [has_trivial_star R] [add_comm_group A] [module R A] [star_add_monoid A] [star_module R A] [invertible 2] :

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

Equations
@[simp]
theorem skew_adjoint_part_apply_coe (R : Type u_1) {A : Type u_2} [semiring R] [star_semigroup R] [has_trivial_star R] [add_comm_group A] [module R A] [star_add_monoid A] [star_module R A] [invertible 2] (x : A) :

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

Equations
@[simp]
theorem algebra_map_star_comm {R : Type u_1} {A : Type u_2} [comm_semiring R] [star_ring R] [semiring A] [star_semigroup A] [algebra R A] [star_module R A] (r : R) :